Skip to content
Snippets Groups Projects
Commit c969cc3d authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Treat equalities with incompatible kinds as "irreducible" constraints

Originally we had the invariant that CTyEqCan and CFunEqCan have LHS
and RHS with compatible kinds.  This is important because if they have
different kinds, then a substitution using the CTyEqCan can give rise
to an ill-kinded type, which in turn makes typeKind crash, and this
led to Trac #7696.  (The possibility of this happening really only
occurred when we introduced kind polymorphism.)

I thought at first this was going to be really awkward to solve, but
happily it turned out to be easy.  We already have CIrredEvCan
constraints, which are "stuck"; we can't use them and we can't solve
them.  Yet. After some substitution from solving other constraints we
may be able to make progress.

So for equality constraints where the LHS and RHS don't have compatible kinds
(although perhaps not YET compatible, eg k and *, just needing to
unify k := *), we now generate a CIrredEvCan, plus the necessary kind
equality constraint.

This entailed some refactoring of course, but only in TcCanonical.  In
particular, the emitKindConstraint code has gone, in favour of a kind
check in canEqLeaf.  See Note [Equalities with incompatible kinds] in
TcCanonical, and Note [CIrredEvCan constraints] in TcRnTypes
parent 24a0e442
No related branches found
No related tags found
No related merge requests found
Loading
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment