motoko icon indicating copy to clipboard operation
motoko copied to clipboard

enhancement: typecheck.ml report subtype errors in context, created using a type zipper

Open crusso opened this issue 4 months ago • 0 comments

I wonder if we could eventually report errors not with a path and a conflict, but in the context of the expect type, something like:

expected (Int, Nat) found (Int, Int) because (Int, Int</:Nat)

expected (Int, { foo: Nat }) found (Int, {}) because (Int, { -foo : Nat })

expected (Int, { #foo }) found (Int, {#foo; #bar}) because (Int, { #foo; +#bar:Nat })

But maybe that is worse... (or too expensive to construct) (edited)

I was thinking the current context (a path) would just be a function from typ -> typ that plugs an error description (encoded as a sentinel type) into a hole in the type and a type pretty printer that uses the sentinel/markers accordingly when printing

crusso avatar Aug 20 '25 09:08 crusso