Suboptimal subtyping relation?

[ecranceMERCE]

In the definition of subtyping adopted in the article, the SubApp rule states that subtyping between $f\ x$ and $f' x'$ can only be discussed when $x = x'$. The implementation follows this definition:

https://github.com/coq-community/trocq/blob/95f083ad0b3bca87324437d835b5957b9bd6a6cd/elpi/annot.elpi#L70-L73

However, this definition seems to introduce suboptimal situations in the presence of constants.

Assume t @ list Type(α) ~ t' :. tR for a given list t containing types. Translating t @ list Type(β) by tR is therefore only authorised if list Type(α) is a subtype of list Type(β). In this case, the SubApp rule asserts that α = β, which is not necessarily true.

Indeed, we have:

tR : listR Type(α) Type(α) Param(α) t t'

which essentially means that for all values A and A' in t and t', Param(α) A A' holds. If α is higher than β, every proof Param(α) A A' can be weakened to Param(β) A A', which means the stronger witness tR at type list Type(α) should be acceptable when expecting a witness at type list Type(β). Therefore, we can state that list Type(α) is actually a subtype of list Type(β), without having α = β.

Are there concrete cases where the translation gets stuck because of this forced equality?

[CohenCyril]

Indeed, this is true for list essentially because we can map the weakening, i.e. list : Type(4,0) -> Type(4,0). This is where Trocq could be used to feed its own subtyping mechanism.