Does Idris have or plan to have anything similar to Coercible and type roles, or have you given it any thought?
(I was thinking about the problem of intrinsically typed de Bruijn *levels*, and thought this may be part of the solution... I'm not sure if it would be!)
Conversation
(Or maybe irrelevant forall/exists would be? Or something...)
2
Replying to
I thought irrelevant parameters in Idris 2 would be something like:
(0 x : A) -> B x
(0 x : A ** B x)
Not sure how it relates to Coercible and type roles though... they are new to me. 🤔