Jon Sterling on Nostr: The code is kind of specific to my type theory, but the idea is the following: 1. ...

The code is kind of specific to my type theory, but the idea is the following:

1. Usually at the mode shift, you use conversion to check type equality. Here, we do that and stop if it succeeds.

2. If that doesn't succeed, we look at the goal type. If it is a type that has an eta law, then we can just blindly apply an introduction rule, and append the corresponding elimination form to the term we are trying to coerce. We do this recursively.

The goal of an algorithm like this is to support "deep" subtyping through all negative types, without having *actual* subtyping in the core language. Forms of subtyping where this is useful include things like singleton types, extension types, or partially instantiated record types (as in Arend or ML modules, and as in my own depicted experimental code).