Skip to content
  • Simon Peyton Jones's avatar
    Treat equalities with incompatible kinds as "irreducible" constraints · c969cc3d
    Simon Peyton Jones authored
    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
    c969cc3d