Type error depends on name of irrelevant record field

[Radvendii]

Describe the bug

let f | forall r. { ; r } -> { x : Number; r } 
       = fun r => %record_insert% "x" r 1 in
(f { x = 0, a = 0 }: _) 

results in a type error

let f | forall r. { ; r } -> { x : Number; r } 
       = fun r => %record_insert% "x" r 1 in
(f { x = 0, y = 0 }: _)

does not

The only difference is whether the second (irrelevant) parameter (a/y) is before or after x in the alphabet.

Expected behavior
This should result in a type error regardless.

Environment

• OS name + version: NixOS
• Version of the code: master

[vkleen]

As far as I can tell, all variations of this (also with type annotation on f instead of a contract annotation) produce errors. None of them are particularly helpful, but it looks like the type checker is complaining about the right thing. Namely, record_insert is typed using dictionary types which are (unfortunately) incompatible with row thing.

The errors in the dynamically typed variants are pretty useless, though.

nickel> let f : forall r. { ; r } -> { x : Number; r }
       = fun r => %record_insert% "x" r 1 in
(f { x = 0, a = 0 }: _)
error: incompatible types
  ┌─ repl-input-0:2:39
  │
2 │        = fun r => %record_insert% "x" r 1 in
  │                                       ^ this expression
  │
  = Expected an expression of type `{ _ : _a }`
  = Found an expression of type `{  ; r }`
  = These types are not compatible

nickel> let f | forall r. { ; r } -> { x : Number; r }
       = fun r => %record_insert% "x" r 1 in
(f { x = 0, a = 0 }: _)
error: multiple rows declaration
  ┌─ repl-input-1:3:4
  │
3 │ (f { x = 0, a = 0 }: _)
  │    ^^^^^^^^^^^^^^^^ this expression
  │
  = Found an expression of a record type with the row `x: { x: _a, a: _b }`
  = But this type appears inside another row type, which already has a declaration for the field `x`
  = A type cannot have two conflicting declarations for the same row

nickel> let f : forall r. { ; r } -> { x : Number; r }
       = fun r => %record_insert% "x" r 1 in
(f { x = 0, y = 0 }: _)
error: incompatible types
  ┌─ repl-input-2:2:39
  │
2 │        = fun r => %record_insert% "x" r 1 in
  │                                       ^ this expression
  │
  = Expected an expression of type `{ _ : _a }`
  = Found an expression of type `{  ; r }`
  = These types are not compatible

nickel> let f | forall r. { ; r } -> { x : Number; r }
       = fun r => %record_insert% "x" r 1 in
(f { x = 0, y = 0 }: _)
error: non mergeable terms
    ┌─ repl-input-3:2:41
    │
  2 │        = fun r => %record_insert% "x" r 1 in
    │                                         ^ cannot merge this expression
  3 │ (f { x = 0, y = 0 }: _)
    │          ^ with this expression
    │
    ┌─ <stdlib/internals.ncl>:133:9
    │
133 │         acc & tail
    │         ---------- originally merged here
    │
    = Both values have the same merge priority but they can't be combined.
    = Primitive values (Number, String, and Bool) or arrays can be merged only if they are equal.
    = Functions can never be merged.

[yannham]

Same as @vkleen here, I can't reproduce. Both examples are producing static type errors on latest master, although the error message is wrong (@Radvendii I think this is similar to one that you fixed in your PR, what the error thinks is the type of the row is actually the type of the enclosing record type)

[Radvendii]

This is clearer in latest master now that #1323 is merged. Now in one case we get a type error and in the other we get a contract violation.

In the output @vkleen pasted above, notice that this is not a type error; it's a runtime error.

nickel> let f | forall r. { ; r } -> { x : Number; r }
       = fun r => %record_insert% "x" r 1 in
(f { x = 0, y = 0 }: _)
error: non mergeable terms
    ┌─ repl-input-3:2:41
    │
  2 │        = fun r => %record_insert% "x" r 1 in
    │                                         ^ cannot merge this expression
  3 │ (f { x = 0, y = 0 }: _)
    │          ^ with this expression
    │
    ┌─ <stdlib/internals.ncl>:133:9
    │
133 │         acc & tail
    │         ---------- originally merged here
    │
    = Both values have the same merge priority but they can't be combined.
    = Primitive values (Number, String, and Bool) or arrays can be merged only if they are equal.
    = Functions can never be merged.

You can see the error / no error very clearly if you discard the result

 nickel> let f | forall r. { ; r } -> { x : Number; r } = fun r => %record_insert% "x" r 1 in let g = fun x => 'a in g (f { x = 0, y = 0 }: _)
'a

nickel> let f | forall r. { ; r } -> { x : Number; r } = fun r => %record_insert% "x" r 1 in let g = fun x => 'a in g (f { x = 0, a = 0 }: _)
error: multiple rows declaration
  ┌─ repl-input-8:1:114
  │
1 │ let f | forall r. { ; r } -> { x : Number; r } = fun r => %record_insert% "x" r 1 in let g = fun x => 'a in g (f { x = 0, a = 0 }: _)
  │                                                                                                                  ^^^^^^^^^^^^^^^^ this expression
  │
  = Found an expression of a record type with the row `x: { x: _a, a: _b }`
  = But this type appears inside another row type, which already has a declaration for the field `x`
  = A type cannot have two conflicting declarations for the same row

[vkleen]

The thing is, I'm not sure the static typechecker is at fault here. Note that these error messages come from giving f a contract annotation. So it might just be the code in internals.ncl that implements the contract check for polymorphic row types that's screwy.

[yannham]

It seems to be a parsing problem with respect to types annotation. I believe you are just typechecking the record. Putting parentheses do trigger the right error:

 nickel> let f | forall r. { ; r } -> { x : Number; r } = fun r => %record_insert% "x" r 1 in let g = fun x => 'a in g (f { x = 0, y = 0 }: _)
'a

nickel> let f | forall r. { ; r } -> { x : Number; r } = fun r => %record_insert% "x" r 1 in let g = fun x => 'a in g ((f { x = 0, y = 0 }) : _)
error: multiple rows declaration
  ┌─ repl-input-13:1:115
  │
1 │ let f | forall r. { ; r } -> { x : Number; r } = fun r => %record_insert% "x" r 1 in let g = fun x => 'a in g ((f { x = 0, y = 0 }) : _)
  │                                                                                                                   ^^^^^^^^^^^^^^^^ this expression
  │
  = Found an expression of a record type `{ x: _a, y: _b }` with the row `x`
  = But this type appears inside another row type, which already has a declaration for the field `x`
  = A type cannot have two conflicting declarations for the same row

It's still a bug though, : should most probably bind more loosely than function application...

[yannham]

Ok, now this is really strange. If I repeat the same example many times in the REPL, sometimes it works, and sometimes it doesn't... 🤯

[Radvendii]

: binding precedence doesn't explain why it depends on whether we use the identifier y or a, does it?

[yannham]

Nope, the binding precedence was a wrong guess of mine, mistaken by the randomness of the bug. After printing the AST with nickel pprint-ast I confirm that it parses as expected, and the there is a bug in the constraint checker for record rows in the typechecker. Which probably depends on some hashmap being iterated in a certain order, which is often the usual suspect for non-deterministic behavior in Nickel.