Skip to content

Draft: typechecker: Relax the CtEvidence invariant for SpecialPred constraints

Alexis King requested to merge lexi.lambda/ghc:relax-ct-invariant into master

As recently discussed on ghc-devs, the invariant on CtEvidence specified in Note [CtEvidence invariants] is currently incorrect in the case of Concrete# constraints. This MR therefore takes @rae’s advice and relaxes the invariant for special constraints. The details of precisely why extending the invariant to special constraints is wrong is spelled out in a new Note [CtEvidence for special constraints], and a new setCtEvPredTypeSpecial function is used to correctly update the types of Concrete# constraints during canonicalisation.

This MR does not actually result in any observable change in behavior, as the incorrect type placed on Concrete# evidence never actually made it into any desugared programs, so the mistake was invisible. Unfortunately, that also makes it impossible to write any regression tests for this patch. However, new assertions in setCtEvPredType and setCtEvPredTypeSpecial catch incorrect uses when assertions are enabled, which was sufficient to catch an additional incorrect use of setCtEvPredType on Concrete# constraints in zonkCtEvidence, which I otherwise would have missed.

Moreover, regardless of whether the change is currently observable, it is nevertheless the right thing to do. In particular, it may prove more important if/when more types of special constraints are added in the future that might otherwise make the discrepancy observable.

Edited by Alexis King

Merge request reports