Closed ahubers closed 2 years ago
Right now a recursive instance like
type instance F [a] = F a
will elaborate to
type instance WF_F [a] = F @ a
when it needs to elaborate to
type instance WF_F [a] = WF_F a
Resolved by previous work
Right now a recursive instance like
will elaborate to
when it needs to elaborate to