[commit: ghc] master: Fix a subtle bug in kind-mis-matched equalities (Trac #6068) (dff0e99)
git at git.haskell.org
git at git.haskell.org
Fri Nov 15 12:29:17 UTC 2013
Repository : ssh://git@git.haskell.org/ghc
On branch : master
Link : http://ghc.haskell.org/trac/ghc/changeset/dff0e99d37f3529041bb2bb66ffda1ea22af14e0/ghc
>---------------------------------------------------------------
commit dff0e99d37f3529041bb2bb66ffda1ea22af14e0
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date: Fri Nov 15 11:50:19 2013 +0000
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.
>---------------------------------------------------------------
dff0e99d37f3529041bb2bb66ffda1ea22af14e0
compiler/typecheck/TcCanonical.lhs | 25 ++++++++--------
compiler/typecheck/TcInteract.lhs | 58 +++++++++++++++++++++++++++---------
2 files changed, 56 insertions(+), 27 deletions(-)
diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs
index ad3b13b..8978878 100644
--- a/compiler/typecheck/TcCanonical.lhs
+++ b/compiler/typecheck/TcCanonical.lhs
@@ -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
diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index 2484958..beb8a9e 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -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
More information about the ghc-commits
mailing list