typecheck/failure/duplicateFields.dhall spec test fails in parsing step instead in type checking one

[jneira]

Hi, the spec tes case https://github.com/dhall-lang/dhall-lang/blob/master/tests/typecheck/failure/duplicateFields.dhall fails when parsing instead when typechecking:

D:\dhall-lang\tests\typecheck\failure>dhall format < duplicateFields.dhall

Error: Invalid input

(stdin):1:16:
  |
1 | { a = 1, a = 2 }
  |                ^
duplicate field: a

As parsing is needed to make the type check, there is no way to test it properly. If the standard forbids the parsing of duplicated fields the test should be moved to tests/parser/failure (and test code should be changed), otherwise the haskell impl should be changed to allow parse the expression. AFAIU the grammar spec doesn't disallow duplicate fields in records.

[f-f]

@jneira this is a known bug of the Haskell implementation. I think we mentioned it in some issue or PR, but I cannot find it at the moment, so I guess we can use this issue to track it.

This is correctly a typecheck failure, as the standards forbids it at typecheck time. You can see more details on this in https://github.com/dhall-lang/dhall-lang/pull/278 (I also considered forbidding this at parse time, but it's not possible to specify such thing in the grammar)

[Gabriella439]

Yeah, this is a non-standard behavior of the Haskell implementation. Fixing this properly will require changing the representation of Map used for parsing vs. type-checking

[MonoidMusician]

That’s what I did in dhall-purescript – I parameterized Expr over the functor used for Record(Lit) and Union(Lit) (also Project). For parsing, I just use a functor that looks like Array (Tuple String a), which will allow duplicate fields, and then during typechecking it is polymorphic what functor I use, but I check to make sure there are no duplicate keys, and internally I use Map String for an unordered comparison, as necessary. (It also makes sense to preserve order when interacting with the AST, for my application, so I mainly use the ordered format.) Here’s the specific commit where I made normalization and typechecking use the unordered fields: https://github.com/MonoidMusician/dhall-purescript/commit/942e33e4cbebad803e8954373daf1a68831678f1 And here’s the helper I use to ensure there are no duplicate keys during normalization: https://github.com/MonoidMusician/dhall-purescript/blob/d6068a760134a2847f3046194a440113a762f394/src/Dhall/TypeCheck.purs#L657

[sjakobi]

Here is an up-to-date list of the problematic test cases:

$ for f in *.dhall
    dhall resolve --immediate-dependencies --file $f
end

dhall: 
Error: Invalid input

RecordLitDuplicateFields.dhall:1:16:
  |
1 | { x = 0, x = 0 }
  |                ^
duplicate field: x

dhall: 
Error: Invalid input

RecordTypeDuplicateFields.dhall:1:26:
  |
1 | { x: Natural, x: Natural }
  |                          ^
duplicate field: x

dhall: 
Error: Invalid input

UnionTypeDuplicateVariants1.dhall:1:7:
  |
1 | <x | x>
  |       ^
duplicate field: x

dhall: 
Error: Invalid input

UnionTypeDuplicateVariants2.dhall:1:16:
  |
1 | <x | x: Natural>
  |                ^
duplicate field: x