Very nice and interesting work! Congrats to Léo!
The paragraph about “higher-order capabilities” is a bit cryptic for me: is List.map f recognized as an identity as soon as f is? And what about Set.Make(X).map and so on? I think about another approach: instead of requiring to write identity functions between two types t and u, we could allow (e : t :> u) as soon as we can recognize that t and u share the same memory representation (or, more generally, that every value of t has a memory representation that is also valid as a value of u). The benefit of coercion is that it naturally allows deep transformations, and I think that it is what @EduardoRFS suggested in Records, tuples and variants subtyping, but one of the difficulties is perhaps to recognize that the memory representations of t and u are compatible. (We can then mix the approaches by allowing coercions between t and u as soon as we are able to write an identity function between the two types.)
I cannot resist to share a related puzzle… You can check that there should be an identity function ('a, 'b, 'c) plus -> ('a, 'b, 'c) cursor between the types:
type zero = [`Zero] and 'a succ = [`Succ of 'a]
type ('a, 'b, 'c) plus =
| PO : (zero, 'a, 'a) plus
| PS : ('a, 'b, 'c) plus -> ('a succ, 'b, 'c succ) plus
type ('a, 'b, 'c) cursor =
| CO : (zero, 'a, 'a) cursor
| CS : ('a, 'b succ, 'c) cursor -> ('a succ, 'b, 'c) cursor
(You can check for instance that for all n >= 0 and for all types 'a, 'b, 'c, we have PS^n PO : ('a, 'b, 'c) plus if and only if CS^n CO : ('a, 'b, 'c) cursor.)
However, I have found very difficult to write such an identity function that will not be in quadratic time with respect to the size of its argument (I think I have a linear-time implementation, but it is incredibly convoluted, and in retrospect it could even have been a good candidate for https://discuss.ocaml.org/t/share-your-crazy-ocaml-code-snippet/8116: I prefer not to share it right now not to spoil if someone wants to search a bit). I don’t know if there is some functions ('a, 'b, 'c) plus -> ('a, 'b, 'c) cursor for which the approach presented here can prove to be an identity.