Core lint failure when optimizing coercions in branched axioms
The attached code causes the failure.
Core Lint correctly checks branched axioms for internal consistency -- when using branch n of an axiom, we must ensure that no branch m < n can possibly apply, no matter what the instantiation for any type variables in the branch may be. However, the coercion optimizer does not respect this property. It will replace coercions used in axioms with equivalent coercions that do not respect this internal consistency property. Everything works out OK in the end (without -dcore-lint, the file compiles and runs correctly), but we go through an invalid state on the way.
In particular, the TrPushAx rules are to blame.
I'm not sure what the best fix for this is, but it seems to be my job to find it.
Trac metadata
| Trac field | Value |
|---|---|
| Version | 7.7 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture |