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.