Coercion Variable Almost Devoid Checking in ForAllCo
In Richard's thesis Section 18.104.22.168, there is a restriction on where a coercion variable can appear in
ForAllCo for the sake of consistency: the coercion variable can appear nowhere except in coherence coercions.
Currently this restriction is missing in coercion quantification (see #15497 (closed)). The goal of this ticket is to add the missing restriction.
After discussion with Richard, we restate the restriction a little bit: the coercion variable can appear nowhere except in
Refl. Allowing it to appear in
Refl should not break consistency.
Notice that this also means
liftCoSubst might fail when it lifts a
ForAllTy over a coercion variable to a