Confusing error messages for named record arguments

[lukaszcz]

Typechecking:

module recordError;

import Stdlib.Prelude open;

type T :=
  mkT {
    x : Nat;
    y : Nat
  };

p : T :=
  mkT {
    x := 0;
    y := 0;
  };

gives the error:

/home/heliax/Documents/progs/juvix/recordError.juvix:15:3: error:
/home/heliax/Documents/progs/juvix/recordError.juvix:15:3:
   |
15 |   };
   |   ^
unexpected '}'
expecting <identifier>

This is about the definition of p. The error should point at the opening { and say that @ is missing.

Carlo was quite confused by this. It's hard to figure out what's wrong if you don't remember you need the @, and even if you do it's easy to miss and be confused, because the error points at the wrong place.

The error changes (but is still confusing) if we remove the final ; inside the record creation.

Typechecking:

module recordError;

import Stdlib.Prelude open;

type T :=
  mkT {
    x : Nat;
    y : Nat
  };

p : T :=
  mkT {
    x := 0;
    y := 0
  };

results in:

/home/heliax/Documents/progs/juvix/recordError.juvix:13:5-11: error:
Unexpected named arguments:
• x := 0