Coerce format descriptions into representation types

[brendanzab]

Note: This is a draft because I'm not really sure if this is a good idea or not, just thought it was a fun thing to play around with, seeing as it doesn't take much code to implement.

---

This PR adds implicit coercions from format descriptions into their representation types during elaboration, removing the need to explicitly call Repr in most cases. This would almost bring us full circle back to when I was trying to use subtyping in Fathom, but now the subtyping would be kept out of the core language, greatly reducing the confusing complications that resulted from conflating types and format descriptions.

Introducing this style of coercive subtyping during elaboration is also not entirely unheard of either: it is a common addition for elaborators to type theories with Tarski-style universes, which seem to have a connection to our approach to format descriptions.

Drawbacks

By inserting calls to Repr implicitly, people learning Fathom could end up finding it harder to understand the difference between format descriptions and host representation types. Repr might also show up in error messages, and this could also result in confusion if people using Fathom aren't used to being explicit about converting between them. We could try to remove the explicit Repr calls during distillation, but would most likely be an imperfect process and could further exacerbate confusion when they do eventually appear.

Introducing subtyping could also make unification more difficult. I don't think this is too much of an issue for this limited use case, but I still don't fully understand the implications or potential interactions. We also probably want to add more subtyping in the future, for example as a way make refinement types usable (coercing from refined to non-refined terms), so we’ll probably have to deal with this anyway down the line.

Resources

When implementing this, I was inspired a bit by elaboration-zoo/experiments/univ-lifts's coe function.

Todo

• [x] document this feature in the reference

[mikeday]

That looks convenient!

[brendanzab]

Thinking I might merge this - we can always remove it if it’s too confusing.