Coercion Variable Almost Devoid Checking in ForAllCo
In Richard's thesis Section 5.8.5.2, 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 GRefl
and 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 ForAllCo
.
Trac metadata
Trac field | Value |
---|---|
Version | |
Type | Task |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |