Commit dff0e99d authored by Simon Peyton Jones's avatar Simon Peyton Jones

Fix a subtle bug in kind-mis-matched equalities (Trac #6068)

When we have an equality constraint where the LHS and RHS
have ill-matched kinds, it get turned into a CIrredEvCan
because a CTyEqCan/CFunEqCan are guaranteed kind-compatible.

But that in turn led to a bug because in the constraint
    c  =  (a:k1) ~ (b:k2)
the kind variables k1 and k2 don't show up in tyVarsOfType c.
Why not?  Because it looks like
    (~) k1 (a:k1) (b:k2)
Maybe (~) should have two kind arguments?  That seemed
like too big a change for not (we wait for NoKinds), so
this patch fixes the bug for now.
parent 434d7836
......@@ -381,19 +381,18 @@ canIrred d ev
= do { let ty = ctEvPred ev
; traceTcS "can_pred" (text "IrredPred = " <+> ppr ty)
; (xi,co) <- flatten d FMFullFlatten ev ty -- co :: xi ~ ty
; let no_flattening = xi `eqType` ty
-- We can't use isTcReflCo, because even if the coercion is
-- Refl, the output type might have had a substitution
-- applied to it. For example 'a' might now be 'C b'
; if no_flattening then
continueWith $
CIrredEvCan { cc_ev = ev, cc_loc = d }
else do
{ mb <- rewriteCtFlavor ev xi co
; case mb of
Just new_ev -> canEvNC d new_ev -- Re-classify and try again
Nothing -> return Stop } } -- Found a cached copy
; mb <- rewriteCtFlavor ev xi co
; case mb of {
Nothing -> return Stop ;
Just new_ev ->
do { -- Re-classify, in case flattening has improved its shape
; case classifyPredType (ctEvPred new_ev) of
ClassPred cls tys -> canClassNC d ev cls tys
EqPred ty1 ty2 -> canEqNC d ev ty1 ty2
TuplePred tys -> canTuple d ev tys
IrredPred {} -> continueWith $
CIrredEvCan { cc_ev = new_ev, cc_loc = d } } } }
canHole :: CtLoc -> CtEvidence -> OccName -> TcS StopOrContinue
canHole d ev occ
......
......@@ -770,22 +770,21 @@ kickOutRewritable new_ev new_tv
`andCts` insols_out) }
(tv_eqs_out, tv_eqs_in) = foldVarEnv kick_out_eqs ([], emptyVarEnv) tv_eqs
(feqs_out, feqs_in) = partitionFunEqs kick_out_ct funeqmap
(dicts_out, dicts_in) = partitionDicts kick_out_ct dictmap
(irs_out, irs_in) = partitionBag kick_out_ct irreds
(insols_out, insols_in) = partitionBag kick_out_ct insols
(feqs_out, feqs_in) = partitionFunEqs kick_out_ct funeqmap
(dicts_out, dicts_in) = partitionDicts kick_out_ct dictmap
(irs_out, irs_in) = partitionBag kick_out_irred irreds
(insols_out, insols_in) = partitionBag kick_out_ct insols
-- Kick out even insolubles; see Note [Kick out insolubles]
kick_out_ct inert_ct = new_ev `canRewrite` ctEvidence inert_ct &&
(new_tv `elemVarSet` tyVarsOfCt inert_ct)
-- NB: tyVarsOfCt will return the type
-- variables /and the kind variables/ that are
-- directly visible in the type. Hence we will
-- have exposed all the rewriting we care about
-- to make the most precise kinds visible for
-- matching classes etc. No need to kick out
-- constraints that mention type variables whose
-- kinds could contain this variable!
kick_out_ct :: Ct -> Bool
kick_out_ct ct = new_ev `canRewrite` ctEvidence ct
&& new_tv `elemVarSet` tyVarsOfCt ct
-- See Note [Kicking out inert constraints]
kick_out_irred :: Ct -> Bool
kick_out_irred ct = new_ev `canRewrite` ctEvidence ct
&& new_tv `elemVarSet` closeOverKinds (tyVarsOfCt ct)
-- See Note [Kicking out Irreds]
kick_out_eqs :: EqualCtList -> ([Ct], TyVarEnv EqualCtList)
-> ([Ct], TyVarEnv EqualCtList)
......@@ -810,6 +809,37 @@ kickOutRewritable new_ev new_tv
kick_out_eq other_ct = pprPanic "kick_out_eq" (ppr other_ct)
\end{code}
Note [Kicking out inert constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Given a new (a -> ty) inert, wewant to kick out an existing inert
constraint if
a) the new constraint can rewrite the inert one
b) 'a' is free in the inert constraint (so that it *will*)
rewrite it if we kick it out.
For (b) we use tyVarsOfCt, which returns the type variables /and
the kind variables/ that are directly visible in the type. Hence we
will have exposed all the rewriting we care about to make the most
precise kinds visible for matching classes etc. No need to kick out
constraints that mention type variables whose kinds contain this
variable! (Except see Note [Kicking out Irreds].)
Note [Kicking out Irreds]
~~~~~~~~~~~~~~~~~~~~~~~~~
There is an awkward special case for Irreds. When we have a
kind-mis-matched equality constraint (a:k1) ~ (ty:k2), we turn it into
an Irred (see Note [Equalities with incompatible kinds] in
TcCanonical). So in this case the free kind variables of k1 and k2
are not visible. More precisely, the type looks like
(~) k1 (a:k1) (ty:k2)
because (~) has kind forall k. k -> k -> Constraint. So the constraint
itself is ill-kinded. We can "see" k1 but not k2. That's why we use
closeOverKinds to make sure we see k2.
This is not pretty. Maybe (~) should have kind
(~) :: forall k1 k1. k1 -> k2 -> Constraint
Note [Kick out insolubles]
~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have an insoluble alpha ~ [alpha], which is insoluble
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment