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 |
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information