experiment: Try pretty-printing a diff when subtyping fails

[Kamirus]

Idea / Specification

type
  [Data = {... b : Text ...}]
 is not compatible with
  [Data = { ... }]

Print both types focusing on incompatible path found during subtype check.
It should print type aliases plus their normalized form.
It should skip most of the compatible fields to focus on the difference, but it should include some of the correct fields to keeps the surrounding (best to keep the 2 surrounding fields from the source, but what if they are sorted?)

[crusso]

Funnily enough, I was thinking of something similar, but instead of representing the context as text, you represent it as a OCaml function of type (hole : typ) -> typ (destination passing style, I guess). When you get to a clash between ty1 and ty2 you would apply the context to pseudo constructor Clash(ty1, ty2) to construct the type containing the clash.

Might produce sucky messages of course and not quite sure what to do about definition (perhaps you just unfold them).

[Kamirus]

Funnily enough, I was thinking of something similar, but instead of representing the context as text, you represent it as a OCaml function of type (hole : typ) -> typ (destination passing style, I guess). When you get to a clash between ty1 and ty2 you would apply the context to pseudo constructor Clash(ty1, ty2) to construct the type containing the clash.

Might produce sucky messages of course and not quite sure what to do about definition (perhaps you just unfold them).

Hm, that would have a single context and two different ty1 and ty2, yes? But with subtyping the context for both could be different, just compatible e.g. Nat in one place and Int in the other. So we probably need to have two contexts.

Anyway, I've tried this idea last week as an improvement for https://linear.app/caffeinelabs/issue/LANG-45/unsupported-additional-field-when-missing-in-both-oldactor-and but now I'm not sure it is better than a RAG entry...