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.