unifier error messages appear in the wrong place

[MangoIV]

Hi! The error messages after unifying seem to appear in the wrong place. Simple example:

data A {a}
data B {b}
data C (a : A) {}

let f : C (b) {b}

In this example I expect C to be authoritative and the error to be reported on the type of f, however, the error is on the parameter on C.

this also happens with other errors like T-016 "Cannot automatically decided whether lhs and rhs unify"

[timsueberkrueb]

Hey, thanks for reporting this issue. We do indeed need to improve our error messages; I think there are more examples.

To fix this, the spans supplied to the type errors need to be adjusted. The errors are defined in https://github.com/polarity-lang/polarity/blob/main/lang/elaborator/src/result.rs. From there, one can find all references of individual errors in the codebase.

[MangoIV]

From there, one can find all references of individual errors in the codebase.

it appears that there's just the span field is missing, e.g. when checking
B =? A, the TypCtor for B looks as follows:

TypCtor(TypCtor { span: None, name: Ident { span: Some(Span { start: ByteIndex(16), end: ByteIndex(17) }), id: "B" }, args: Args { args: [] } })

It looks like the span is there but only in name, not in span...

Is this expected? I think this is why it is missing in the error.

[MangoIV]

I have traced back this empty span for TypCtor to very early in the pipeline. I wonder what the idea behind spans being allowed to be empty is; can one have a check on e.g. contained identifiers on spans and return Some span of the nested structure?

[BinderDavid]

I have traced back this empty span for TypCtor to very early in the pipeline. I wonder what the idea behind spans being allowed to be empty is; can one have a check on e.g. contained identifiers on spans and return Some span of the nested structure?

The reason for optional spans are the de/refunctionalization code actions. If a file gets parsed, lowered, typechecked, then all the spans should be Some(span), but when we modify the AST for code actions we set the spans to None.

(I am currently winding down from a week of OOPSLA, but I will have some time in the next few days to take a closer look :) )

Edit: Another reason is elaborated type information: When we annotate some subterm with an inferred type, then that type is represented by an AST, but it does not correspond to some text written by the user.

[timsueberkrueb]

The reason for optional spans are the de/refunctionalization code actions

This, but also syntactic sugar and substitution during elaboration (dependent pattern matching).

[timsueberkrueb]

data A {a}
data B {b}
data C (a : A) {}

let f : C (b) {b}

Okay, so what I think happens in this particular example is the following: In the declaration data B { b }, the constructor b is declared without type. This is allowed because B has no type parameters.

In lowering, we hence infer the type to TypCtor(TypCtor { span: None, name: Ident { span: Some(Span { start: ByteIndex(16), end: ByteIndex(17) }), id: "B" }, args: Args { args: [] } }):

polarity/lang/lowering/src/lower/decls/data_declaration.rs

Line 48 in db9028b

if type_arity == 0 {

This does not have a span simply because it does not occur in the program.

The spans in the ast are correct, but these are probably not the spans we want to use for this error message.

[timsueberkrueb]

For instance, if you change the program to:

data A {a}
data B {b: B} -- annotate the type of b explicitly
data C (a : A) {}

let f : C (b) {b}

The error message changes to:

Error: T-002

  × The following terms are not equal:
  │   1: B
  │   2: A
  │ 
   ╭─[file:///home/tim/Dev/polarity-lang/polarity/examples/foo.pol:1:1]
 1 │ data A {a}
 2 │ data B {b: B}
   ·            ┬
   ·            ╰── Source of (1)
 3 │ data C (a : A) {}
   ·             ┬
   ·             ╰── Source of (2)
 4 │ 
   ╰────

Which is better but it is still missing the information where the error originated from in f.

[MangoIV]

Yeah… it would be good to annotate why it is trying to unify A and B and then put that in the error.

[MangoIV]