summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
authorSimon Peyton Jones <simonpj@microsoft.com>2012-09-10 10:01:51 +0100
committerSimon Peyton Jones <simonpj@microsoft.com>2012-09-17 13:45:42 +0100
commitd30b9cf45793c9e674463c86345931cbae345e7a (patch)
tree70ebb623cf086c9f4f1026b1996009aa6078e224 /compiler
parent0683258393f8eb3046c08cdb88868fa1467e6fd2 (diff)
downloadhaskell-d30b9cf45793c9e674463c86345931cbae345e7a.tar.gz
Another refactoring of constraints
1. Rejig CtLoc * CtLoc is now *not* parameterised (much simpler) * CtLoc includes the "depth" of the constraint * CtLoc includes the TcLclEnv at the birthplace That gives (a) the SrcSpan, (b) the [ErrCtxt] (c) the [TcIdBinder] * The CtLoc of a constraint is no longer in its CtEvidence * Where we passed 'depth' before, now we pass CtLoc 2. Some significant refactoring in TcErrors * Get rid of cec_extra * Traverse every constraint, so that we can be sure to generate bindings where necessary. (This was really a lurking bug before.) 3. Merge zonking into TcCanonical. This turned out to be almost trivial; just a small change to TcCanonical.flattenTyVar. The nice consequence is that we don't need to zonk a constraint before solving it; instead it gets zonked "on the fly" as it were.
Diffstat (limited to 'compiler')
-rw-r--r--compiler/typecheck/Inst.lhs101
-rw-r--r--compiler/typecheck/TcCanonical.lhs417
-rw-r--r--compiler/typecheck/TcErrors.lhs509
-rw-r--r--compiler/typecheck/TcExpr.lhs2
-rw-r--r--compiler/typecheck/TcInteract.lhs207
-rw-r--r--compiler/typecheck/TcMType.lhs26
-rw-r--r--compiler/typecheck/TcRnMonad.lhs9
-rw-r--r--compiler/typecheck/TcRnTypes.lhs157
-rw-r--r--compiler/typecheck/TcRules.lhs8
-rw-r--r--compiler/typecheck/TcSMonad.lhs90
-rw-r--r--compiler/typecheck/TcSimplify.lhs28
-rw-r--r--compiler/typecheck/TcType.lhs19
-rw-r--r--compiler/typecheck/TcUnify.lhs9
13 files changed, 695 insertions, 887 deletions
diff --git a/compiler/typecheck/Inst.lhs b/compiler/typecheck/Inst.lhs
index 68a53964a3..34118c4ea6 100644
--- a/compiler/typecheck/Inst.lhs
+++ b/compiler/typecheck/Inst.lhs
@@ -30,9 +30,7 @@ module Inst (
tyVarsOfWC, tyVarsOfBag,
tyVarsOfCt, tyVarsOfCts,
- tidyEvVar, tidyCt, tidyGivenLoc,
-
- substEvVar, substImplication, substCt
+ tidyEvVar, tidyCt, tidySkolemInfo
) where
#include "HsVersions.h"
@@ -85,7 +83,7 @@ emitWanted :: CtOrigin -> TcPredType -> TcM EvVar
emitWanted origin pred
= do { loc <- getCtLoc origin
; ev <- newWantedEvVar pred
- ; emitFlat (mkNonCanonical (CtWanted { ctev_wloc = loc, ctev_pred = pred, ctev_evar = ev }))
+ ; emitFlat (mkNonCanonical loc (CtWanted { ctev_pred = pred, ctev_evar = ev }))
; return ev }
newMethodFromName :: CtOrigin -> Name -> TcRhoType -> TcM (HsExpr TcId)
@@ -555,14 +553,13 @@ tidyCt env ct
= case ct of
CHoleCan {} -> ct { cc_ev = tidy_flavor env (cc_ev ct) }
_ -> CNonCanonical { cc_ev = tidy_flavor env (cc_ev ct)
- , cc_depth = cc_depth ct }
+ , cc_loc = cc_loc ct }
where
tidy_flavor :: TidyEnv -> CtEvidence -> CtEvidence
-- NB: we do not tidy the ctev_evtm/var field because we don't
-- show it in error messages
- tidy_flavor env ctev@(CtGiven { ctev_gloc = gloc, ctev_pred = pred })
- = ctev { ctev_gloc = tidyGivenLoc env gloc
- , ctev_pred = tidyType env pred }
+ tidy_flavor env ctev@(CtGiven { ctev_pred = pred })
+ = ctev { ctev_pred = tidyType env pred }
tidy_flavor env ctev@(CtWanted { ctev_pred = pred })
= ctev { ctev_pred = tidyType env pred }
tidy_flavor env ctev@(CtDerived { ctev_pred = pred })
@@ -571,78 +568,26 @@ tidyCt env ct
tidyEvVar :: TidyEnv -> EvVar -> EvVar
tidyEvVar env var = setVarType var (tidyType env (varType var))
-tidyGivenLoc :: TidyEnv -> GivenLoc -> GivenLoc
-tidyGivenLoc env (CtLoc skol lcl)
- = CtLoc (tidySkolemInfo env skol) lcl
-
-tidySkolemInfo :: TidyEnv -> SkolemInfo -> SkolemInfo
-tidySkolemInfo env (SigSkol cx ty) = SigSkol cx (tidyType env ty)
-tidySkolemInfo env (InferSkol ids) = InferSkol (mapSnd (tidyType env) ids)
-tidySkolemInfo env (UnifyForAllSkol skol_tvs ty)
- = UnifyForAllSkol (map tidy_tv skol_tvs) (tidyType env ty)
- where
- tidy_tv tv = case getTyVar_maybe ty' of
- Just tv' -> tv'
- Nothing -> pprPanic "ticySkolemInfo" (ppr tv <+> ppr ty')
- where
- ty' = tidyTyVarOcc env tv
-tidySkolemInfo _ info = info
-
----------------- Substitution -------------------------
--- This is used only in TcSimpify, for substituations that are *also*
--- reflected in the unification variables. So we don't substitute
--- in the evidence.
-
-substCt :: TvSubst -> Ct -> Ct
--- Conservatively converts it to non-canonical:
--- Postcondition: if the constraint does not get rewritten
-substCt subst ct
- | pty <- ctPred ct
- , sty <- substTy subst pty
- = if sty `eqType` pty then
- ct { cc_ev = substFlavor subst (cc_ev ct) }
- else
- CNonCanonical { cc_ev = substFlavor subst (cc_ev ct)
- , cc_depth = cc_depth ct }
-
-substWC :: TvSubst -> WantedConstraints -> WantedConstraints
-substWC subst (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
- = WC { wc_flat = mapBag (substCt subst) flat
- , wc_impl = mapBag (substImplication subst) implic
- , wc_insol = mapBag (substCt subst) insol }
-
-substImplication :: TvSubst -> Implication -> Implication
-substImplication subst implic@(Implic { ic_skols = tvs
- , ic_given = given
- , ic_wanted = wanted
- , ic_loc = loc })
- = implic { ic_skols = tvs'
- , ic_given = map (substEvVar subst1) given
- , ic_wanted = substWC subst1 wanted
- , ic_loc = substGivenLoc subst1 loc }
+tidySkolemInfo :: TidyEnv -> SkolemInfo -> (TidyEnv, SkolemInfo)
+tidySkolemInfo env (SigSkol cx ty)
+ = (env', SigSkol cx ty')
where
- (subst1, tvs') = mapAccumL substTyVarBndr subst tvs
-
-substEvVar :: TvSubst -> EvVar -> EvVar
-substEvVar subst var = setVarType var (substTy subst (varType var))
+ (env', ty') = tidyOpenType env ty
-substFlavor :: TvSubst -> CtEvidence -> CtEvidence
-substFlavor subst ctev@(CtGiven { ctev_gloc = gloc, ctev_pred = pred })
- = ctev { ctev_gloc = substGivenLoc subst gloc
- , ctev_pred = substTy subst pred }
-
-substFlavor subst ctev@(CtWanted { ctev_pred = pred })
- = ctev { ctev_pred = substTy subst pred }
-
-substFlavor subst ctev@(CtDerived { ctev_pred = pty })
- = ctev { ctev_pred = substTy subst pty }
+tidySkolemInfo env (InferSkol ids)
+ = (env', InferSkol ids')
+ where
+ (env', ids') = mapAccumL do_one env ids
+ do_one env (name, ty) = (env', (name, ty'))
+ where
+ (env', ty') = tidyOpenType env ty
-substGivenLoc :: TvSubst -> GivenLoc -> GivenLoc
-substGivenLoc subst (CtLoc skol lcl)
- = CtLoc (substSkolemInfo subst skol) lcl
+tidySkolemInfo env (UnifyForAllSkol skol_tvs ty)
+ = (env1, UnifyForAllSkol skol_tvs' ty')
+ where
+ env1 = tidyFreeTyVars env (tyVarsOfType ty `delVarSetList` skol_tvs)
+ (env2, skol_tvs') = tidyTyVarBndrs env1 skol_tvs
+ ty' = tidyType env2 ty
-substSkolemInfo :: TvSubst -> SkolemInfo -> SkolemInfo
-substSkolemInfo subst (SigSkol cx ty) = SigSkol cx (substTy subst ty)
-substSkolemInfo subst (InferSkol ids) = InferSkol (mapSnd (substTy subst) ids)
-substSkolemInfo _ info = info
+tidySkolemInfo env info = (env, info)
\end{code}
diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs
index db26b7a94b..d972e2ea85 100644
--- a/compiler/typecheck/TcCanonical.lhs
+++ b/compiler/typecheck/TcCanonical.lhs
@@ -165,50 +165,48 @@ EvBinds, so we are again good.
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
canonicalize :: Ct -> TcS StopOrContinue
-canonicalize ct@(CNonCanonical { cc_ev = fl, cc_depth = d })
+canonicalize ct@(CNonCanonical { cc_ev = ev, cc_loc = d })
= do { traceTcS "canonicalize (non-canonical)" (ppr ct)
; {-# SCC "canEvVar" #-}
- canEvNC d fl }
+ canEvNC d ev }
-canonicalize (CDictCan { cc_depth = d
- , cc_ev = fl
+canonicalize (CDictCan { cc_loc = d
+ , cc_ev = ev
, cc_class = cls
, cc_tyargs = xis })
= {-# SCC "canClass" #-}
- canClass d fl cls xis -- Do not add any superclasses
-canonicalize (CTyEqCan { cc_depth = d
- , cc_ev = fl
+ canClass d ev cls xis -- Do not add any superclasses
+canonicalize (CTyEqCan { cc_loc = d
+ , cc_ev = ev
, cc_tyvar = tv
, cc_rhs = xi })
= {-# SCC "canEqLeafTyVarLeftRec" #-}
- canEqLeafTyVarLeftRec d fl tv xi
+ canEqLeafTyVarLeftRec d ev tv xi
-canonicalize (CFunEqCan { cc_depth = d
- , cc_ev = fl
+canonicalize (CFunEqCan { cc_loc = d
+ , cc_ev = ev
, cc_fun = fn
, cc_tyargs = xis1
, cc_rhs = xi2 })
= {-# SCC "canEqLeafFunEq" #-}
- canEqLeafFunEq d fl (fn,xis1) xi2
+ canEqLeafFunEq d ev (fn,xis1) xi2
-canonicalize (CIrredEvCan { cc_ev = fl
- , cc_depth = d
+canonicalize (CIrredEvCan { cc_ev = ev
+ , cc_loc = d
, cc_ty = xi })
- = canIrred d fl xi
+ = canIrred d ev xi
canonicalize ct@(CHoleCan {})
= do { emitInsoluble ct
; return Stop }
-canEvNC :: SubGoalDepth
- -> CtEvidence
- -> TcS StopOrContinue
+canEvNC :: CtLoc -> CtEvidence -> TcS StopOrContinue
-- Called only for non-canonical EvVars
-canEvNC d fl
- = case classifyPredType (ctEvPred fl) of
- ClassPred cls tys -> canClassNC d fl cls tys
- EqPred ty1 ty2 -> canEqNC d fl ty1 ty2
- IrredPred ev_ty -> canIrred d fl ev_ty
- TuplePred tys -> canTuple d fl tys
+canEvNC d ev
+ = case classifyPredType (ctEvPred ev) of
+ ClassPred cls tys -> canClassNC d ev cls tys
+ EqPred ty1 ty2 -> canEqNC d ev ty1 ty2
+ IrredPred ev_ty -> canIrred d ev ev_ty
+ TuplePred tys -> canTuple d ev tys
\end{code}
@@ -219,13 +217,12 @@ canEvNC d fl
%************************************************************************
\begin{code}
-canTuple :: SubGoalDepth -- Depth
- -> CtEvidence -> [PredType] -> TcS StopOrContinue
-canTuple d fl tys
+canTuple :: CtLoc -> CtEvidence -> [PredType] -> TcS StopOrContinue
+canTuple d ev tys
= do { traceTcS "can_pred" (text "TuplePred!")
; let xcomp = EvTupleMk
xdecomp x = zipWith (\_ i -> EvTupleSel x i) tys [0..]
- ; ctevs <- xCtFlavor fl tys (XEvTerm xcomp xdecomp)
+ ; ctevs <- xCtFlavor ev tys (XEvTerm xcomp xdecomp)
; canEvVarsCreated d ctevs }
\end{code}
@@ -237,7 +234,7 @@ canTuple d fl tys
\begin{code}
canClass, canClassNC
- :: SubGoalDepth -- Depth
+ :: CtLoc
-> CtEvidence
-> Class -> [Type] -> TcS StopOrContinue
-- Precondition: EvVar is class evidence
@@ -247,32 +244,32 @@ canClass, canClassNC
-- for already-canonical class constraints (but which might have
-- been subsituted or somthing), and hence do not need superclasses
-canClassNC d fl cls tys
- = canClass d fl cls tys
+canClassNC d ev cls tys
+ = canClass d ev cls tys
`andWhenContinue` emitSuperclasses
-canClass d fl cls tys
+canClass d ev cls tys
= do { -- sctx <- getTcSContext
- ; (xis, cos) <- flattenMany d FMFullFlatten fl tys
+ ; (xis, cos) <- flattenMany d FMFullFlatten ev tys
; let co = mkTcTyConAppCo (classTyCon cls) cos
xi = mkClassPred cls xis
- ; mb <- rewriteCtFlavor fl xi co
+ ; mb <- rewriteCtFlavor ev xi co
; case mb of
- Just new_fl ->
- let (ClassPred cls xis_for_dict) = classifyPredType (ctEvPred new_fl)
+ Just new_ev ->
+ let (ClassPred cls xis_for_dict) = classifyPredType (ctEvPred new_ev)
in continueWith $
- CDictCan { cc_ev = new_fl
- , cc_tyargs = xis_for_dict, cc_class = cls, cc_depth = d }
+ CDictCan { cc_ev = new_ev, cc_loc = d
+ , cc_tyargs = xis_for_dict, cc_class = cls }
Nothing -> return Stop }
emitSuperclasses :: Ct -> TcS StopOrContinue
-emitSuperclasses ct@(CDictCan { cc_depth = d, cc_ev = fl
+emitSuperclasses ct@(CDictCan { cc_loc = d, cc_ev = ev
, cc_tyargs = xis_new, cc_class = cls })
-- Add superclasses of this one here, See Note [Adding superclasses].
-- But only if we are not simplifying the LHS of a rule.
- = do { newSCWorkFromFlavored d fl cls xis_new
+ = do { newSCWorkFromFlavored d ev cls xis_new
-- Arguably we should "seq" the coercions if they are derived,
-- as we do below for emit_kind_constraint, to allow errors in
-- superclasses to be executed if deferred to runtime!
@@ -344,8 +341,7 @@ By adding superclasses definitely only once, during canonicalisation, this situa
happen.
\begin{code}
-
-newSCWorkFromFlavored :: SubGoalDepth -- Depth
+newSCWorkFromFlavored :: CtLoc -- Depth
-> CtEvidence -> Class -> [Xi] -> TcS ()
-- Returns superclasses, see Note [Adding superclasses]
newSCWorkFromFlavored d flavor cls xis
@@ -369,7 +365,7 @@ newSCWorkFromFlavored d flavor cls xis
= do { let sc_rec_theta = transSuperClasses cls xis
impr_theta = filter is_improvement_pty sc_rec_theta
; traceTcS "newSCWork/Derived" $ text "impr_theta =" <+> ppr impr_theta
- ; mb_der_evs <- mapM (newDerived (ctev_wloc flavor)) impr_theta
+ ; mb_der_evs <- mapM newDerived impr_theta
; emitWorkNC d (catMaybes mb_der_evs) }
is_improvement_pty :: PredType -> Bool
@@ -392,24 +388,23 @@ is_improvement_pty ty = go (classifyPredType ty)
\begin{code}
-canIrred :: SubGoalDepth -- Depth
- -> CtEvidence -> TcType -> TcS StopOrContinue
+canIrred :: CtLoc -> CtEvidence -> TcType -> TcS StopOrContinue
-- Precondition: ty not a tuple and no other evidence form
-canIrred d fl ty
+canIrred d ev ty
= do { traceTcS "can_pred" (text "IrredPred = " <+> ppr ty)
- ; (xi,co) <- flatten d FMFullFlatten fl ty -- co :: xi ~ ty
+ ; (xi,co) <- flatten d FMFullFlatten ev ty -- co :: xi ~ ty
; let no_flattening = xi `eqType` ty
-- In this particular case it is not safe to
-- say 'isTcReflCo' because the new constraint may
-- be reducible!
- ; mb <- rewriteCtFlavor fl xi co
+ ; mb <- rewriteCtFlavor ev xi co
; case mb of
- Just new_fl
+ Just new_ev
| no_flattening
-> continueWith $
- CIrredEvCan { cc_ev = new_fl, cc_ty = xi, cc_depth = d }
+ CIrredEvCan { cc_ev = new_ev, cc_ty = xi, cc_loc = d }
| otherwise
- -> canEvNC d new_fl
+ -> canEvNC d new_ev
Nothing -> return Stop }
\end{code}
@@ -465,8 +460,7 @@ data FlattenMode = FMSubstOnly
| FMFullFlatten
-- Flatten a bunch of types all at once.
-flattenMany :: SubGoalDepth -- Depth
- -> FlattenMode
+flattenMany :: CtLoc -> FlattenMode
-> CtEvidence -> [Type] -> TcS ([Xi], [TcCoercion])
-- Coercions :: Xi ~ Type
-- Returns True iff (no flattening happened)
@@ -484,36 +478,35 @@ flattenMany d f ctxt tys
-- Flatten a type to get rid of type function applications, returning
-- the new type-function-free type, and a collection of new equality
-- constraints. See Note [Flattening] for more detail.
-flatten :: SubGoalDepth -- Depth
- -> FlattenMode
+flatten :: CtLoc -> FlattenMode
-> CtEvidence -> TcType -> TcS (Xi, TcCoercion)
-- Postcondition: Coercion :: Xi ~ TcType
-flatten d f ctxt ty
+flatten loc f ctxt ty
| Just ty' <- tcView ty
- = do { (xi, co) <- flatten d f ctxt ty'
+ = do { (xi, co) <- flatten loc f ctxt ty'
; if eqType xi ty then return (ty,co) else return (xi,co) }
-- Small tweak for better error messages
flatten _ _ _ xi@(LitTy {}) = return (xi, mkTcReflCo xi)
-flatten d f ctxt (TyVarTy tv)
- = flattenTyVar d f ctxt tv
+flatten loc f ctxt (TyVarTy tv)
+ = flattenTyVar loc f ctxt tv
-flatten d f ctxt (AppTy ty1 ty2)
- = do { (xi1,co1) <- flatten d f ctxt ty1
- ; (xi2,co2) <- flatten d f ctxt ty2
+flatten loc f ctxt (AppTy ty1 ty2)
+ = do { (xi1,co1) <- flatten loc f ctxt ty1
+ ; (xi2,co2) <- flatten loc f ctxt ty2
; return (mkAppTy xi1 xi2, mkTcAppCo co1 co2) }
-flatten d f ctxt (FunTy ty1 ty2)
- = do { (xi1,co1) <- flatten d f ctxt ty1
- ; (xi2,co2) <- flatten d f ctxt ty2
+flatten loc f ctxt (FunTy ty1 ty2)
+ = do { (xi1,co1) <- flatten loc f ctxt ty1
+ ; (xi2,co2) <- flatten loc f ctxt ty2
; return (mkFunTy xi1 xi2, mkTcFunCo co1 co2) }
-flatten d f ctxt (TyConApp tc tys)
+flatten loc f ctxt (TyConApp tc tys)
-- For a normal type constructor or data family application, we just
-- recursively flatten the arguments.
| not (isSynFamilyTyCon tc)
- = do { (xis,cos) <- flattenMany d f ctxt tys
+ = do { (xis,cos) <- flattenMany loc f ctxt tys
; return (mkTyConApp tc xis, mkTcTyConAppCo tc cos) }
-- Otherwise, it's a type function application, and we have to
@@ -521,7 +514,7 @@ flatten d f ctxt (TyConApp tc tys)
-- between the application and a newly generated flattening skolem variable.
| otherwise
= ASSERT( tyConArity tc <= length tys ) -- Type functions are saturated
- do { (xis, cos) <- flattenMany d f ctxt tys
+ do { (xis, cos) <- flattenMany loc f ctxt tys
; let (xi_args, xi_rest) = splitAt (tyConArity tc) xis
(cos_args, cos_rest) = splitAt (tyConArity tc) cos
-- The type function might be *over* saturated
@@ -549,7 +542,7 @@ flatten d f ctxt (TyConApp tc tys)
-- For now I say we don't keep it fully rewritten.
do { traceTcS "flatten/flat-cache hit" $ ppr ct
; let rhs_xi = cc_rhs ct
- ; (flat_rhs_xi,co) <- flatten (cc_depth ct) f ctev rhs_xi
+ ; (flat_rhs_xi,co) <- flatten (cc_loc ct) f ctev rhs_xi
; let final_co = evTermCoercion (ctEvTerm ctev)
`mkTcTransCo` mkTcSymCo co
; return (final_co, flat_rhs_xi) }
@@ -558,14 +551,13 @@ flatten d f ctxt (TyConApp tc tys)
-> do { traceTcS "flatten/flat-cache miss" $ empty
; rhs_ty <- newFlattenSkolemTy fam_ty
; let co = mkTcReflCo fam_ty
- new_fl = CtGiven { ctev_gloc = ctev_gloc ctxt
- , ctev_pred = mkTcEqPred fam_ty rhs_ty
+ new_ev = CtGiven { ctev_pred = mkTcEqPred fam_ty rhs_ty
, ctev_evtm = EvCoercion co }
- ct = CFunEqCan { cc_ev = new_fl
+ ct = CFunEqCan { cc_ev = new_ev
, cc_fun = tc
, cc_tyargs = xi_args
, cc_rhs = rhs_ty
- , cc_depth = d }
+ , cc_loc = loc }
; updWorkListTcS $ extendWorkListEq ct
; return (co, rhs_ty) }
@@ -573,15 +565,14 @@ flatten d f ctxt (TyConApp tc tys)
-> do { traceTcS "flatten/flat-cache miss" $ empty
; rhs_xi_var <- newFlexiTcSTy (typeKind fam_ty)
; let pred = mkTcEqPred fam_ty rhs_xi_var
- wloc = ctev_wloc ctxt
- ; mw <- newWantedEvVar wloc pred
+ ; mw <- newWantedEvVar pred
; case mw of
Fresh ctev ->
do { let ct = CFunEqCan { cc_ev = ctev
, cc_fun = tc
, cc_tyargs = xi_args
, cc_rhs = rhs_xi_var
- , cc_depth = d }
+ , cc_loc = loc }
; updWorkListTcS $ extendWorkListEq ct
; return (evTermCoercion (ctEvTerm ctev), rhs_xi_var) }
Cached {} -> panic "flatten TyConApp, var must be fresh!" }
@@ -594,11 +585,11 @@ flatten d f ctxt (TyConApp tc tys)
)
}
-flatten d _f ctxt ty@(ForAllTy {})
+flatten loc _f ctxt ty@(ForAllTy {})
-- We allow for-alls when, but only when, no type function
-- applications inside the forall involve the bound type variables.
= do { let (tvs, rho) = splitForAllTys ty
- ; (rho', co) <- flatten d FMSubstOnly ctxt rho
+ ; (rho', co) <- flatten loc FMSubstOnly ctxt rho
-- Substitute only under a forall
-- See Note [Flattening under a forall]
; return (mkForAllTys tvs rho', foldr mkTcForAllCo co tvs) }
@@ -622,40 +613,48 @@ because now the 'b' has escaped its scope. We'd have to flatten to
and we have not begun to think about how to make that work!
\begin{code}
-flattenTyVar :: SubGoalDepth
- -> FlattenMode
+flattenTyVar :: CtLoc -> FlattenMode
-> CtEvidence -> TcTyVar -> TcS (Xi, TcCoercion)
-- "Flattening" a type variable means to apply the substitution to it
-- The substitution is actually the union of the substitution in the TyBinds
-- for the unification variables that have been unified already with the inert
-- equalities, see Note [Spontaneously solved in TyBinds] in TcInteract.
-flattenTyVar d f ctxt tv
- = do { ty_binds <- getTcSTyBindsMap
- ; case lookupVarEnv ty_binds tv of
- Nothing -> flatten_from_inerts
- Just (_tv,ty) -> -- Recurse
- do { (ty_final,co') <- flatten d f ctxt ty
- ; return (ty_final, co') } }
- -- NB: ty_binds coercions are all ReflCo,
- -- so no need to transitively compose co' with another coercion,
- -- unlike in 'flatten_from_inerts'
+flattenTyVar loc f ctxt tv
+ = do { mb_ty <- isFilledMetaTyVar_maybe tv
+ ; case mb_ty of {
+ Just ty -> flatten loc f ctxt ty ;
+ Nothing ->
+
+ -- Try in ty_binds
+ do { ty_binds <- getTcSTyBindsMap
+ ; case lookupVarEnv ty_binds tv of {
+ Just (_tv,ty) -> flatten loc f ctxt ty ;
+ -- NB: ty_binds coercions are all ReflCo,
+ -- so no need to transitively compose co' with another coercion,
+ -- unlike in 'flatten_from_inerts'
+ Nothing ->
+
+ -- Try in the inert equalities
+ do { ieqs <- getInertEqs
+ ; let mco = tv_eq_subst ieqs tv -- co : v ~ ty
+ ; case mco of {
+ Just (co,ty) ->
+ do { (ty_final,co') <- flatten loc f ctxt ty
+ ; return (ty_final, co' `mkTcTransCo` mkTcSymCo co) } ;
+ -- NB recursive call.
+ -- Why? Because inert subst. non-idempotent, Note [Detailed InertCans Invariants]
+ -- In fact, because of flavors, it couldn't possibly be idempotent,
+ -- this is explained in Note [Non-idempotent inert substitution]
+
+ Nothing ->
+
+ -- Done, but make sure the kind is zonked
+ do { let knd = tyVarKind tv
+ ; (new_knd,_kind_co) <- flatten loc f ctxt knd
+ ; let ty = mkTyVarTy (setVarType tv new_knd)
+ ; return (ty, mkTcReflCo ty) }
+ } } } } } }
where
- flatten_from_inerts
- = do { ieqs <- getInertEqs
- ; let mco = tv_eq_subst ieqs tv -- co : v ~ ty
- ; case mco of -- Done, but make sure the kind is zonked
- Nothing ->
- do { let knd = tyVarKind tv
- ; (new_knd,_kind_co) <- flatten d f ctxt knd
- ; let ty = mkTyVarTy (setVarType tv new_knd)
- ; return (ty, mkTcReflCo ty) }
- -- NB recursive call.
- -- Why? Because inert subst. non-idempotent, Note [Detailed InertCans Invariants]
- -- In fact, because of flavors, it couldn't possibly be idempotent,
- -- this is explained in Note [Non-idempotent inert substitution]
- Just (co,ty) ->
- do { (ty_final,co') <- flatten d f ctxt ty
- ; return (ty_final, co' `mkTcTransCo` mkTcSymCo co) } }
tv_eq_subst subst tv
| Just ct <- lookupVarEnv subst tv
, let ctev = cc_ev ct
@@ -702,108 +701,106 @@ Insufficient (non-recursive) rewriting was the reason for #5668.
%************************************************************************
\begin{code}
-canEvVarsCreated :: SubGoalDepth -> [CtEvidence] -> TcS StopOrContinue
-canEvVarsCreated _d [] = return Stop
+canEvVarsCreated :: CtLoc -> [CtEvidence] -> TcS StopOrContinue
+canEvVarsCreated _loc [] = return Stop
-- Add all but one to the work list
-- and return the first (if any) for futher processing
-canEvVarsCreated d (ev : evs)
- = do { emitWorkNC d evs; canEvNC d ev }
+canEvVarsCreated loc (ev : evs)
+ = do { emitWorkNC loc evs; canEvNC loc ev }
-- Note the "NC": these are fresh goals, not necessarily canonical
-emitWorkNC :: SubGoalDepth -> [CtEvidence] -> TcS ()
-emitWorkNC depth evs
+emitWorkNC :: CtLoc -> [CtEvidence] -> TcS ()
+emitWorkNC loc evs
| null evs = return ()
| otherwise = updWorkListTcS (extendWorkListCts (map mk_nc evs))
where
- mk_nc ev = CNonCanonical { cc_ev = ev, cc_depth = depth }
+ mk_nc ev = CNonCanonical { cc_ev = ev, cc_loc = loc }
-------------------------
canEqNC, canEq
- :: SubGoalDepth
- -> CtEvidence
+ :: CtLoc -> CtEvidence
-> Type -> Type -> TcS StopOrContinue
-canEqNC d fl ty1 ty2
- = canEq d fl ty1 ty2
+canEqNC loc ev ty1 ty2
+ = canEq loc ev ty1 ty2
`andWhenContinue` emitKindConstraint
-canEq _d fl ty1 ty2
+canEq _loc ev ty1 ty2
| eqType ty1 ty2 -- Dealing with equality here avoids
-- later spurious occurs checks for a~a
- = if isWanted fl then
- setEvBind (ctev_evar fl) (EvCoercion (mkTcReflCo ty1)) >> return Stop
+ = if isWanted ev then
+ setEvBind (ctev_evar ev) (EvCoercion (mkTcReflCo ty1)) >> return Stop
else
return Stop
-- If one side is a variable, orient and flatten,
-- WITHOUT expanding type synonyms, so that we tend to
-- substitute a ~ Age rather than a ~ Int when @type Age = Int@
-canEq d fl ty1@(TyVarTy {}) ty2
- = canEqLeaf d fl ty1 ty2
-canEq d fl ty1 ty2@(TyVarTy {})
- = canEqLeaf d fl ty1 ty2
+canEq loc ev ty1@(TyVarTy {}) ty2
+ = canEqLeaf loc ev ty1 ty2
+canEq loc ev ty1 ty2@(TyVarTy {})
+ = canEqLeaf loc ev ty1 ty2
-- See Note [Naked given applications]
-canEq d fl ty1 ty2
- | Just ty1' <- tcView ty1 = canEq d fl ty1' ty2
- | Just ty2' <- tcView ty2 = canEq d fl ty1 ty2'
+canEq loc ev ty1 ty2
+ | Just ty1' <- tcView ty1 = canEq loc ev ty1' ty2
+ | Just ty2' <- tcView ty2 = canEq loc ev ty1 ty2'
-canEq d fl ty1@(TyConApp fn tys) ty2
+canEq loc ev ty1@(TyConApp fn tys) ty2
| isSynFamilyTyCon fn, length tys == tyConArity fn
- = canEqLeaf d fl ty1 ty2
-canEq d fl ty1 ty2@(TyConApp fn tys)
+ = canEqLeaf loc ev ty1 ty2
+canEq loc ev ty1 ty2@(TyConApp fn tys)
| isSynFamilyTyCon fn, length tys == tyConArity fn
- = canEqLeaf d fl ty1 ty2
+ = canEqLeaf loc ev ty1 ty2
-canEq d fl ty1 ty2
+canEq loc ev ty1 ty2
| Just (tc1,tys1) <- tcSplitTyConApp_maybe ty1
, Just (tc2,tys2) <- tcSplitTyConApp_maybe ty2
, isDecomposableTyCon tc1 && isDecomposableTyCon tc2
= -- Generate equalities for each of the corresponding arguments
if (tc1 /= tc2 || length tys1 /= length tys2)
-- Fail straight away for better error messages
- then canEqFailure d fl
+ then canEqFailure loc ev
else
do { let xcomp xs = EvCoercion (mkTcTyConAppCo tc1 (map evTermCoercion xs))
xdecomp x = zipWith (\_ i -> EvCoercion $ mkTcNthCo i (evTermCoercion x)) tys1 [0..]
xev = XEvTerm xcomp xdecomp
- ; ctevs <- xCtFlavor fl (zipWith mkTcEqPred tys1 tys2) xev
- ; canEvVarsCreated d ctevs }
+ ; ctevs <- xCtFlavor ev (zipWith mkTcEqPred tys1 tys2) xev
+ ; canEvVarsCreated loc ctevs }
-- See Note [Equality between type applications]
-- Note [Care with type applications] in TcUnify
-canEq d fl ty1 ty2 -- e.g. F a b ~ Maybe c
+canEq loc ev ty1 ty2 -- e.g. F a b ~ Maybe c
-- where F has arity 1
| Just (s1,t1) <- tcSplitAppTy_maybe ty1
, Just (s2,t2) <- tcSplitAppTy_maybe ty2
- = canEqAppTy d fl s1 t1 s2 t2
+ = canEqAppTy loc ev s1 t1 s2 t2
-canEq d fl s1@(ForAllTy {}) s2@(ForAllTy {})
+canEq loc ev s1@(ForAllTy {}) s2@(ForAllTy {})
| tcIsForAllTy s1, tcIsForAllTy s2
- , CtWanted { ctev_wloc = loc, ctev_evar = orig_ev } <- fl
+ , CtWanted { ctev_evar = orig_ev } <- ev
= do { let (tvs1,body1) = tcSplitForAllTys s1
(tvs2,body2) = tcSplitForAllTys s2
; if not (equalLength tvs1 tvs2) then
- canEqFailure d fl
+ canEqFailure loc ev
else
- do { traceTcS "Creating implication for polytype equality" $ ppr fl
+ do { traceTcS "Creating implication for polytype equality" $ ppr ev
; deferTcSForAllEq (loc,orig_ev) (tvs1,body1) (tvs2,body2)
; return Stop } }
| otherwise
= do { traceTcS "Ommitting decomposition of given polytype equality" $
pprEq s1 s2 -- See Note [Do not decompose given polytype equalities]
; return Stop }
-canEq d fl _ _ = canEqFailure d fl
+canEq loc ev _ _ = canEqFailure loc ev
------------------------
-- Type application
-canEqAppTy :: SubGoalDepth
- -> CtEvidence
+canEqAppTy :: CtLoc -> CtEvidence
-> Type -> Type -> Type -> Type
-> TcS StopOrContinue
-canEqAppTy d fl s1 t1 s2 t2
+canEqAppTy loc ev s1 t1 s2 t2
= ASSERT( not (isKind t1) && not (isKind t2) )
- if isGiven fl then
+ if isGiven ev then
do { traceTcS "canEq (app case)" $
text "Ommitting decomposition of given equality between: "
<+> ppr (AppTy s1 t1) <+> text "and" <+> ppr (AppTy s2 t2)
@@ -815,41 +812,41 @@ canEqAppTy d fl s1 t1 s2 t2
xevcomp _ = error "canEqAppTy: can't happen" -- Can't happen
xev = XEvTerm { ev_comp = xevcomp
, ev_decomp = error "canEqAppTy: can't happen" }
- ; ctevs <- xCtFlavor fl [mkTcEqPred s1 s2, mkTcEqPred t1 t2] xev
- ; canEvVarsCreated d ctevs }
+ ; ctevs <- xCtFlavor ev [mkTcEqPred s1 s2, mkTcEqPred t1 t2] xev
+ ; canEvVarsCreated loc ctevs }
-canEqFailure :: SubGoalDepth -> CtEvidence -> TcS StopOrContinue
-canEqFailure d fl
- = do { emitInsoluble (CNonCanonical { cc_ev = fl, cc_depth = d })
+canEqFailure :: CtLoc -> CtEvidence -> TcS StopOrContinue
+canEqFailure loc ev
+ = do { emitInsoluble (CNonCanonical { cc_ev = ev, cc_loc = loc })
; return Stop }
------------------------
emitKindConstraint :: Ct -> TcS StopOrContinue
emitKindConstraint ct -- By now ct is canonical
= case ct of
- CTyEqCan { cc_depth = d
- , cc_ev = fl, cc_tyvar = tv
+ CTyEqCan { cc_loc = loc
+ , cc_ev = ev, cc_tyvar = tv
, cc_rhs = ty }
- -> emit_kind_constraint d fl (mkTyVarTy tv) ty
+ -> emit_kind_constraint loc ev (mkTyVarTy tv) ty
- CFunEqCan { cc_depth = d
- , cc_ev = fl
+ CFunEqCan { cc_loc = loc
+ , cc_ev = ev
, cc_fun = fn, cc_tyargs = xis1
, cc_rhs = xi2 }
- -> emit_kind_constraint d fl (mkTyConApp fn xis1) xi2
+ -> emit_kind_constraint loc ev (mkTyConApp fn xis1) xi2
_ -> continueWith ct
where
- emit_kind_constraint d fl ty1 ty2
+ emit_kind_constraint loc ev ty1 ty2
| compatKind k1 k2 -- True when ty1,ty2 are themselves kinds,
= continueWith ct -- because then k1, k2 are BOX
| otherwise
= ASSERT( isKind k1 && isKind k2 )
- do { mw <- newWantedEvVar kind_co_wloc (mkEqPred k1 k2)
+ do { mw <- newWantedEvVar (mkEqPred k1 k2)
; kev_tm <- case mw of
Cached ev_tm -> return ev_tm
- Fresh kev -> do { emitWorkNC d [kev]
+ Fresh kev -> do { emitWorkNC kind_co_loc [kev]
; return (ctEvTerm kev) }
; let xcomp [x] = mkEvKindCast x (evTermCoercion kev_tm)
@@ -857,7 +854,7 @@ emitKindConstraint ct -- By now ct is canonical
xdecomp x = [mkEvKindCast x (evTermCoercion kev_tm)]
xev = XEvTerm xcomp xdecomp
- ; ctevs <- xCtFlavor fl [mkTcEqPred ty1 ty2] xev
+ ; ctevs <- xCtFlavor ev [mkTcEqPred ty1 ty2] xev
-- Important: Do not cache original as Solved since we are supposed to
-- solve /exactly/ the same constraint later! Example:
-- (alpha :: kappa0)
@@ -880,12 +877,7 @@ emitKindConstraint ct -- By now ct is canonical
-- Always create a Wanted kind equality even if
-- you are decomposing a given constraint.
-- NB: DV finds this reasonable for now. Maybe we have to revisit.
- kind_co_wloc = pushErrCtxtSameOrigin ctxt wanted_loc
- wanted_loc = case fl of
- CtWanted { ctev_wloc = wloc } -> wloc
- CtDerived { ctev_wloc = wloc } -> wloc
- CtGiven { ctev_gloc = gloc } -> setCtLocOrigin gloc orig
- orig = TypeEqOrigin (UnifyOrigin ty1 ty2)
+ kind_co_loc = pushErrCtxtSameOrigin ctxt loc
\end{code}
Note [Do not decompose given polytype equalities]
@@ -1062,28 +1054,27 @@ reOrient :: CtEvidence -> TypeClassifier -> TypeClassifier -> Bool
-- We try to say False if possible, to minimise evidence generation
--
-- Postcondition: After re-orienting, first arg is not OTherCls
-reOrient _fl (OtherCls {}) (FunCls {}) = True
-reOrient _fl (OtherCls {}) (VarCls {}) = True
-reOrient _fl (OtherCls {}) (OtherCls {}) = panic "reOrient" -- One must be Var/Fun
+reOrient _ev (OtherCls {}) (FunCls {}) = True
+reOrient _ev (OtherCls {}) (VarCls {}) = True
+reOrient _ev (OtherCls {}) (OtherCls {}) = panic "reOrient" -- One must be Var/Fun
-reOrient _fl (FunCls {}) (VarCls _tv) = False
- -- But consider the following variation: isGiven fl && isMetaTyVar tv
+reOrient _ev (FunCls {}) (VarCls _tv) = False
+ -- But consider the following variation: isGiven ev && isMetaTyVar tv
-- See Note [No touchables as FunEq RHS] in TcSMonad
-reOrient _fl (FunCls {}) _ = False -- Fun/Other on rhs
+reOrient _ev (FunCls {}) _ = False -- Fun/Other on rhs
-reOrient _fl (VarCls {}) (FunCls {}) = True
-reOrient _fl (VarCls {}) (OtherCls {}) = False
+reOrient _ev (VarCls {}) (FunCls {}) = True
+reOrient _ev (VarCls {}) (OtherCls {}) = False
-reOrient _fl (VarCls tv1) (VarCls tv2)
+reOrient _ev (VarCls tv1) (VarCls tv2)
| isMetaTyVar tv2 && not (isMetaTyVar tv1) = True
| otherwise = False
-- Just for efficiency, see CTyEqCan invariants
------------------
-canEqLeaf :: SubGoalDepth -- Depth
- -> CtEvidence
+canEqLeaf :: CtLoc -> CtEvidence
-> Type -> Type
-> TcS StopOrContinue
-- Canonicalizing "leaf" equality constraints which cannot be
@@ -1093,53 +1084,51 @@ canEqLeaf :: SubGoalDepth -- Depth
-- Preconditions:
-- * one of the two arguments is variable or family applications
-- * the two types are not equal (looking through synonyms)
-canEqLeaf d fl s1 s2
+canEqLeaf loc ev s1 s2
| cls1 `re_orient` cls2
- = do { traceTcS "canEqLeaf (reorienting)" $ ppr fl <+> dcolon <+> pprEq s1 s2
+ = do { traceTcS "canEqLeaf (reorienting)" $ ppr ev <+> dcolon <+> pprEq s1 s2
; let xcomp [x] = EvCoercion (mkTcSymCo (evTermCoercion x))
xcomp _ = panic "canEqLeaf: can't happen"
xdecomp x = [EvCoercion (mkTcSymCo (evTermCoercion x))]
xev = XEvTerm xcomp xdecomp
- ; ctevs <- xCtFlavor fl [mkTcEqPred s2 s1] xev
+ ; ctevs <- xCtFlavor ev [mkTcEqPred s2 s1] xev
; case ctevs of
[] -> return Stop
- [ctev] -> canEqLeafOriented d ctev s2 s1
+ [ctev] -> canEqLeafOriented loc ctev s2 s1
_ -> panic "canEqLeaf" }
| otherwise
= do { traceTcS "canEqLeaf" $ ppr (mkTcEqPred s1 s2)
- ; canEqLeafOriented d fl s1 s2 }
+ ; canEqLeafOriented loc ev s1 s2 }
where
- re_orient = reOrient fl
+ re_orient = reOrient ev
cls1 = classify s1
cls2 = classify s2
-canEqLeafOriented :: SubGoalDepth -- Depth
- -> CtEvidence
+canEqLeafOriented :: CtLoc -> CtEvidence
-> TcType -> TcType -> TcS StopOrContinue
-- By now s1 will either be a variable or a type family application
-canEqLeafOriented d fl s1 s2
- = can_eq_split_lhs d fl s1 s2
- where can_eq_split_lhs d fl s1 s2
+canEqLeafOriented loc ev s1 s2
+ = can_eq_split_lhs loc ev s1 s2
+ where can_eq_split_lhs loc ev s1 s2
| Just (fn,tys1) <- splitTyConApp_maybe s1
- = canEqLeafFunEq d fl (fn,tys1) s2
+ = canEqLeafFunEq loc ev (fn,tys1) s2
| Just tv <- getTyVar_maybe s1
- = canEqLeafTyVarLeftRec d fl tv s2
+ = canEqLeafTyVarLeftRec loc ev tv s2
| otherwise
= pprPanic "canEqLeafOriented" $
- text "Non-variable or non-family equality LHS" <+> ppr (ctEvPred fl)
+ text "Non-variable or non-family equality LHS" <+> ppr (ctEvPred ev)
-canEqLeafFunEq :: SubGoalDepth
- -> CtEvidence
- -> (TyCon,[TcType]) -> TcType -> TcS StopOrContinue
-canEqLeafFunEq d ev (fn,tys1) ty2 -- ev :: F tys1 ~ ty2
+canEqLeafFunEq :: CtLoc -> CtEvidence
+ -> (TyCon,[TcType]) -> TcType -> TcS StopOrContinue
+canEqLeafFunEq loc ev (fn,tys1) ty2 -- ev :: F tys1 ~ ty2
= do { traceTcS "canEqLeafFunEq" $ pprEq (mkTyConApp fn tys1) ty2
; (xis1,cos1) <-
{-# SCC "flattenMany" #-}
- flattenMany d FMFullFlatten ev tys1 -- Flatten type function arguments
+ flattenMany loc FMFullFlatten ev tys1 -- Flatten type function arguments
-- cos1 :: xis1 ~ tys1
; (xi2,co2) <- {-# SCC "flatten" #-}
- flatten d FMFullFlatten ev ty2 -- co2 :: xi2 ~ ty2
+ flatten loc FMFullFlatten ev ty2 -- co2 :: xi2 ~ ty2
; let fam_head = mkTyConApp fn xis1
-- Fancy higher-dimensional coercion between equalities!
@@ -1156,23 +1145,22 @@ canEqLeafFunEq d ev (fn,tys1) ty2 -- ev :: F tys1 ~ ty2
| isTcReflCo xco -> continueWith new_ct
| otherwise -> do { updWorkListTcS (extendWorkListEq new_ct); return Stop }
where
- new_ct = CFunEqCan { cc_ev = new_ev, cc_depth = d
+ new_ct = CFunEqCan { cc_ev = new_ev, cc_loc = loc
, cc_fun = fn, cc_tyargs = xis1, cc_rhs = xi2 } } }
-canEqLeafTyVarLeftRec :: SubGoalDepth
- -> CtEvidence
+canEqLeafTyVarLeftRec :: CtLoc -> CtEvidence
-> TcTyVar -> TcType -> TcS StopOrContinue
-canEqLeafTyVarLeftRec d fl tv s2 -- fl :: tv ~ s2
+canEqLeafTyVarLeftRec loc ev tv s2 -- ev :: tv ~ s2
= do { traceTcS "canEqLeafTyVarLeftRec" $ pprEq (mkTyVarTy tv) s2
- ; (xi1,co1) <- flattenTyVar d FMFullFlatten fl tv -- co1 :: xi1 ~ tv
+ ; (xi1,co1) <- flattenTyVar loc FMFullFlatten ev tv -- co1 :: xi1 ~ tv
; traceTcS "canEqLeafTyVarLeftRec2" $ empty
; let co = mkTcTyConAppCo eqTyCon $ [ mkTcReflCo (defaultKind $ typeKind s2)
, co1, mkTcReflCo s2]
-- co :: (xi1 ~ s2) ~ (tv ~ s2)
- ; mb <- rewriteCtFlavor fl (mkTcEqPred xi1 s2) co
+ ; mb <- rewriteCtFlavor ev (mkTcEqPred xi1 s2) co
-- NB that rewriteCtFlavor does not cache the result
-- See Note [Caching loops]
@@ -1180,19 +1168,18 @@ canEqLeafTyVarLeftRec d fl tv s2 -- fl :: tv ~ s2
; case mb of
Nothing -> return Stop
- Just new_fl ->
+ Just new_ev ->
case getTyVar_maybe xi1 of
- Just tv' -> canEqLeafTyVarLeft d new_fl tv' s2
- Nothing -> canEq d new_fl xi1 s2 }
+ Just tv' -> canEqLeafTyVarLeft loc new_ev tv' s2
+ Nothing -> canEq loc new_ev xi1 s2 }
-canEqLeafTyVarLeft :: SubGoalDepth -- Depth
- -> CtEvidence
+canEqLeafTyVarLeft :: CtLoc -> CtEvidence
-> TcTyVar -> TcType -> TcS StopOrContinue
-- Precondition LHS is fully rewritten from inerts (but not RHS)
-canEqLeafTyVarLeft d fl tv s2 -- eqv : tv ~ s2
+canEqLeafTyVarLeft loc ev tv s2 -- eqv : tv ~ s2
= do { let tv_ty = mkTyVarTy tv
; traceTcS "canEqLeafTyVarLeft" (pprEq tv_ty s2)
- ; (xi2, co2) <- flatten d FMFullFlatten fl s2 -- Flatten RHS co:xi2 ~ s2
+ ; (xi2, co2) <- flatten loc FMFullFlatten ev s2 -- Flatten RHS co:xi2 ~ s2
; traceTcS "canEqLeafTyVarLeft" (nest 2 (vcat [ text "tv =" <+> ppr tv
, text "s2 =" <+> ppr s2
@@ -1200,7 +1187,7 @@ canEqLeafTyVarLeft d fl tv s2 -- eqv : tv ~ s2
-- Reflexivity exposed through flattening
; if tv_ty `eqType` xi2 then
- when (isWanted fl) (setEvBind (ctev_evar fl) (EvCoercion co2)) >>
+ when (isWanted ev) (setEvBind (ctev_evar ev) (EvCoercion co2)) >>
return Stop
else do
-- Not reflexivity but maybe an occurs error
@@ -1208,16 +1195,16 @@ canEqLeafTyVarLeft d fl tv s2 -- eqv : tv ~ s2
xi2' = fromMaybe xi2 occ_check_result
co = mkTcTyConAppCo eqTyCon $
[mkTcReflCo (defaultKind $ typeKind s2), mkTcReflCo tv_ty, co2]
- ; mb <- rewriteCtFlavor fl (mkTcEqPred tv_ty xi2') co
+ ; mb <- rewriteCtFlavor ev (mkTcEqPred tv_ty xi2') co
-- NB that rewriteCtFlavor does not cache the result (as it used to)
-- which would be wrong if the constraint has an occurs error
; case mb of
- Just new_fl -> case occ_check_result of
+ Just new_ev -> case occ_check_result of
Just {} -> continueWith $
- CTyEqCan { cc_ev = new_fl, cc_depth = d
+ CTyEqCan { cc_ev = new_ev, cc_loc = loc
, cc_tyvar = tv, cc_rhs = xi2' }
- Nothing -> canEqFailure d new_fl
+ Nothing -> canEqFailure loc new_ev
Nothing -> return Stop
} }
\end{code}
diff --git a/compiler/typecheck/TcErrors.lhs b/compiler/typecheck/TcErrors.lhs
index cb6990d91e..cec65dea00 100644
--- a/compiler/typecheck/TcErrors.lhs
+++ b/compiler/typecheck/TcErrors.lhs
@@ -11,13 +11,13 @@ module TcErrors(
reportUnsolved, reportAllUnsolved,
warnDefaulting,
- flattenForAllErrorTcS,
solverDepthErrorTcS
) where
#include "HsVersions.h"
import TcCanonical( occurCheckExpand )
+import TcRnTypes
import TcRnMonad
import TcMType
import TcType
@@ -41,6 +41,7 @@ import BasicTypes
import Util
import FastString
import Outputable
+import SrcLoc
import DynFlags
import Data.List ( partition, mapAccumL )
\end{code}
@@ -130,10 +131,10 @@ report_unsolved mb_binds_var defer wanted
-- Don't report ambiguity errors if
-- there are any other solid errors
-- to report
- , cec_extra = empty
, cec_tidy = tidy_env
- , cec_defer = defer
- , cec_binds = mb_binds_var }
+ , cec_defer = defer
+ , cec_suppress = False
+ , cec_binds = mb_binds_var }
; traceTc "reportUnsolved (after unflattening):" $
vcat [ pprTvBndrs (varSetElems free_tvs)
@@ -150,7 +151,6 @@ data ReportErrCtxt
-- (innermost first)
-- ic_skols and givens are tidied, rest are not
, cec_tidy :: TidyEnv
- , cec_extra :: SDoc -- Add this to each error message
, cec_insol :: Bool -- True <=> do not report errors involving
-- ambiguous errors
@@ -159,15 +159,19 @@ data ReportErrCtxt
-- Just ev <=> make some errors (depending on cec_defer)
-- into warnings, and emit evidence bindings
-- into 'ev' for unsolved constraints
+
, cec_defer :: Bool -- True <=> -fdefer-type-errors
-- Irrelevant if cec_binds = Nothing
+ , cec_suppress :: Bool -- True <=> More important errors have occurred,
+ -- so create bindings if need be, but
+ -- don't issue any more errors/warnings
}
reportImplic :: ReportErrCtxt -> Implication -> TcM ()
reportImplic ctxt implic@(Implic { ic_skols = tvs, ic_given = given
, ic_wanted = wanted, ic_binds = evb
- , ic_insol = insoluble, ic_loc = loc })
- | BracketSkol <- ctLocOrigin loc
+ , ic_insol = insoluble, ic_info = info })
+ | BracketSkol <- info
, not insoluble -- For Template Haskell brackets report only
= return () -- definite errors. The whole thing will be re-checked
-- later when we plug it in, and meanwhile there may
@@ -177,10 +181,11 @@ reportImplic ctxt implic@(Implic { ic_skols = tvs, ic_given = given
= reportWanteds ctxt' wanted
where
(env1, tvs') = mapAccumL tidyTyVarBndr (cec_tidy ctxt) tvs
+ (env2, info') = tidySkolemInfo env1 info
implic' = implic { ic_skols = tvs'
- , ic_given = map (tidyEvVar env1) given
- , ic_loc = tidyGivenLoc env1 loc }
- ctxt' = ctxt { cec_tidy = env1
+ , ic_given = map (tidyEvVar env2) given
+ , ic_info = info' }
+ ctxt' = ctxt { cec_tidy = env2
, cec_encl = implic' : cec_encl ctxt
, cec_binds = case cec_binds ctxt of
Nothing -> Nothing
@@ -188,7 +193,7 @@ reportImplic ctxt implic@(Implic { ic_skols = tvs, ic_given = given
reportWanteds :: ReportErrCtxt -> WantedConstraints -> TcM ()
reportWanteds ctxt (WC { wc_flat = flats, wc_insol = insols, wc_impl = implics })
- = do { reportOrDefer ctxt tidy_cts
+ = do { reportFlats ctxt tidy_cts
; mapBagM_ (reportImplic ctxt) implics }
where
env = cec_tidy ctxt
@@ -198,47 +203,6 @@ reportWanteds ctxt (WC { wc_flat = flats, wc_insol = insols, wc_impl = implics }
-- to report unsolved Derived goals as error
-- See Note [Do not report derived but soluble errors]
-reportOrDefer :: ReportErrCtxt -> Cts -> TcM ()
-reportOrDefer ctxt@(CEC { cec_binds = mb_binds_var
- , cec_defer = defer_errs }) cts
- | Just ev_binds_var <- mb_binds_var
- , defer_errs -- -fdefer-type-errors: Defer all
- -- See Note [Deferring coercion errors to runtime]
- = mapBagM_ (deferToRuntime ev_binds_var ctxt mkFlatErr) cts
-
- | Just ev_binds_var <- mb_binds_var
- -- No -fdefer-type-errors: Defer only holes
- -- See Note [Deferring coercion errors to runtime]
- = do { let (holes, non_holes) = partitionBag isHoleCt cts
- ; reportFlats ctxt non_holes
- ; mapBagM_ (deferToRuntime ev_binds_var ctxt mkFlatErr) holes }
- -- Thijs had something about extending the tidy-env, but I don't know why
-
- | otherwise -- Defer nothing
- = reportFlats ctxt cts
-
-deferToRuntime :: EvBindsVar -> ReportErrCtxt -> (ReportErrCtxt -> Ct -> TcM ErrMsg)
- -> Ct -> TcM ()
--- See Note [Deferring coercion errors to runtime]
-deferToRuntime ev_binds_var ctxt mk_err_msg ct
- | CtWanted { ctev_wloc = loc, ctev_pred = pred, ctev_evar = ev_id } <- cc_ev ct
- = do { ctxt' <- relevantBindings ctxt ct
- ; err <- setCtLoc loc $
- mk_err_msg ctxt' ct
- ; dflags <- getDynFlags
- ; let err_msg = pprLocErrMsg err
- err_fs = mkFastString $ showSDoc dflags $
- err_msg $$ text "(deferred type error)"
-
- -- Create the binding
- ; addTcEvBind ev_binds_var ev_id (EvDelayedError pred err_fs)
-
- -- And emit a warning
- ; reportWarning (makeIntoWarning err) }
-
- | otherwise -- Do not set any evidence for Given/Derived
- = return ()
-
reportFlats :: ReportErrCtxt -> Cts -> TcM ()
reportFlats ctxt flats -- Here 'flats' includes insolble goals
= tryReporters
@@ -292,19 +256,6 @@ isTyFun_maybe ty = case tcSplitTyConApp_maybe ty of
_ -> Nothing
-----------------
-mkFlatErr :: ReportErrCtxt -> Ct -> TcM ErrMsg
--- Context is already set
-mkFlatErr ctxt ct -- The constraint is always wanted
- | isHoleCt ct
- = mkHoleError ctxt ct
- | otherwise
- = case classifyPredType (ctPred ct) of
- ClassPred cls _ | isIPClass cls -> mkIPErr ctxt [ct]
- | otherwise -> mkDictErr ctxt [ct]
- IrredPred {} -> mkIrredErr ctxt [ct]
- EqPred {} -> mkEqErr1 ctxt ct
- TuplePred {} -> panic "mkFlat"
-
reportAmbigErrs :: Reporter
reportAmbigErrs ctxt cts
| cec_insol ctxt = return ()
@@ -352,10 +303,9 @@ mkUniReporter :: (ReportErrCtxt -> Ct -> TcM ErrMsg) -> Reporter
-- Reports errors one at a time
mkUniReporter mk_err ctxt
= mapM_ $ \ct ->
- do { ctxt' <- relevantBindings ctxt ct
- ; err <- setCtFlavorLoc (cc_ev ct) $
- mk_err ctxt' ct;
- ; reportError err }
+ do { err <- mk_err ctxt ct
+ ; maybeReportError ctxt err ct
+ ; maybeAddDeferredBinding ctxt err ct }
mkGroupReporter :: (ReportErrCtxt -> [Ct] -> TcM ErrMsg)
-- Make error message for a group
@@ -366,50 +316,75 @@ mkGroupReporter :: (ReportErrCtxt -> [Ct] -> TcM ErrMsg)
mkGroupReporter _ _ []
= return ()
mkGroupReporter mk_err ctxt (ct1 : rest)
- = do { ctxt' <- relevantBindings ctxt ct1
- ; err <- setCtFlavorLoc flavor $
- mk_err ctxt' cts
- ; reportError err
+ = do { err <- mk_err ctxt cts
+ ; maybeReportError ctxt err ct1
+ ; mapM_ (maybeAddDeferredBinding ctxt err) (ct1:rest)
+ -- Add deferred bindings for all
; mkGroupReporter mk_err ctxt others }
where
- flavor = cc_ev ct1
+ loc = cc_loc ct1
cts = ct1 : friends
(friends, others) = partition is_friend rest
- is_friend friend = cc_ev friend `same_group` flavor
-
- same_group :: CtEvidence -> CtEvidence -> Bool
- same_group (CtGiven {ctev_gloc = l1}) (CtGiven {ctev_gloc = l2}) = same_loc l1 l2
- same_group (CtWanted {ctev_wloc = l1}) (CtWanted {ctev_wloc = l2}) = same_loc l1 l2
- same_group (CtDerived {ctev_wloc = l1}) (CtDerived {ctev_wloc = l2}) = same_loc l1 l2
- same_group _ _ = False
+ is_friend friend = cc_loc friend `same_loc` loc
- same_loc :: CtLoc o -> CtLoc o -> Bool
+ same_loc :: CtLoc -> CtLoc -> Bool
same_loc l1 l2 = ctLocSpan l1 == ctLocSpan l2
+maybeReportError :: ReportErrCtxt -> ErrMsg -> Ct -> TcM ()
+-- Report the error and/or make a deferred binding for it
+maybeReportError ctxt err ct
+ | cec_suppress ctxt
+ = return ()
+ | isHoleCt ct || cec_defer ctxt -- And it's a hole or we have -fdefer-type-errors
+ = reportWarning (makeIntoWarning err)
+ | otherwise
+ = reportError err
+
+maybeAddDeferredBinding :: ReportErrCtxt -> ErrMsg -> Ct -> TcM ()
+-- See Note [Deferring coercion errors to runtime]
+maybeAddDeferredBinding ctxt err ct
+ | CtWanted { ctev_pred = pred, ctev_evar = ev_id } <- cc_ev ct
+ -- Only add deferred bindings for Wanted constraints
+ , isHoleCt ct || cec_defer ctxt -- And it's a hole or we have -fdefer-type-errors
+ , Just ev_binds_var <- cec_binds ctxt -- We hvae somewhere to put the bindings
+ = do { dflags <- getDynFlags
+ ; let err_msg = pprLocErrMsg err
+ err_fs = mkFastString $ showSDoc dflags $
+ err_msg $$ text "(deferred type error)"
+
+ -- Create the binding
+ ; addTcEvBind ev_binds_var ev_id (EvDelayedError pred err_fs) }
+
+ | otherwise -- Do not set any evidence for Given/Derived
+ = return ()
tryReporters :: [(String, Ct -> PredTree -> Bool, Reporter)]
-> Reporter -> Reporter
-- Use the first reporter in the list whose predicate says True
tryReporters reporters deflt ctxt cts
= do { traceTc "tryReporters {" (ppr cts)
- ; go reporters cts
+ ; go ctxt reporters cts
; traceTc "tryReporters }" empty }
where
- go [] cts = deflt ctxt cts
- go ((str, pred, reporter) : rs) cts
- | null yeses = traceTc "tryReporters: no" (text str) >>
- go rs cts
- | otherwise = traceTc "tryReporters: yes" (text str <+> ppr yeses) >>
- reporter ctxt yeses
+ go ctxt [] cts = deflt ctxt cts
+ go ctxt ((str, pred, reporter) : rs) cts
+ | null yeses = do { traceTc "tryReporters: no" (text str)
+ ; go ctxt rs cts }
+ | otherwise = do { traceTc "tryReporters: yes" (text str <+> ppr yeses)
+ ; reporter ctxt yeses :: TcM ()
+ ; go (ctxt { cec_suppress = True }) rs nos }
+ -- Carry on with the rest, because we must make
+ -- deferred bindings for them if we have
+ -- -fdefer-type-errors
where
- yeses = filter keep_me cts
+ (yeses, nos) = partition keep_me cts
keep_me ct = pred ct (classifyPredType (ctPred ct))
-- Add the "arising from..." part to a message about bunch of dicts
addArising :: CtOrigin -> SDoc -> SDoc
addArising orig msg = hang msg 2 (pprArising orig)
-pprWithArising :: [Ct] -> (WantedLoc, SDoc)
+pprWithArising :: [Ct] -> (CtLoc, SDoc)
-- Print something like
-- (Eq a) arising from a use of x at y
-- (Show a) arising from a use of p at q
@@ -419,26 +394,30 @@ pprWithArising []
= panic "pprWithArising"
pprWithArising (ct:cts)
| null cts
- = (loc, addArising (ctLocOrigin (ctWantedLoc ct))
+ = (loc, addArising (ctLocOrigin loc)
(pprTheta [ctPred ct]))
| otherwise
= (loc, vcat (map ppr_one (ct:cts)))
where
- loc = ctWantedLoc ct
+ loc = cc_loc ct
ppr_one ct = hang (parens (pprType (ctPred ct)))
- 2 (pprArisingAt (ctWantedLoc ct))
+ 2 (pprArisingAt (cc_loc ct))
-mkErrorReport :: ReportErrCtxt -> SDoc -> TcM ErrMsg
-mkErrorReport ctxt msg = mkErrTcM (cec_tidy ctxt, msg $$ cec_extra ctxt)
+mkErrorMsg :: ReportErrCtxt -> Ct -> SDoc -> TcM ErrMsg
+mkErrorMsg ctxt ct msg
+ = do { let tcl_env = ctLocEnv (cc_loc ct)
+ ; err_info <- mkErrInfo (cec_tidy ctxt) (tcl_ctxt tcl_env)
+ ; mkLongErrAt (tcl_loc tcl_env) msg err_info }
-type UserGiven = ([EvVar], GivenLoc)
+type UserGiven = ([EvVar], SkolemInfo, SrcSpan)
getUserGivens :: ReportErrCtxt -> [UserGiven]
-- One item for each enclosing implication
getUserGivens (CEC {cec_encl = ctxt})
= reverse $
- [ (givens, loc) | Implic {ic_given = givens, ic_loc = loc} <- ctxt
- , not (null givens) ]
+ [ (givens, info, tcl_loc env)
+ | Implic {ic_given = givens, ic_env = env, ic_info = info } <- ctxt
+ , not (null givens) ]
\end{code}
Note [Do not report derived but soluble errors]
@@ -500,70 +479,44 @@ solve it.
\begin{code}
mkIrredErr :: ReportErrCtxt -> [Ct] -> TcM ErrMsg
mkIrredErr ctxt cts
- = mkErrorReport ctxt msg
+ = do { (ctxt, binds_msg) <- relevantBindings ctxt ct1
+ ; mkErrorMsg ctxt ct1 (msg $$ binds_msg) }
where
(ct1:_) = cts
- orig = ctLocOrigin (ctWantedLoc ct1)
+ orig = ctLocOrigin (cc_loc ct1)
givens = getUserGivens ctxt
msg = couldNotDeduce givens (map ctPred cts, orig)
-\end{code}
-\begin{code}
+----------------
mkHoleError :: ReportErrCtxt -> Ct -> TcM ErrMsg
mkHoleError ctxt ct@(CHoleCan {})
- = do { let env0 = cec_tidy ctxt
- ; let vars = tyVarsOfCt ct
-
- ; zonked_vars <- zonkTyVarsAndFV vars
-
- ; (env1, zonked_ty) <- zonkTidyTcType env0 (cc_hole_ty ct)
-
- ; let (env2, tyvars) = tidyOpenTyVars env1 (varSetElems zonked_vars)
-
- ; tyvars_msg <- mapM loc_msg tyvars
-
- ; traceTc "mkHoleError" (ppr env2)
-
- ; let msg = (text "Found hole" <+> quotes (text "_") <+> text "with type") <+> pprType zonked_ty
+ = do { let tyvars = varSetElems (tyVarsOfCt ct)
+ tyvars_msg = map loc_msg tyvars
+ msg = (text "Found hole" <+> quotes (text "_")
+ <+> text "with type") <+> pprType (cc_hole_ty ct)
$$ (if null tyvars_msg then empty else text "Where:" <+> vcat tyvars_msg)
-
- ; mkErrorReport ctxt msg
- }
+ ; (ctxt, binds_doc) <- relevantBindings ctxt ct
+ ; mkErrorMsg ctxt ct (msg $$ binds_doc) }
where
- loc_msg tv = case tcTyVarDetails tv of
- SkolemTv {} -> return $ (quotes $ ppr tv) <+> skol_msg
- MetaTv {} -> do { tyvar <- readMetaTyVar tv
- ; return $ case tyvar of
- (Indirect ty) -> (quotes $ pprType ty) <+> skol_msg
- Flexi -> (quotes $ ppr tv) <+> text "is a free type variable"
- }
- det -> return $ pprTcTyVarDetails det
- where skol_msg = ppr_skol (getSkolemInfo (cec_encl ctxt) tv) (getSrcLoc tv)
-
- ppr_skol given_loc tv_loc = case skol_info of
- UnkSkol -> ptext (sLit "is an unknown type variable")
- _ -> sep [ ptext (sLit "is a rigid type variable bound by"),
- sep [ppr skol_info, ptext (sLit "at") <+> ppr tv_loc]]
- where
- skol_info = ctLocOrigin given_loc
+ loc_msg tv
+ = case tcTyVarDetails tv of
+ SkolemTv {} -> quotes (ppr tv) <+> skol_msg
+ MetaTv {} -> quotes (ppr tv) <+> text "is a free type variable"
+ det -> pprTcTyVarDetails det
+ where
+ skol_msg = pprSkol (getSkolemInfo (cec_encl ctxt) tv) (getSrcLoc tv)
mkHoleError _ ct = pprPanic "mkHoleError" (ppr ct)
-\end{code}
-%************************************************************************
-%* *
- Implicit parameter errors
-%* *
-%************************************************************************
-
-\begin{code}
+----------------
mkIPErr :: ReportErrCtxt -> [Ct] -> TcM ErrMsg
mkIPErr ctxt cts
- = do { (ctxt', _, ambig_err) <- mkAmbigMsg ctxt cts
- ; mkErrorReport ctxt' (msg $$ ambig_err) }
+ = do { (ctxt, _, ambig_err) <- mkAmbigMsg ctxt cts
+ ; (ctxt, bind_msg) <- relevantBindings ctxt ct1
+ ; mkErrorMsg ctxt ct1 (msg $$ ambig_err $$ bind_msg) }
where
(ct1:_) = cts
- orig = ctLocOrigin (ctWantedLoc ct1)
+ orig = ctLocOrigin (cc_loc ct1)
preds = map ctPred cts
givens = getUserGivens ctxt
msg | null givens
@@ -591,110 +544,107 @@ mkEqErr _ [] = panic "mkEqErr"
mkEqErr1 :: ReportErrCtxt -> Ct -> TcM ErrMsg
-- Wanted constraints only!
mkEqErr1 ctxt ct
- = if isGiven flav then
- let ctx2 = ctxt { cec_extra = cec_extra ctxt $$ inaccessible_msg flav }
- in mkEqErr_help ctx2 ct False ty1 ty2
- else
- do { let orig = ctLocOrigin (getWantedLoc flav)
- ; (ctxt1, orig') <- zonkTidyOrigin ctxt orig
- ; mk_err ctxt1 orig' }
+ = do { (ctxt, binds_msg) <- relevantBindings ctxt ct
+ ; (ctxt, orig) <- zonkTidyOrigin ctxt orig
+ ; if isGiven ev then
+ mkEqErr_help ctxt (inaccessible_msg orig $$ binds_msg) ct False ty1 ty2
+ else
+ mk_err binds_msg orig }
where
-
- flav = cc_ev ct
-
- inaccessible_msg (CtGiven { ctev_gloc = loc })
- = hang (ptext (sLit "Inaccessible code in"))
- 2 (ppr (ctLocOrigin loc))
- -- If a Solved then we should not report inaccessible code
- inaccessible_msg _ = empty
-
+ ev = cc_ev ct
+ orig = ctLocOrigin (cc_loc ct)
(ty1, ty2) = getEqPredTys (ctPred ct)
+ inaccessible_msg orig = hang (ptext (sLit "Inaccessible code in"))
+ 2 (ppr orig)
+
-- If the types in the error message are the same as the types
-- we are unifying, don't add the extra expected/actual message
- mk_err ctxt1 (TypeEqOrigin (UnifyOrigin { uo_actual = act, uo_expected = exp }))
+ mk_err extra (TypeEqOrigin (UnifyOrigin { uo_actual = act, uo_expected = exp }))
| act `pickyEqType` ty1
- , exp `pickyEqType` ty2 = mkEqErr_help ctxt1 ct True ty2 ty1
+ , exp `pickyEqType` ty2 = mkEqErr_help ctxt extra ct True ty2 ty1
| exp `pickyEqType` ty1
- , act `pickyEqType` ty2 = mkEqErr_help ctxt1 ct True ty1 ty2
- | otherwise = mkEqErr_help ctxt2 ct False ty1 ty2
+ , act `pickyEqType` ty2 = mkEqErr_help ctxt extra ct True ty1 ty2
+ | otherwise = mkEqErr_help ctxt extra1 ct False ty1 ty2
where
- ctxt2 = ctxt1 { cec_extra = msg $$ cec_extra ctxt1 }
- msg = mkExpectedActualMsg exp act
- mk_err ctxt1 _ = mkEqErr_help ctxt1 ct False ty1 ty2
+ extra1 = msg $$ extra
+ msg = mkExpectedActualMsg exp act
+ mk_err extra _ = mkEqErr_help ctxt extra ct False ty1 ty2
mkEqErr_help, reportEqErr
- :: ReportErrCtxt
+ :: ReportErrCtxt -> SDoc
-> Ct
-> Bool -- True <=> Types are correct way round;
-- report "expected ty1, actual ty2"
-- False <=> Just report a mismatch without orientation
-- The ReportErrCtxt has expected/actual
-> TcType -> TcType -> TcM ErrMsg
-mkEqErr_help ctxt ct oriented ty1 ty2
- | Just tv1 <- tcGetTyVar_maybe ty1 = mkTyVarEqErr ctxt ct oriented tv1 ty2
- | Just tv2 <- tcGetTyVar_maybe ty2 = mkTyVarEqErr ctxt ct oriented tv2 ty1
- | otherwise = reportEqErr ctxt ct oriented ty1 ty2
+mkEqErr_help ctxt extra ct oriented ty1 ty2
+ | Just tv1 <- tcGetTyVar_maybe ty1 = mkTyVarEqErr ctxt extra ct oriented tv1 ty2
+ | Just tv2 <- tcGetTyVar_maybe ty2 = mkTyVarEqErr ctxt extra ct oriented tv2 ty1
+ | otherwise = reportEqErr ctxt extra ct oriented ty1 ty2
-reportEqErr ctxt ct oriented ty1 ty2
- = do { ctxt' <- mkEqInfoMsg ctxt ct ty1 ty2
- ; mkErrorReport ctxt' (misMatchOrCND ctxt' ct oriented ty1 ty2) }
+reportEqErr ctxt extra1 ct oriented ty1 ty2
+ = do { (ctxt', extra2) <- mkEqInfoMsg ctxt ct ty1 ty2
+ ; mkErrorMsg ctxt' ct (vcat [ misMatchOrCND ctxt' ct oriented ty1 ty2
+ , extra2, extra1]) }
-mkTyVarEqErr :: ReportErrCtxt -> Ct -> Bool -> TcTyVar -> TcType -> TcM ErrMsg
+mkTyVarEqErr :: ReportErrCtxt -> SDoc -> Ct -> Bool -> TcTyVar -> TcType -> TcM ErrMsg
-- tv1 and ty2 are already tidied
-mkTyVarEqErr ctxt ct oriented tv1 ty2
+mkTyVarEqErr ctxt extra ct oriented tv1 ty2
-- Occurs check
| isNothing (occurCheckExpand tv1 ty2)
= let occCheckMsg = hang (text "Occurs check: cannot construct the infinite type:") 2
(sep [ppr ty1, char '~', ppr ty2])
- in mkErrorReport ctxt occCheckMsg
+ in mkErrorMsg ctxt ct (occCheckMsg $$ extra)
| isSkolemTyVar tv1 -- ty2 won't be a meta-tyvar, or else the thing would
-- be oriented the other way round; see TcCanonical.reOrient
|| isSigTyVar tv1 && not (isTyVarTy ty2)
- = mkErrorReport (addExtraTyVarInfo ctxt ty1 ty2)
- (misMatchOrCND ctxt ct oriented ty1 ty2)
+ = mkErrorMsg ctxt ct (vcat [ misMatchOrCND ctxt ct oriented ty1 ty2
+ , extraTyVarInfo ctxt ty1 ty2
+ , extra ])
-- So tv is a meta tyvar, and presumably it is
-- an *untouchable* meta tyvar, else it'd have been unified
| not (k2 `tcIsSubKind` k1) -- Kind error
- = mkErrorReport ctxt $ (kindErrorMsg (mkTyVarTy tv1) ty2)
+ = mkErrorMsg ctxt ct $ (kindErrorMsg (mkTyVarTy tv1) ty2 $$ extra)
-- Check for skolem escape
| (implic:_) <- cec_encl ctxt -- Get the innermost context
- , let esc_skols = filter (`elemVarSet` (tyVarsOfType ty2)) (ic_skols implic)
- implic_loc = ic_loc implic
+ , Implic { ic_env = env, ic_skols = skols, ic_info = skol_info } <- implic
+ , let esc_skols = filter (`elemVarSet` (tyVarsOfType ty2)) skols
, not (null esc_skols)
- = setCtLoc implic_loc $ -- Override the error message location from the
- -- place the equality arose to the implication site
- do { let msg = misMatchMsg oriented ty1 ty2
+ = do { let msg = misMatchMsg oriented ty1 ty2
esc_doc = sep [ ptext (sLit "because type variable") <> plural esc_skols
<+> pprQuotedList esc_skols
, ptext (sLit "would escape") <+>
if isSingleton esc_skols then ptext (sLit "its scope")
else ptext (sLit "their scope") ]
- extra1 = vcat [ nest 2 $ esc_doc
- , sep [ (if isSingleton esc_skols
- then ptext (sLit "This (rigid, skolem) type variable is")
- else ptext (sLit "These (rigid, skolem) type variables are"))
- <+> ptext (sLit "bound by")
- , nest 2 $ ppr (ctLocOrigin implic_loc) ] ]
- ; mkErrorReport ctxt (msg $$ extra1) }
+ tv_extra = vcat [ nest 2 $ esc_doc
+ , sep [ (if isSingleton esc_skols
+ then ptext (sLit "This (rigid, skolem) type variable is")
+ else ptext (sLit "These (rigid, skolem) type variables are"))
+ <+> ptext (sLit "bound by")
+ , nest 2 $ ppr skol_info
+ , nest 2 $ ptext (sLit "at") <+> ppr (tcl_loc env) ] ]
+ ; mkErrorMsg ctxt ct (msg $$ tv_extra $$ extra) }
-- Nastiest case: attempt to unify an untouchable variable
| (implic:_) <- cec_encl ctxt -- Get the innermost context
- , let implic_loc = ic_loc implic
- given = ic_given implic
- = setCtLoc (ic_loc implic) $
- do { let msg = misMatchMsg oriented ty1 ty2
- extra = quotes (ppr tv1)
- <+> sep [ ptext (sLit "is untouchable")
- , ptext (sLit "inside the constraints") <+> pprEvVarTheta given
- , ptext (sLit "bound at") <+> ppr (ctLocOrigin implic_loc)]
- ; mkErrorReport (addExtraTyVarInfo ctxt ty1 ty2) (msg $$ nest 2 extra) }
+ , Implic { ic_env = env, ic_given = given, ic_info = skol_info } <- implic
+ = do { let msg = misMatchMsg oriented ty1 ty2
+ untch_extra
+ = nest 2 $
+ sep [ quotes (ppr tv1) <+> ptext (sLit "is untouchable")
+ , nest 2 $ ptext (sLit "inside the constraints") <+> pprEvVarTheta given
+ , nest 2 $ ptext (sLit "bound by") <+> ppr skol_info
+ , nest 2 $ ptext (sLit "at") <+> ppr (tcl_loc env) ]
+ tv_extra = extraTyVarInfo ctxt ty1 ty2
+ ; mkErrorMsg ctxt ct (vcat [msg, untch_extra, tv_extra, extra]) }
| otherwise
- = reportEqErr ctxt ct oriented (mkTyVarTy tv1) ty2
+ = reportEqErr ctxt extra ct oriented (mkTyVarTy tv1) ty2
-- This *can* happen (Trac #6123, and test T2627b)
-- Consider an ambiguous top-level constraint (a ~ F a)
-- Not an occurs check, becuase F is a type function.
@@ -703,7 +653,7 @@ mkTyVarEqErr ctxt ct oriented tv1 ty2
k2 = typeKind ty2
ty1 = mkTyVarTy tv1
-mkEqInfoMsg :: ReportErrCtxt -> Ct -> TcType -> TcType -> TcM ReportErrCtxt
+mkEqInfoMsg :: ReportErrCtxt -> Ct -> TcType -> TcType -> TcM (ReportErrCtxt, SDoc)
-- Report (a) ambiguity if either side is a type function application
-- e.g. F a0 ~ Int
-- (b) warning about injectivity if both sides are the same
@@ -713,7 +663,7 @@ mkEqInfoMsg ctxt ct ty1 ty2
= do { (ctxt', _, ambig_msg) <- if isJust mb_fun1 || isJust mb_fun2
then mkAmbigMsg ctxt [ct]
else return (ctxt, False, empty)
- ; return (ctxt' { cec_extra = tyfun_msg $$ ambig_msg $$ cec_extra ctxt' }) }
+ ; return (ctxt', tyfun_msg $$ ambig_msg) }
where
mb_fun1 = isTyFun_maybe ty1
mb_fun2 = isTyFun_maybe ty2
@@ -744,22 +694,23 @@ couldNotDeduce givens (wanteds, orig)
= vcat [ addArising orig (ptext (sLit "Could not deduce") <+> pprTheta wanteds)
, vcat (pp_givens givens)]
-pp_givens :: [([EvVar], GivenLoc)] -> [SDoc]
+pp_givens :: [UserGiven] -> [SDoc]
pp_givens givens
= case givens of
[] -> []
(g:gs) -> ppr_given (ptext (sLit "from the context")) g
: map (ppr_given (ptext (sLit "or from"))) gs
- where ppr_given herald (gs,loc)
+ where
+ ppr_given herald (gs, skol_info, loc)
= hang (herald <+> pprEvVarTheta gs)
- 2 (sep [ ptext (sLit "bound by") <+> ppr (ctLocOrigin loc)
- , ptext (sLit "at") <+> ppr (ctLocSpan loc)])
+ 2 (sep [ ptext (sLit "bound by") <+> ppr skol_info
+ , ptext (sLit "at") <+> ppr loc])
-addExtraTyVarInfo :: ReportErrCtxt -> TcType -> TcType -> ReportErrCtxt
+extraTyVarInfo :: ReportErrCtxt -> TcType -> TcType -> SDoc
-- Add on extra info about the types themselves
-- NB: The types themselves are already tidied
-addExtraTyVarInfo ctxt ty1 ty2
- = ctxt { cec_extra = nest 2 (extra1 $$ extra2) $$ cec_extra ctxt }
+extraTyVarInfo ctxt ty1 ty2
+ = nest 2 (extra1 $$ extra2)
where
extra1 = tyVarExtraInfoMsg (cec_encl ctxt) ty1
extra2 = tyVarExtraInfoMsg (cec_encl ctxt) ty2
@@ -771,21 +722,13 @@ tyVarExtraInfoMsg implics ty
, isTcTyVar tv, isSkolemTyVar tv
, let pp_tv = quotes (ppr tv)
= case tcTyVarDetails tv of
- SkolemTv {} -> pp_tv <+> ppr_skol (getSkolemInfo implics tv) (getSrcLoc tv)
+ SkolemTv {} -> pp_tv <+> pprSkol (getSkolemInfo implics tv) (getSrcLoc tv)
FlatSkol {} -> pp_tv <+> ptext (sLit "is a flattening type variable")
RuntimeUnk {} -> pp_tv <+> ptext (sLit "is an interactive-debugger skolem")
MetaTv {} -> empty
| otherwise -- Normal case
= empty
- where
- ppr_skol given_loc tv_loc
- = case skol_info of
- UnkSkol -> ptext (sLit "is an unknown type variable")
- _ -> sep [ ptext (sLit "is a rigid type variable bound by"),
- sep [ppr skol_info, ptext (sLit "at") <+> ppr tv_loc]]
- where
- skol_info = ctLocOrigin given_loc
kindErrorMsg :: TcType -> TcType -> SDoc -- Types are already tidy
kindErrorMsg ty1 ty2
@@ -847,8 +790,9 @@ mkDictErr ctxt cts
-- have the same source-location origin, to try avoid a cascade
-- of error from one location
; (ctxt, err) <- mk_dict_err ctxt (head (no_inst_cts ++ overlap_cts))
- ; mkErrorReport ctxt err }
+ ; mkErrorMsg ctxt ct1 err }
where
+ ct1:_ = cts
no_givens = null (getUserGivens ctxt)
is_no_inst (ct, (matches, unifiers, _))
= no_givens
@@ -863,13 +807,14 @@ mkDictErr ctxt cts
(clas, tys) = getClassPredTys (ctPred ct)
mk_dict_err :: ReportErrCtxt -> (Ct, ClsInstLookupResult)
- -> TcM (ReportErrCtxt, SDoc)
+ -> TcM (ReportErrCtxt, SDoc)
-- Report an overlap error if this class constraint results
-- from an overlap (returning Left clas), otherwise return (Right pred)
mk_dict_err ctxt (ct, (matches, unifiers, safe_haskell))
| null matches -- No matches but perhaps several unifiers
- = do { (ctxt', is_ambig, ambig_msg) <- mkAmbigMsg ctxt [ct]
- ; return (ctxt', cannot_resolve_msg is_ambig ambig_msg) }
+ = do { (ctxt, is_ambig, ambig_msg) <- mkAmbigMsg ctxt [ct]
+ ; (ctxt, binds_msg) <- relevantBindings ctxt ct
+ ; return (ctxt, cannot_resolve_msg is_ambig binds_msg ambig_msg) }
| not safe_haskell -- Some matches => overlap errors
= return (ctxt, overlap_msg)
@@ -877,22 +822,20 @@ mk_dict_err ctxt (ct, (matches, unifiers, safe_haskell))
| otherwise
= return (ctxt, safe_haskell_msg)
where
- orig = ctLocOrigin (ctWantedLoc ct)
+ orig = ctLocOrigin (cc_loc ct)
pred = ctPred ct
(clas, tys) = getClassPredTys pred
ispecs = [ispec | (ispec, _) <- matches]
givens = getUserGivens ctxt
all_tyvars = all isTyVarTy tys
- cannot_resolve_msg has_ambig_tvs ambig_msg
+ cannot_resolve_msg has_ambig_tvs binds_msg ambig_msg
= vcat [ addArising orig (no_inst_herald <+> pprParendType pred)
, vcat (pp_givens givens)
, if has_ambig_tvs && (not (null unifiers) || not (null givens))
- then ambig_msg $$ potential_msg
+ then ambig_msg $$ binds_msg $$ potential_msg
else empty
- , show_fixes (inst_decl_fixes
- ++ add_to_ctxt_fixes has_ambig_tvs
- ++ drv_fixes) ]
+ , show_fixes (add_to_ctxt_fixes has_ambig_tvs ++ drv_fixes) ]
potential_msg
| null unifiers = empty
@@ -916,19 +859,14 @@ mk_dict_err ctxt (ct, (matches, unifiers, safe_haskell))
ppr_skol skol_info = ppr skol_info
-- Do not suggest adding constraints to an *inferred* type signature!
- get_good_orig ic = case ctLocOrigin (ic_loc ic) of
- SigSkol (InfSigCtxt {}) _ -> Nothing
- origin -> Just origin
+ get_good_orig ic = case ic_info ic of
+ SigSkol (InfSigCtxt {}) _ -> Nothing
+ origin -> Just origin
no_inst_herald
| null givens && null matches = ptext (sLit "No instance for")
| otherwise = ptext (sLit "Could not deduce")
- inst_decl_fixes
- | all_tyvars = []
- | otherwise = [ sep [ ptext (sLit "add an instance declaration for")
- , pprParendType pred] ]
-
drv_fixes = case orig of
DerivOrigin -> [drv_fix]
_ -> []
@@ -977,12 +915,12 @@ mk_dict_err ctxt (ct, (matches, unifiers, safe_haskell))
givens = getUserGivens ctxt
matching_givens = mapCatMaybes matchable givens
- matchable (evvars,gloc)
+ matchable (evvars,skol_info,loc)
= case ev_vars_matching of
[] -> Nothing
_ -> Just $ hang (pprTheta ev_vars_matching)
- 2 (sep [ ptext (sLit "bound by") <+> ppr (ctLocOrigin gloc)
- , ptext (sLit "at") <+> ppr (ctLocSpan gloc)])
+ 2 (sep [ ptext (sLit "bound by") <+> ppr skol_info
+ , ptext (sLit "at") <+> ppr loc])
where ev_vars_matching = filter ev_var_matches (map evVarPred evvars)
ev_var_matches ty = case getClassPredTys_maybe ty of
Just (clas', tys')
@@ -1088,10 +1026,8 @@ mkAmbigMsg ctxt cts
, tyVarsOfType zonked_ty `intersectsVarSet` ambig_tv_set]
; return (ctxt, True, mk_msg dflags ambig_ids) }
where
- ct1_bndrs = case cts of
- (ct1:_) -> ASSERT( not (isGivenCt ct1) )
- tcl_bndrs (ctLocEnv (ctWantedLoc ct1))
- [] -> panic "mkAmbigMsg"
+ ct1:_ = cts
+ ct1_bndrs = tcl_bndrs (ctLocEnv (cc_loc ct1))
ambig_tv_set = foldr (unionVarSet . filterVarSet isAmbiguousTyVar . tyVarsOfCt)
emptyVarSet cts
@@ -1128,14 +1064,22 @@ mkAmbigMsg ctxt cts
-- if it is not already set!
]
-getSkolemInfo :: [Implication] -> TcTyVar -> GivenLoc
+
+pprSkol :: SkolemInfo -> SrcLoc -> SDoc
+pprSkol UnkSkol _
+ = ptext (sLit "is an unknown type variable")
+pprSkol skol_info tv_loc
+ = sep [ ptext (sLit "is a rigid type variable bound by"),
+ sep [ppr skol_info, ptext (sLit "at") <+> ppr tv_loc]]
+
+getSkolemInfo :: [Implication] -> TcTyVar -> SkolemInfo
-- Get the skolem info for a type variable
-- from the implication constraint that binds it
getSkolemInfo [] tv
= pprPanic "No skolem info:" (ppr tv)
getSkolemInfo (implic:implics) tv
- | tv `elem` ic_skols implic = ic_loc implic
+ | tv `elem` ic_skols implic = ic_info implic
| otherwise = getSkolemInfo implics tv
-----------------------
@@ -1144,10 +1088,8 @@ getSkolemInfo (implic:implics) tv
-- careful to zonk the Id's type first, so it has to be in the monad.
-- We must be careful to pass it a zonked type variable, too.
-relevantBindings :: ReportErrCtxt
- -> Ct
- -> TcM ReportErrCtxt
- -- cec_extra includes info about relevant bindings
+relevantBindings :: ReportErrCtxt -> Ct
+ -> TcM (ReportErrCtxt, SDoc)
relevantBindings ctxt ct
= do { (tidy_env', docs) <- go (cec_tidy ctxt) (6, emptyVarSet)
(reverse (tcl_bndrs lcl_env))
@@ -1158,11 +1100,11 @@ relevantBindings ctxt ct
; let doc = hang (ptext (sLit "Relevant bindings include"))
2 (vcat docs)
; if null docs
- then return ctxt
- else return (ctxt { cec_tidy = tidy_env'
- , cec_extra = doc $$ cec_extra ctxt }) }
+ then return (ctxt, empty)
+ else do { traceTc "rb" doc
+ ; return (ctxt { cec_tidy = tidy_env' }, doc) } }
where
- lcl_env = ctEvEnv (cc_ev ct)
+ lcl_env = ctLocEnv (cc_loc ct)
ct_tvs = tyVarsOfCt ct
go :: TidyEnv -> (Int, TcTyVarSet)
@@ -1217,44 +1159,19 @@ are created by in RtClosureInspect.zonkRTTIType.
%************************************************************************
\begin{code}
-solverDepthErrorTcS :: Int -> [Ct] -> TcM a
-solverDepthErrorTcS depth stack
- | null stack -- Shouldn't happen unless you say -fcontext-stack=0
- = failWith msg
- | otherwise
- = setCtFlavorLoc (cc_ev top_item) $
- do { zstack <- mapM zonkCt stack
+solverDepthErrorTcS :: Ct -> TcM a
+solverDepthErrorTcS ct
+ = setCtLoc loc $
+ do { ct <- zonkCt ct
; env0 <- tcInitTidyEnv
- ; let zstack_tvs = foldr (unionVarSet . tyVarsOfCt) emptyVarSet zstack
- tidy_env = tidyFreeTyVars env0 zstack_tvs
- tidy_cts = map (tidyCt tidy_env) zstack
- ; failWithTcM (tidy_env, hang msg 2 (vcat (map (ppr . ctPred) tidy_cts))) }
+ ; let tidy_env = tidyFreeTyVars env0 (tyVarsOfCt ct)
+ tidy_ct = tidyCt tidy_env ct
+ ; failWithTcM (tidy_env, hang msg 2 (ppr tidy_ct)) }
where
- top_item = head stack
+ loc = cc_loc ct
+ depth = ctLocDepth loc
msg = vcat [ ptext (sLit "Context reduction stack overflow; size =") <+> int depth
, ptext (sLit "Use -fcontext-stack=N to increase stack size to N") ]
-
-flattenForAllErrorTcS :: CtEvidence -> TcType -> TcM a
-flattenForAllErrorTcS fl ty
- = setCtFlavorLoc fl $
- do { env0 <- tcInitTidyEnv
- ; let (env1, ty') = tidyOpenType env0 ty
- msg = sep [ ptext (sLit "Cannot deal with a type function under a forall type:")
- , ppr ty' ]
- ; failWithTcM (env1, msg) }
-\end{code}
-
-%************************************************************************
-%* *
- Setting the context
-%* *
-%************************************************************************
-
-\begin{code}
-setCtFlavorLoc :: CtEvidence -> TcM a -> TcM a
-setCtFlavorLoc (CtWanted { ctev_wloc = loc }) thing = setCtLoc loc thing
-setCtFlavorLoc (CtDerived { ctev_wloc = loc }) thing = setCtLoc loc thing
-setCtFlavorLoc (CtGiven { ctev_gloc = loc }) thing = setCtLoc loc thing
\end{code}
%************************************************************************
@@ -1269,8 +1186,12 @@ zonkTidyTcType env ty = do { ty' <- zonkTcType ty
; return (tidyOpenType env ty') }
zonkTidyOrigin :: ReportErrCtxt -> CtOrigin -> TcM (ReportErrCtxt, CtOrigin)
+zonkTidyOrigin ctxt (GivenOrigin skol_info)
+ = do { skol_info1 <- zonkSkolemInfo skol_info
+ ; let (env1, skol_info2) = tidySkolemInfo (cec_tidy ctxt) skol_info1
+ ; return (ctxt { cec_tidy = env1 }, GivenOrigin skol_info2) }
zonkTidyOrigin ctxt (TypeEqOrigin (UnifyOrigin { uo_actual = act, uo_expected = exp }))
- = do { (env1, act') <- zonkTidyTcType (cec_tidy ctxt) act
+ = do { (env1, act') <- zonkTidyTcType (cec_tidy ctxt) act
; (env2, exp') <- zonkTidyTcType env1 exp
; return ( ctxt { cec_tidy = env2 }
, TypeEqOrigin (UnifyOrigin { uo_actual = act', uo_expected = exp' })) }
diff --git a/compiler/typecheck/TcExpr.lhs b/compiler/typecheck/TcExpr.lhs
index fed6fa7381..0b0eddc266 100644
--- a/compiler/typecheck/TcExpr.lhs
+++ b/compiler/typecheck/TcExpr.lhs
@@ -236,7 +236,7 @@ tcExpr HsHole res_ty
; traceTc "tcExpr.HsHole" (ppr ty)
; ev <- mkSysLocalM (mkFastString "_") ty
; loc <- getCtLoc HoleOrigin
- ; let can = CHoleCan { cc_ev = CtWanted loc ty ev, cc_hole_ty = ty, cc_depth = 0 }
+ ; let can = CHoleCan { cc_ev = CtWanted ty ev, cc_hole_ty = ty, cc_loc = loc }
; traceTc "tcExpr.HsHole emitting" (ppr can)
; emitInsoluble can
; tcWrapResult (HsVar ev) ty res_ty }
diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index e85fc0207e..662e47aeb7 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -85,12 +85,12 @@ Note [Basic Simplifier Plan]
If in Step 1 no such element exists, we have exceeded our context-stack
depth and will simply fail.
\begin{code}
-solveInteractGiven :: GivenLoc -> [TcTyVar] -> [EvVar] -> TcS ()
+solveInteractGiven :: CtLoc -> [TcTyVar] -> [EvVar] -> TcS ()
-- In principle the givens can kick out some wanteds from the inert
-- resulting in solving some more wanted goals here which could emit
-- implications. That's why I return a bag of implications. Not sure
-- if this can happen in practice though.
-solveInteractGiven gloc fsks givens
+solveInteractGiven loc fsks givens
= do { implics <- solveInteract (fsk_bag `unionBags` given_bag)
; ASSERT( isEmptyBag implics )
return () } -- We do not decompose *given* polymorphic equalities
@@ -99,14 +99,12 @@ solveInteractGiven gloc fsks givens
-- See Note [Do not decompose given polytype equalities]
-- in TcCanonical
where
- given_bag = listToBag [ mkNonCanonical $ CtGiven { ctev_gloc = gloc
- , ctev_evtm = EvId ev_id
- , ctev_pred = evVarPred ev_id }
+ given_bag = listToBag [ mkNonCanonical loc $ CtGiven { ctev_evtm = EvId ev_id
+ , ctev_pred = evVarPred ev_id }
| ev_id <- givens ]
- fsk_bag = listToBag [ mkNonCanonical $ CtGiven { ctev_gloc = gloc
- , ctev_evtm = EvCoercion (mkTcReflCo tv_ty)
- , ctev_pred = pred }
+ fsk_bag = listToBag [ mkNonCanonical loc $ CtGiven { ctev_evtm = EvCoercion (mkTcReflCo tv_ty)
+ , ctev_pred = pred }
| tv <- fsks
, let FlatSkol fam_ty = tcTyVarDetails tv
tv_ty = mkTyVarTy tv
@@ -131,7 +129,7 @@ solveInteract cts
NoWorkRemaining -- Done, successfuly (modulo frozen)
-> return ()
MaxDepthExceeded ct -- Failure, depth exceeded
- -> wrapErrTcS $ solverDepthErrorTcS (cc_depth ct) [ct]
+ -> wrapErrTcS $ solverDepthErrorTcS ct
NextWorkItem ct -- More work, loop around!
-> do { runSolverPipeline thePipeline ct; solve_loop max_depth } }
@@ -153,14 +151,15 @@ selectNextWorkItem max_depth
= updWorkListTcS_return pick_next
where
pick_next :: WorkList -> (SelectWorkItem, WorkList)
- pick_next wl = case selectWorkItem wl of
- (Nothing,_)
- -> (NoWorkRemaining,wl) -- No more work
- (Just ct, new_wl)
- | cc_depth ct > max_depth -- Depth exceeded
- -> (MaxDepthExceeded ct,new_wl)
- (Just ct, new_wl)
- -> (NextWorkItem ct, new_wl) -- New workitem and worklist
+ pick_next wl
+ = case selectWorkItem wl of
+ (Nothing,_)
+ -> (NoWorkRemaining,wl) -- No more work
+ (Just ct, new_wl)
+ | ctLocDepth (cc_loc ct) > max_depth -- Depth exceeded
+ -> (MaxDepthExceeded ct,new_wl)
+ (Just ct, new_wl)
+ -> (NextWorkItem ct, new_wl) -- New workitem and worklist
runSolverPipeline :: [(String,SimplifierStage)] -- The pipeline
-> WorkItem -- The work item
@@ -298,7 +297,7 @@ spontaneousSolveStage workItem
-- Post: tv ~ xi is now in TyBinds, no need to put in inerts as well
-- see Note [Spontaneously solved in TyBinds]
-> do { bumpStepCountTcS
- ; traceFireTcS (cc_depth workItem) $
+ ; traceFireTcS workItem $
ptext (sLit "Spontaneously solved:") <+> ppr workItem
; kickOutRewritable Given new_tv
; return Stop } }
@@ -426,7 +425,7 @@ data SPSolveResult = SPCantSolve
-- See Note [Touchables and givens]
trySpontaneousSolve :: WorkItem -> TcS SPSolveResult
trySpontaneousSolve workItem@(CTyEqCan { cc_ev = gw
- , cc_tyvar = tv1, cc_rhs = xi, cc_depth = d })
+ , cc_tyvar = tv1, cc_rhs = xi, cc_loc = d })
| isGiven gw
= return SPCantSolve
| Just tv2 <- tcGetTyVar_maybe xi
@@ -453,8 +452,8 @@ trySpontaneousSolve workItem@(CTyEqCan { cc_ev = gw
trySpontaneousSolve _ = return SPCantSolve
----------------
-trySpontaneousEqOneWay :: SubGoalDepth
- -> CtEvidence -> TcTyVar -> Xi -> TcS SPSolveResult
+trySpontaneousEqOneWay :: CtLoc -> CtEvidence
+ -> TcTyVar -> Xi -> TcS SPSolveResult
-- tv is a MetaTyVar, not untouchable
trySpontaneousEqOneWay d gw tv xi
| not (isSigTyVar tv) || isTyVarTy xi
@@ -463,8 +462,8 @@ trySpontaneousEqOneWay d gw tv xi
= return SPCantSolve
----------------
-trySpontaneousEqTwoWay :: SubGoalDepth
- -> CtEvidence -> TcTyVar -> TcTyVar -> TcS SPSolveResult
+trySpontaneousEqTwoWay :: CtLoc -> CtEvidence
+ -> TcTyVar -> TcTyVar -> TcS SPSolveResult
-- Both tyvars are *touchable* MetaTyvars so there is only a chance for kind error here
trySpontaneousEqTwoWay d gw tv1 tv2
@@ -550,8 +549,7 @@ unification variables as RHS of type family equations: F xis ~ alpha.
\begin{code}
----------------
-solveWithIdentity :: SubGoalDepth
- -> CtEvidence -> TcTyVar -> Xi -> TcS SPSolveResult
+solveWithIdentity :: CtLoc -> CtEvidence -> TcTyVar -> Xi -> TcS SPSolveResult
-- Solve with the identity coercion
-- Precondition: kind(xi) is a sub-kind of kind(tv)
-- Precondition: CtEvidence is Wanted or Derived
@@ -649,19 +647,18 @@ interactWithInertsStage wi
; case ir of
IRWorkItemConsumed { ir_fire = rule }
-> do { bumpStepCountTcS
- ; traceFireTcS (cc_depth wi)
- (mk_msg rule (text "WorkItemConsumed"))
+ ; traceFireTcS wi (mk_msg rule (text "WorkItemConsumed"))
; insertInertItemTcS atomic_inert
; return Stop }
IRReplace { ir_fire = rule }
-> do { bumpStepCountTcS
- ; traceFireTcS (cc_depth atomic_inert)
+ ; traceFireTcS atomic_inert
(mk_msg rule (text "InertReplace"))
; insertInertItemTcS wi
; return Stop }
IRInertConsumed { ir_fire = rule }
-> do { bumpStepCountTcS
- ; traceFireTcS (cc_depth atomic_inert)
+ ; traceFireTcS atomic_inert
(mk_msg rule (text "InertItemConsumed"))
; return (ContinueWith wi) }
IRKeepGoing {} -- Should we do a bumpStepCountTcS? No for now.
@@ -675,16 +672,16 @@ interactWithInertsStage wi
doInteractWithInert :: Ct -> Ct -> TcS InteractResult
-- Identical class constraints.
-doInteractWithInert inertItem@(CDictCan { cc_ev = fl1, cc_class = cls1, cc_tyargs = tys1 })
- workItem@(CDictCan { cc_ev = fl2, cc_class = cls2, cc_tyargs = tys2 })
+doInteractWithInert inertItem@(CDictCan { cc_ev = fl1, cc_class = cls1, cc_tyargs = tys1, cc_loc = loc1 })
+ workItem@(CDictCan { cc_ev = fl2, cc_class = cls2, cc_tyargs = tys2, cc_loc = loc2 })
| cls1 == cls2
= do { let pty1 = mkClassPred cls1 tys1
pty2 = mkClassPred cls2 tys2
- inert_pred_loc = (pty1, pprFlavorArising fl1)
- work_item_pred_loc = (pty2, pprFlavorArising fl2)
+ inert_pred_loc = (pty1, pprArisingAt loc1)
+ work_item_pred_loc = (pty2, pprArisingAt loc2)
; let fd_eqns = improveFromAnother inert_pred_loc work_item_pred_loc
- ; any_fundeps <- rewriteWithFunDeps fd_eqns fl2
+ ; fd_work <- rewriteWithFunDeps fd_eqns loc2
-- We don't really rewrite tys2, see below _rewritten_tys2, so that's ok
-- NB: We do create FDs for given to report insoluble equations that arise
-- from pairs of Givens, and also because of floating when we approximate
@@ -694,24 +691,22 @@ doInteractWithInert inertItem@(CDictCan { cc_ev = fl1, cc_class = cls1, cc_tyarg
; traceTcS "doInteractWithInert:dict"
(vcat [ text "inertItem =" <+> ppr inertItem
, text "workItem =" <+> ppr workItem
- , text "fundeps =" <+> ppr any_fundeps ])
+ , text "fundeps =" <+> ppr fd_work ])
- ; case any_fundeps of
+ ; case fd_work of
-- No Functional Dependencies
- Nothing
- | eqTypes tys1 tys2 -> solveOneFromTheOther "Cls/Cls" fl1 workItem
+ [] | eqTypes tys1 tys2 -> solveOneFromTheOther "Cls/Cls" fl1 workItem
| otherwise -> return (IRKeepGoing "NOP")
-- Actual Functional Dependencies
- Just fd_work
- | cls1 `hasKey` ipClassNameKey
+ _ | cls1 `hasKey` ipClassNameKey
, isGiven fl1, isGiven fl2 -- See Note [Shadowing of Implicit Parameters]
-> return (IRReplace ("Replace IP"))
-- Standard thing: create derived fds and keep on going. Importantly we don't
-- throw workitem back in the worklist because this can cause loops. See #5236.
| otherwise
- -> do { emitFDWorkAsDerived fd_work (cc_depth workItem)
+ -> do { updWorkListTcS (extendWorkListEqs fd_work)
; return (IRKeepGoing "Cls/Cls (new fundeps)") } -- Just keep going without droping the inert
}
@@ -725,9 +720,9 @@ doInteractWithInert (CIrredEvCan { cc_ev = ifl, cc_ty = ty1 })
= solveOneFromTheOther "Irred/Irred" ifl workItem
doInteractWithInert ii@(CFunEqCan { cc_ev = ev1, cc_fun = tc1
- , cc_tyargs = args1, cc_rhs = xi1, cc_depth = d1 })
+ , cc_tyargs = args1, cc_rhs = xi1, cc_loc = d1 })
wi@(CFunEqCan { cc_ev = ev2, cc_fun = tc2
- , cc_tyargs = args2, cc_rhs = xi2, cc_depth = d2 })
+ , cc_tyargs = args2, cc_rhs = xi2, cc_loc = d2 })
| fl1 `canSolve` fl2 && lhss_match
= do { traceTcS "interact with inerts: FunEq/FunEq" $
vcat [ text "workItem =" <+> ppr wi
@@ -1287,45 +1282,36 @@ To achieve this required some refactoring of FunDeps.lhs (nicer
now!).
\begin{code}
-rewriteWithFunDeps :: [Equation]
- -> CtEvidence
- -> TcS (Maybe [CtEvidence])
- -- Not quite a WantedEvVar unfortunately
- -- Because our intention could be to make
- -- it derived at the end of the day
--- NB: The flavor of the returned EvVars will be decided by the caller
+rewriteWithFunDeps :: [Equation] -> CtLoc -> TcS [Ct]
+-- NB: The returned constraints are all Derived
-- Post: returns no trivial equalities (identities) and all EvVars returned are fresh
-rewriteWithFunDeps eqn_pred_locs fl
- = do { fd_ev_poss <- mapM (instFunDepEqn wloc) eqn_pred_locs
- ; let fd_ev_pos :: [(Int,CtEvidence)]
- fd_ev_pos = concat fd_ev_poss
- ; if null fd_ev_pos then return Nothing
- else return (Just (map snd fd_ev_pos)) }
- where
- wloc | CtGiven { ctev_gloc = gl } <- fl = setCtLocOrigin gl FunDepOrigin
- | otherwise = ctev_wloc fl
-
-instFunDepEqn :: WantedLoc -> Equation -> TcS [(Int,CtEvidence)]
+rewriteWithFunDeps eqn_pred_locs loc
+ = do { fd_cts <- mapM (instFunDepEqn loc) eqn_pred_locs
+ ; return (concat fd_cts) }
+
+instFunDepEqn :: CtLoc -> Equation -> TcS [Ct]
-- Post: Returns the position index as well as the corresponding FunDep equality
-instFunDepEqn wl (FDEqn { fd_qtvs = tvs, fd_eqs = eqs
- , fd_pred1 = d1, fd_pred2 = d2 })
+instFunDepEqn loc (FDEqn { fd_qtvs = tvs, fd_eqs = eqs
+ , fd_pred1 = d1, fd_pred2 = d2 })
= do { (subst, _) <- instFlexiTcS tvs -- Takes account of kind substitution
; foldM (do_one subst) [] eqs }
where
- do_one subst ievs (FDEq { fd_pos = i, fd_ty_left = ty1, fd_ty_right = ty2 })
- = let sty1 = Type.substTy subst ty1
- sty2 = Type.substTy subst ty2
- in if eqType sty1 sty2 then return ievs -- Return no trivial equalities
- else do { mb_eqv <- newDerived (push_ctx wl) (mkTcEqPred sty1 sty2)
- ; case mb_eqv of
- Just ctev -> return $ (i,ctev):ievs
- Nothing -> return ievs }
- -- We are eventually going to emit FD work back in the work list so
- -- it is important that we only return the /freshly created/ and not
- -- some existing equality!
- push_ctx :: WantedLoc -> WantedLoc
- push_ctx loc = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc
-
+ der_loc = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc
+
+ do_one subst ievs (FDEq { fd_ty_left = ty1, fd_ty_right = ty2 })
+ | eqType sty1 sty2
+ = return ievs -- Return no trivial equalities
+ | otherwise
+ = do { mb_eqv <- newDerived (mkTcEqPred sty1 sty2)
+ ; case mb_eqv of
+ Just ev -> return (mkNonCanonical der_loc ev : ievs)
+ Nothing -> return ievs }
+ -- We are eventually going to emit FD work back in the work list so
+ -- it is important that we only return the /freshly created/ and not
+ -- some existing equality!
+ where
+ sty1 = Type.substTy subst ty1
+ sty2 = Type.substTy subst ty2
mkEqnMsg :: (TcPredType, SDoc)
-> (TcPredType, SDoc) -> TidyEnv -> TcM (TidyEnv, SDoc)
@@ -1338,14 +1324,6 @@ mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
nest 2 (sep [ppr tpred1 <> comma, nest 2 from1]),
nest 2 (sep [ppr tpred2 <> comma, nest 2 from2])]
; return (tidy_env, msg) }
-
-
-emitFDWorkAsDerived :: [CtEvidence] -- All Derived
- -> SubGoalDepth -> TcS ()
-emitFDWorkAsDerived evlocs d
- = updWorkListTcS $ extendWorkListEqs (map mk_fd_ct evlocs)
- where
- mk_fd_ct der_ev = CNonCanonical { cc_ev = der_ev, cc_depth = d }
\end{code}
@@ -1358,7 +1336,6 @@ emitFDWorkAsDerived evlocs d
*********************************************************************************
\begin{code}
-
topReactionsStage :: SimplifierStage
topReactionsStage workItem
= tryTopReact workItem
@@ -1372,7 +1349,7 @@ tryTopReact wi
NoTopInt -> return (ContinueWith wi)
SomeTopInt rule what_next
-> do { bumpStepCountTcS
- ; traceFireTcS (cc_depth wi) $
+ ; traceFireTcS wi $
vcat [ ptext (sLit "Top react:") <+> text rule
, text "WorkItem =" <+> ppr wi ]
; return what_next } }
@@ -1397,11 +1374,11 @@ doTopReact inerts workItem
= do { traceTcS "doTopReact" (ppr workItem)
; case workItem of
CDictCan { cc_ev = fl, cc_class = cls, cc_tyargs = xis
- , cc_depth = d }
+ , cc_loc = d }
-> doTopReactDict inerts workItem fl cls xis d
CFunEqCan { cc_ev = fl, cc_fun = tc, cc_tyargs = args
- , cc_rhs = xi, cc_depth = d }
+ , cc_rhs = xi, cc_loc = d }
-> doTopReactFunEq workItem fl tc args xi d
_ -> -- Any other work item does not react with any top-level equations
@@ -1409,32 +1386,28 @@ doTopReact inerts workItem
--------------------
doTopReactDict :: InertSet -> WorkItem -> CtEvidence -> Class -> [Xi]
- -> SubGoalDepth -> TcS TopInteractResult
-doTopReactDict inerts workItem fl cls xis depth
+ -> CtLoc -> TcS TopInteractResult
+doTopReactDict inerts workItem fl cls xis loc
= do { instEnvs <- getInstEnvs
; let fd_eqns = improveFromInstEnv instEnvs
(mkClassPred cls xis, arising_sdoc)
- ; m <- rewriteWithFunDeps fd_eqns fl
- ; case m of
- Just fd_work ->
- do { emitFDWorkAsDerived fd_work depth
- ; return SomeTopInt { tir_rule = "Dict/Top (fundeps)"
- , tir_new_item = ContinueWith workItem } }
- Nothing
- | isWanted fl
- -> do { lkup_inst_res <- matchClassInst inerts cls xis (getWantedLoc fl)
- ; case lkup_inst_res of
- GenInst wtvs ev_term -> do { addSolvedDict fl
- ; doSolveFromInstance wtvs ev_term }
- NoInstance -> return NoTopInt }
- | otherwise
- -> return NoTopInt }
+ ; fd_work <- rewriteWithFunDeps fd_eqns loc
+ ; if not (null fd_work) then
+ do { updWorkListTcS (extendWorkListEqs fd_work)
+ ; return SomeTopInt { tir_rule = "Dict/Top (fundeps)"
+ , tir_new_item = ContinueWith workItem } }
+ else -- No fundeps
+ if isWanted fl then
+ do { lkup_inst_res <- matchClassInst inerts cls xis loc
+ ; case lkup_inst_res of
+ GenInst wtvs ev_term -> do { addSolvedDict fl
+ ; doSolveFromInstance wtvs ev_term }
+ NoInstance -> return NoTopInt }
+ else
+ return NoTopInt }
where
- arising_sdoc
- | isGiven fl = pprArisingAt $ getGivenLoc fl
- | otherwise = pprArisingAt $ getWantedLoc fl
-
+ arising_sdoc = pprArisingAt loc
dict_id = ctEvId fl
doSolveFromInstance :: [CtEvidence] -> EvTerm -> TcS TopInteractResult
@@ -1452,8 +1425,8 @@ doTopReactDict inerts workItem fl cls xis depth
ppr dict_id
; setEvBind dict_id ev_term
; let mk_new_wanted ev
- = CNonCanonical { cc_ev = ev
- , cc_depth = depth + 1 }
+ = CNonCanonical { cc_ev = ev
+ , cc_loc = bumpCtLocDepth loc }
; updWorkListTcS (extendWorkListCts (map mk_new_wanted evs))
; return $
SomeTopInt { tir_rule = "Dict/Top (solved, more work)"
@@ -1461,8 +1434,8 @@ doTopReactDict inerts workItem fl cls xis depth
--------------------
doTopReactFunEq :: Ct -> CtEvidence -> TyCon -> [Xi] -> Xi
- -> SubGoalDepth -> TcS TopInteractResult
-doTopReactFunEq ct fl fun_tc args xi d
+ -> CtLoc -> TcS TopInteractResult
+doTopReactFunEq ct fl fun_tc args xi loc
= ASSERT (isSynFamilyTyCon fun_tc) -- No associated data families have
-- reached that far
@@ -1498,7 +1471,7 @@ doTopReactFunEq ct fl fun_tc args xi d
; case ctevs of
[ctev] -> updWorkListTcS $ extendWorkListEq $
CNonCanonical { cc_ev = ctev
- , cc_depth = d+1 }
+ , cc_loc = bumpCtLocDepth loc }
ctevs -> -- No subgoal (because it's cached)
ASSERT( null ctevs) return ()
; return $ SomeTopInt { tir_rule = str
@@ -1714,7 +1687,7 @@ data LookupInstResult
= NoInstance
| GenInst [CtEvidence] EvTerm
-matchClassInst :: InertSet -> Class -> [Type] -> WantedLoc -> TcS LookupInstResult
+matchClassInst :: InertSet -> Class -> [Type] -> CtLoc -> TcS LookupInstResult
matchClassInst _ clas [ _, ty ] _
| className clas == singIClassName
@@ -1757,7 +1730,7 @@ matchClassInst inerts clas tys loc
; if null theta then
return (GenInst [] (EvDFunApp dfun_id tys []))
else do
- { evc_vars <- instDFunConstraints loc theta
+ { evc_vars <- instDFunConstraints theta
; let new_ev_vars = freshGoals evc_vars
-- new_ev_vars are only the real new variables that can be emitted
dfun_app = EvDFunApp dfun_id tys (getEvTerms evc_vars)
diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs
index eefe3d5b6e..15cfdd4690 100644
--- a/compiler/typecheck/TcMType.lhs
+++ b/compiler/typecheck/TcMType.lhs
@@ -66,7 +66,7 @@ module TcMType (
zonkTcType, zonkTcTypes, zonkTcThetaType,
zonkTcKind, defaultKindVarToStar,
- zonkEvVar, zonkWC, zonkId, zonkCt,
+ zonkEvVar, zonkWC, zonkId, zonkCt, zonkSkolemInfo,
tcGetGlobalTyVars,
) where
@@ -623,17 +623,17 @@ zonkImplication implic@(Implic { ic_untch = untch
, ic_skols = skols
, ic_given = given
, ic_wanted = wanted
- , ic_loc = loc })
+ , ic_info = info })
= do { skols' <- mapM zonkTcTyVarBndr skols -- Need to zonk their kinds!
-- as Trac #7230 showed
; given' <- mapM zonkEvVar given
- ; loc' <- zonkGivenLoc loc
+ ; info' <- zonkSkolemInfo info
; wanted' <- zonkWCRec binds_var untch wanted
; return (implic { ic_skols = skols'
, ic_given = given'
, ic_fsks = [] -- Zonking removes all FlatSkol tyvars
, ic_wanted = wanted'
- , ic_loc = loc' }) }
+ , ic_info = info' }) }
zonkEvVar :: EvVar -> TcM EvVar
zonkEvVar var = do { ty' <- zonkTcType (varType var)
@@ -643,7 +643,8 @@ zonkEvVar var = do { ty' <- zonkTcType (varType var)
zonkWC :: EvBindsVar -- May add new bindings for wanted family equalities in here
-> WantedConstraints -> TcM WantedConstraints
zonkWC binds_var wc
- = zonkWCRec binds_var noUntouchables wc
+ = do { untch <- getUntouchables
+ ; zonkWCRec binds_var untch wc }
zonkWCRec :: EvBindsVar
-> Untouchables
@@ -732,13 +733,12 @@ zonkCt ct
| otherwise = do { fl' <- zonkCtEvidence (cc_ev ct)
; return $
CNonCanonical { cc_ev = fl'
- , cc_depth = cc_depth ct } }
+ , cc_loc = cc_loc ct } }
zonkCtEvidence :: CtEvidence -> TcM CtEvidence
-zonkCtEvidence ctev@(CtGiven { ctev_gloc = loc, ctev_pred = pred })
- = do { loc' <- zonkGivenLoc loc
- ; pred' <- zonkTcType pred
- ; return (ctev { ctev_gloc = loc', ctev_pred = pred'}) }
+zonkCtEvidence ctev@(CtGiven { ctev_pred = pred })
+ = do { pred' <- zonkTcType pred
+ ; return (ctev { ctev_pred = pred'}) }
zonkCtEvidence ctev@(CtWanted { ctev_pred = pred })
= do { pred' <- zonkTcType pred
; return (ctev { ctev_pred = pred' }) }
@@ -746,12 +746,6 @@ zonkCtEvidence ctev@(CtDerived { ctev_pred = pred })
= do { pred' <- zonkTcType pred
; return (ctev { ctev_pred = pred' }) }
-zonkGivenLoc :: GivenLoc -> TcM GivenLoc
--- GivenLocs may have unification variables inside them!
-zonkGivenLoc (CtLoc skol_info lcl)
- = do { skol_info' <- zonkSkolemInfo skol_info
- ; return (CtLoc skol_info' lcl) }
-
zonkSkolemInfo :: SkolemInfo -> TcM SkolemInfo
zonkSkolemInfo (SigSkol cx ty) = do { ty' <- zonkTcType ty
; return (SigSkol cx ty') }
diff --git a/compiler/typecheck/TcRnMonad.lhs b/compiler/typecheck/TcRnMonad.lhs
index 5da628aa39..610ef45178 100644
--- a/compiler/typecheck/TcRnMonad.lhs
+++ b/compiler/typecheck/TcRnMonad.lhs
@@ -815,13 +815,14 @@ updCtxt upd = updLclEnv (\ env@(TcLclEnv { tcl_ctxt = ctxt }) ->
popErrCtxt :: TcM a -> TcM a
popErrCtxt = updCtxt (\ msgs -> case msgs of { [] -> []; (_ : ms) -> ms })
-getCtLoc :: orig -> TcM (CtLoc orig)
+getCtLoc :: CtOrigin -> TcM CtLoc
getCtLoc origin
- = do { env <- getLclEnv ; return (CtLoc origin env) }
+ = do { env <- getLclEnv
+ ; return (CtLoc { ctl_origin = origin, ctl_env = env, ctl_depth = 0 }) }
-setCtLoc :: CtLoc orig -> TcM a -> TcM a
+setCtLoc :: CtLoc -> TcM a -> TcM a
-- Set the SrcSpan and error context from the CtLoc
-setCtLoc (CtLoc _ lcl) thing_inside
+setCtLoc (CtLoc { ctl_env = lcl }) thing_inside
= updLclEnv (\env -> env { tcl_loc = tcl_loc lcl
, tcl_bndrs = tcl_bndrs lcl
, tcl_ctxt = tcl_ctxt lcl })
diff --git a/compiler/typecheck/TcRnTypes.lhs b/compiler/typecheck/TcRnTypes.lhs
index 2fdfb22e98..e72fda6062 100644
--- a/compiler/typecheck/TcRnTypes.lhs
+++ b/compiler/typecheck/TcRnTypes.lhs
@@ -54,25 +54,26 @@ module TcRnTypes(
isCDictCan_Maybe, isCFunEqCan_Maybe,
isCIrredEvCan, isCNonCanonical, isWantedCt, isDerivedCt,
isGivenCt, isHoleCt,
- ctWantedLoc, ctEvidence,
+ ctEvidence,
SubGoalDepth, mkNonCanonical, mkNonCanonicalCt,
- ctPred, ctEvPred, ctEvTerm, ctEvId, ctEvEnv,
+ ctPred, ctEvPred, ctEvTerm, ctEvId,
WantedConstraints(..), insolubleWC, emptyWC, isEmptyWC,
andWC, unionsWC, addFlats, addImplics, mkFlatWC, addInsols,
Implication(..),
- CtLoc(..), ctLocSpan, ctLocEnv, ctLocOrigin, setCtLocOrigin,
+ CtLoc(..), ctLocSpan, ctLocEnv, ctLocOrigin,
+ ctLocDepth, bumpCtLocDepth,
+ setCtLocOrigin,
CtOrigin(..), EqOrigin(..),
- WantedLoc, GivenLoc, pushErrCtxt,
- pushErrCtxtSameOrigin,
+ pushErrCtxt, pushErrCtxtSameOrigin,
SkolemInfo(..),
- CtEvidence(..), pprFlavorArising,
+ CtEvidence(..),
mkGivenLoc,
isWanted, isGiven,
- isDerived, getWantedLoc, getGivenLoc, canSolve, canRewrite,
+ isDerived, canSolve, canRewrite,
CtFlavour(..), ctEvFlavour, ctFlavour,
-- Pretty printing
@@ -118,7 +119,6 @@ import DynFlags
import Outputable
import ListSetOps
import FastString
-import Util
import Data.Set (Set)
\end{code}
@@ -848,9 +848,6 @@ type Xi = Type -- In many comments, "xi" ranges over Xi
type Cts = Bag Ct
-type SubGoalDepth = Int -- An ever increasing number used to restrict
- -- simplifier iterations. Bounded by -fcontext-stack.
-
data Ct
-- Atomic canonical constraints
= CDictCan { -- e.g. Num xi
@@ -858,8 +855,7 @@ data Ct
cc_class :: Class,
cc_tyargs :: [Xi],
- cc_depth :: SubGoalDepth -- Simplification depth of this constraint
- -- See Note [WorkList]
+ cc_loc :: CtLoc
}
| CIrredEvCan { -- These stand for yet-unknown predicates
@@ -868,7 +864,7 @@ data Ct
-- Since, if it were a type constructor application, that'd make the
-- whole constraint a CDictCan, or CTyEqCan. And it can't be
-- a type family application either because it's a Xi type.
- cc_depth :: SubGoalDepth -- See Note [WorkList]
+ cc_loc :: CtLoc
}
| CTyEqCan { -- tv ~ xi (recall xi means function free)
@@ -880,8 +876,7 @@ data Ct
cc_ev :: CtEvidence, -- See Note [Ct/evidence invariant]
cc_tyvar :: TcTyVar,
cc_rhs :: Xi,
-
- cc_depth :: SubGoalDepth -- See Note [WorkList]
+ cc_loc :: CtLoc
}
| CFunEqCan { -- F xis ~ xi
@@ -893,21 +888,20 @@ data Ct
cc_rhs :: Xi, -- *never* over-saturated (because if so
-- we should have decomposed)
- cc_depth :: SubGoalDepth -- See Note [WorkList]
+ cc_loc :: CtLoc
}
| CNonCanonical { -- See Note [NonCanonical Semantics]
- cc_ev :: CtEvidence,
- cc_depth :: SubGoalDepth
+ cc_ev :: CtEvidence,
+ cc_loc :: CtLoc
}
| CHoleCan {
cc_ev :: CtEvidence,
cc_hole_ty :: TcTauType, -- Not a Xi! See same not as above
- cc_depth :: SubGoalDepth -- See Note [WorkList]
+ cc_loc :: CtLoc
}
-
\end{code}
Note [Ct/evidence invariant]
@@ -919,11 +913,11 @@ This holds by construction; look at the unique place where CDictCan is
built (in TcCanonical)
\begin{code}
-mkNonCanonical :: CtEvidence -> Ct
-mkNonCanonical flav = CNonCanonical { cc_ev = flav, cc_depth = 0}
+mkNonCanonical :: CtLoc -> CtEvidence -> Ct
+mkNonCanonical loc ev = CNonCanonical { cc_ev = ev, cc_loc = loc }
mkNonCanonicalCt :: Ct -> Ct
-mkNonCanonicalCt ct = CNonCanonical { cc_ev = cc_ev ct, cc_depth = 0}
+mkNonCanonicalCt ct = CNonCanonical { cc_ev = cc_ev ct, cc_loc = cc_loc ct }
ctEvidence :: Ct -> CtEvidence
ctEvidence = cc_ev
@@ -949,11 +943,6 @@ dropDerivedWC wc@(WC { wc_flat = flats })
%************************************************************************
\begin{code}
-ctWantedLoc :: Ct -> WantedLoc
--- Only works for Wanted/Derived
-ctWantedLoc ct = ASSERT2( not (isGiven (cc_ev ct)), ppr ct )
- getWantedLoc (cc_ev ct)
-
isWantedCt :: Ct -> Bool
isWantedCt = isWanted . cc_ev
@@ -996,8 +985,7 @@ isHoleCt _ = False
\begin{code}
instance Outputable Ct where
- ppr ct = ppr (cc_ev ct) <+>
- braces (ppr (cc_depth ct)) <+> parens (text ct_sort)
+ ppr ct = ppr (cc_ev ct) <+> parens (text ct_sort)
where ct_sort = case ct of
CTyEqCan {} -> "CTyEqCan"
CFunEqCan {} -> "CFunEqCan"
@@ -1113,7 +1101,7 @@ data Implication
-- free in the environment
ic_skols :: [TcTyVar], -- Introduced skolems
- -- See Note [Skolems in an implication]
+ ic_info :: SkolemInfo, -- See Note [Skolems in an implication]
-- See Note [Shadowing in a constraint]
ic_fsks :: [TcTyVar], -- Extra flatten-skolems introduced by the flattening
@@ -1122,9 +1110,9 @@ data Implication
ic_given :: [EvVar], -- Given evidence variables
-- (order does not matter)
- ic_loc :: GivenLoc, -- Binding location of the implication,
- -- which is also the location of all the
- -- given evidence variables
+ ic_env :: TcLclEnv, -- Gives the source location and error context
+ -- for the implicatdion, and hence for all the
+ -- given evidence variables
ic_wanted :: WantedConstraints, -- The wanted
ic_insol :: Bool, -- True iff insolubleWC ic_wanted is true
@@ -1137,7 +1125,7 @@ instance Outputable Implication where
ppr (Implic { ic_untch = untch, ic_skols = skols, ic_fsks = fsks
, ic_given = given
, ic_wanted = wanted
- , ic_binds = binds, ic_loc = loc })
+ , ic_binds = binds, ic_info = info })
= ptext (sLit "Implic") <+> braces
(sep [ ptext (sLit "Untouchables = ") <+> ppr untch
, ptext (sLit "Skolems = ") <+> ppr skols
@@ -1145,8 +1133,7 @@ instance Outputable Implication where
, ptext (sLit "Given = ") <+> pprEvVars given
, ptext (sLit "Wanted = ") <+> ppr wanted
, ptext (sLit "Binds = ") <+> ppr binds
- , pprSkolInfo (ctLocOrigin loc)
- , ppr (ctLocSpan loc) ])
+ , pprSkolInfo info ])
\end{code}
Note [Shadowing in a constraint]
@@ -1227,7 +1214,7 @@ pprWantedsWithLocs wcs
%************************************************************************
%* *
- CtLoc
+ CtEvidence
%* *
%************************************************************************
@@ -1239,19 +1226,16 @@ may be un-zonked.
\begin{code}
data CtEvidence
- = CtGiven { ctev_gloc :: GivenLoc
- , ctev_pred :: TcPredType
+ = CtGiven { ctev_pred :: TcPredType
, ctev_evtm :: EvTerm } -- See Note [Evidence field of CtEvidence]
-- Truly given, not depending on subgoals
-- NB: Spontaneous unifications belong here
- | CtWanted { ctev_wloc :: WantedLoc
- , ctev_pred :: TcPredType
+ | CtWanted { ctev_pred :: TcPredType
, ctev_evar :: EvVar } -- See Note [Evidence field of CtEvidence]
-- Wanted goal
- | CtDerived { ctev_wloc :: WantedLoc
- , ctev_pred :: TcPredType }
+ | CtDerived { ctev_pred :: TcPredType }
-- A goal that we don't really have to solve and can't immediately
-- rewrite anything other than a derived (there's no evidence!)
-- but if we do manage to solve it may help in solving other goals.
@@ -1276,11 +1260,6 @@ ctEvTerm (CtWanted { ctev_evar = ev }) = EvId ev
ctEvTerm ctev@(CtDerived {}) = pprPanic "ctEvTerm: derived constraint cannot have id"
(ppr ctev)
-ctEvEnv :: CtEvidence -> TcLclEnv
-ctEvEnv (CtWanted { ctev_wloc = loc }) = ctLocEnv loc
-ctEvEnv (CtDerived { ctev_wloc = loc }) = ctLocEnv loc
-ctEvEnv (CtGiven { ctev_gloc = loc }) = ctLocEnv loc
-
ctEvId :: CtEvidence -> TcId
ctEvId (CtWanted { ctev_evar = ev }) = ev
ctEvId ctev = pprPanic "ctEvId:" (ppr ctev)
@@ -1297,19 +1276,6 @@ instance Outputable CtEvidence where
CtDerived {} -> ptext (sLit "[D]") <+> text "_" <+> ppr_pty
where ppr_pty = dcolon <+> ppr (ctEvPred fl)
-getWantedLoc :: CtEvidence -> WantedLoc
--- Precondition: Wanted or Derived
-getWantedLoc fl = ctev_wloc fl
-
-getGivenLoc :: CtEvidence -> GivenLoc
--- Precondition: Given
-getGivenLoc fl = ctev_gloc fl
-
-pprFlavorArising :: CtEvidence -> SDoc
-pprFlavorArising (CtGiven { ctev_gloc = gl }) = pprArisingAt gl
-pprFlavorArising ctev = pprArisingAt (ctev_wloc ctev)
-
-
isWanted :: CtEvidence -> Bool
isWanted (CtWanted {}) = True
isWanted _ = False
@@ -1343,9 +1309,6 @@ canRewrite :: CtFlavour -> CtFlavour -> Bool
-- canRewrite ct1 ct2
-- The equality constraint ct1 can be used to rewrite inside ct2
canRewrite = canSolve
-
-mkGivenLoc :: WantedLoc -> SkolemInfo -> GivenLoc
-mkGivenLoc wl sk = setCtLocOrigin wl sk
\end{code}
%************************************************************************
@@ -1360,35 +1323,49 @@ dictionaries don't appear in the original source code.
type will evolve...
\begin{code}
-data CtLoc orig = CtLoc orig TcLclEnv
+data CtLoc = CtLoc { ctl_origin :: CtOrigin
+ , ctl_env :: TcLclEnv
+ , ctl_depth :: SubGoalDepth }
-- The TcLclEnv includes particularly
-- source location: tcl_loc :: SrcSpan
-- context: tcl_ctxt :: [ErrCtxt]
-- binder stack: tcl_bndrs :: [TcIdBinders]
-type WantedLoc = CtLoc CtOrigin -- Instantiation for wanted constraints
-type GivenLoc = CtLoc SkolemInfo -- Instantiation for given constraints
+type SubGoalDepth = Int -- An ever increasing number used to restrict
+ -- simplifier iterations. Bounded by -fcontext-stack.
+ -- See Note [WorkList]
-ctLocEnv :: CtLoc o -> TcLclEnv
-ctLocEnv (CtLoc _ lcl) = lcl
+mkGivenLoc :: SkolemInfo -> TcLclEnv -> CtLoc
+mkGivenLoc skol_info env = CtLoc { ctl_origin = GivenOrigin skol_info
+ , ctl_env = env
+ , ctl_depth = 0 }
-ctLocSpan :: CtLoc o -> SrcSpan
-ctLocSpan (CtLoc _ lcl) = tcl_loc lcl
+ctLocEnv :: CtLoc -> TcLclEnv
+ctLocEnv = ctl_env
-ctLocOrigin :: CtLoc o -> o
-ctLocOrigin (CtLoc o _) = o
+ctLocDepth :: CtLoc -> SubGoalDepth
+ctLocDepth = ctl_depth
-setCtLocOrigin :: CtLoc o -> o' -> CtLoc o'
-setCtLocOrigin (CtLoc _ lcl) o = CtLoc o lcl
+ctLocOrigin :: CtLoc -> CtOrigin
+ctLocOrigin = ctl_origin
-pushErrCtxt :: orig -> ErrCtxt -> CtLoc orig -> CtLoc orig
-pushErrCtxt o err (CtLoc _ lcl)
- = CtLoc o (lcl { tcl_ctxt = err : tcl_ctxt lcl })
+ctLocSpan :: CtLoc -> SrcSpan
+ctLocSpan (CtLoc { ctl_env = lcl}) = tcl_loc lcl
-pushErrCtxtSameOrigin :: ErrCtxt -> CtLoc orig -> CtLoc orig
+bumpCtLocDepth :: CtLoc -> CtLoc
+bumpCtLocDepth loc@(CtLoc { ctl_depth = d }) = loc { ctl_depth = d+1 }
+
+setCtLocOrigin :: CtLoc -> CtOrigin -> CtLoc
+setCtLocOrigin ctl orig = ctl { ctl_origin = orig }
+
+pushErrCtxt :: CtOrigin -> ErrCtxt -> CtLoc -> CtLoc
+pushErrCtxt o err loc@(CtLoc { ctl_env = lcl })
+ = loc { ctl_origin = o, ctl_env = lcl { tcl_ctxt = err : tcl_ctxt lcl } }
+
+pushErrCtxtSameOrigin :: ErrCtxt -> CtLoc -> CtLoc
-- Just add information w/o updating the origin!
-pushErrCtxtSameOrigin err (CtLoc o lcl)
- = CtLoc o (lcl { tcl_ctxt = err : tcl_ctxt lcl })
+pushErrCtxtSameOrigin err loc@(CtLoc { ctl_env = lcl })
+ = loc { ctl_env = lcl { tcl_ctxt = err : tcl_ctxt lcl } }
pprArising :: CtOrigin -> SDoc
-- Used for the main, top-level error message
@@ -1397,9 +1374,10 @@ pprArising (TypeEqOrigin {}) = empty
pprArising FunDepOrigin = empty
pprArising orig = text "arising from" <+> ppr orig
-pprArisingAt :: Outputable o => CtLoc o -> SDoc
-pprArisingAt (CtLoc o lcl) = sep [ text "arising from" <+> ppr o
- , text "at" <+> ppr (tcl_loc lcl)]
+pprArisingAt :: CtLoc -> SDoc
+pprArisingAt (CtLoc { ctl_origin = o, ctl_env = lcl})
+ = sep [ text "arising from" <+> ppr o
+ , text "at" <+> ppr (tcl_loc lcl)]
\end{code}
%************************************************************************
@@ -1491,9 +1469,11 @@ pprSkolInfo UnkSkol = WARN( True, text "pprSkolInfo: UnkSkol" ) ptext (sLit "Unk
%************************************************************************
\begin{code}
--- CtOrigin gives the origin of *wanted* constraints
data CtOrigin
- = OccurrenceOf Name -- Occurrence of an overloaded identifier
+ = GivenOrigin SkolemInfo
+
+ -- All the others are for *wanted* constraints
+ | OccurrenceOf Name -- Occurrence of an overloaded identifier
| AppOrigin -- An application of some kind
| SpecPragOrigin Name -- Specialisation pragma for identifier
@@ -1537,6 +1517,7 @@ instance Outputable CtOrigin where
ppr orig = pprO orig
pprO :: CtOrigin -> SDoc
+pprO (GivenOrigin sk) = ppr sk
pprO (OccurrenceOf name) = hsep [ptext (sLit "a use of"), quotes (ppr name)]
pprO AppOrigin = ptext (sLit "an application")
pprO (SpecPragOrigin name) = hsep [ptext (sLit "a specialisation pragma for"), quotes (ppr name)]
diff --git a/compiler/typecheck/TcRules.lhs b/compiler/typecheck/TcRules.lhs
index bc9c0b7816..1a569d02c7 100644
--- a/compiler/typecheck/TcRules.lhs
+++ b/compiler/typecheck/TcRules.lhs
@@ -177,7 +177,7 @@ tcRule (HsRule name act hs_bndrs lhs fv_lhs rhs fv_rhs)
])
-- Simplify the RHS constraints
- ; loc <- getCtLoc (RuleSkol name)
+ ; lcl_env <- getLclEnv
; rhs_binds_var <- newTcEvBinds
; emitImplication $ Implic { ic_untch = noUntouchables
, ic_skols = qtkvs
@@ -186,7 +186,8 @@ tcRule (HsRule name act hs_bndrs lhs fv_lhs rhs fv_rhs)
, ic_wanted = rhs_wanted
, ic_insol = insolubleWC rhs_wanted
, ic_binds = rhs_binds_var
- , ic_loc = loc }
+ , ic_info = RuleSkol name
+ , ic_env = lcl_env }
-- For the LHS constraints we must solve the remaining constraints
-- (a) so that we report insoluble ones
@@ -199,7 +200,8 @@ tcRule (HsRule name act hs_bndrs lhs fv_lhs rhs fv_rhs)
, ic_wanted = other_lhs_wanted
, ic_insol = insolubleWC other_lhs_wanted
, ic_binds = lhs_binds_var
- , ic_loc = loc }
+ , ic_info = RuleSkol name
+ , ic_env = lcl_env }
; return (HsRule name act
(map (RuleBndr . noLoc) (qtkvs ++ tpl_ids))
diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs
index 7560b80f11..89706cd512 100644
--- a/compiler/typecheck/TcSMonad.lhs
+++ b/compiler/typecheck/TcSMonad.lhs
@@ -25,10 +25,10 @@ module TcSMonad (
emitInsoluble,
isWanted, isDerived,
- isGivenCt, isWantedCt, isDerivedCt, pprFlavorArising,
+ isGivenCt, isWantedCt, isDerivedCt,
canRewrite, canSolve,
- mkGivenLoc, ctWantedLoc,
+ mkGivenLoc,
TcS, runTcS, runTcSWithEvBinds, failTcS, panicTcS, traceTcS, -- Basic functionality
traceFireTcS, bumpStepCountTcS,
@@ -82,7 +82,7 @@ module TcSMonad (
compatKind, mkKindErrorCtxtTcS,
- Untouchables, isTouchableMetaTyVarTcS,
+ Untouchables, isTouchableMetaTyVarTcS, isFilledMetaTyVar_maybe,
getDefaultInfo, getDynFlags,
@@ -701,8 +701,7 @@ prepareInertsForImplications is
| otherwise = funeq { cc_ev = given_ev }
where
ev = ctEvidence funeq
- given_ev = CtGiven { ctev_gloc = setCtLocOrigin (ctev_wloc ev) UnkSkol
- , ctev_evtm = EvId (ctev_evar ev)
+ given_ev = CtGiven { ctev_evtm = EvId (ctev_evar ev)
, ctev_pred = ctev_pred ev }
\end{code}
@@ -960,13 +959,13 @@ bumpStepCountTcS = TcS $ \env -> do { let ref = tcs_count env
; n <- TcM.readTcRef ref
; TcM.writeTcRef ref (n+1) }
-traceFireTcS :: SubGoalDepth -> SDoc -> TcS ()
+traceFireTcS :: Ct -> SDoc -> TcS ()
-- Dump a rule-firing trace
-traceFireTcS depth doc
+traceFireTcS ct doc
= TcS $ \env ->
TcM.ifDOptM Opt_D_dump_cs_trace $
do { n <- TcM.readTcRef (tcs_count env)
- ; let msg = int n <> brackets (int depth) <+> doc
+ ; let msg = int n <> brackets (int (ctLocDepth (cc_loc ct))) <+> doc
; TcM.dumpTcRn msg }
runTcS :: TcS a -- What to run
@@ -1221,7 +1220,7 @@ getGblEnv = wrapTcS $ TcM.getGblEnv
-- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> TcS ()
+checkWellStagedDFun :: PredType -> DFunId -> CtLoc -> TcS ()
checkWellStagedDFun pred dfun_id loc
= wrapTcS $ TcM.setCtLoc loc $
do { use_stage <- TcM.getStage
@@ -1237,6 +1236,17 @@ isTouchableMetaTyVarTcS :: TcTyVar -> TcS Bool
isTouchableMetaTyVarTcS tv
= do { untch <- getUntouchables
; return $ isTouchableMetaTyVar untch tv }
+
+isFilledMetaTyVar_maybe :: TcTyVar -> TcS (Maybe Type)
+isFilledMetaTyVar_maybe tv
+ = ASSERT( isTcTyVar tv )
+ case tcTyVarDetails tv of
+ MetaTv { mtv_ref = ref }
+ -> do { cts <- wrapTcS (TcM.readTcRef ref)
+ ; case cts of
+ Indirect ty -> return (Just ty)
+ Flexi -> return Nothing }
+ _ -> return Nothing
\end{code}
Note [Do not add duplicate derived insolubles]
@@ -1385,17 +1395,17 @@ setEvBind the_ev tm
; tc_evbinds <- getTcEvBinds
; wrapTcS $ TcM.addTcEvBind tc_evbinds the_ev tm }
-newGivenEvVar :: GivenLoc -> TcPredType -> EvTerm -> TcS CtEvidence
+newGivenEvVar :: TcPredType -> EvTerm -> TcS CtEvidence
-- Make a new variable of the given PredType,
-- immediately bind it to the given term
-- and return its CtEvidence
-newGivenEvVar gloc pred rhs
+newGivenEvVar pred rhs
= do { new_ev <- wrapTcS $ TcM.newEvVar pred
; setEvBind new_ev rhs
- ; return (CtGiven { ctev_gloc = gloc, ctev_pred = pred, ctev_evtm = EvId new_ev }) }
+ ; return (CtGiven { ctev_pred = pred, ctev_evtm = EvId new_ev }) }
-newWantedEvVar :: WantedLoc -> TcPredType -> TcS MaybeNew
-newWantedEvVar loc pty
+newWantedEvVar :: TcPredType -> TcS MaybeNew
+newWantedEvVar pty
= do { mb_ct <- lookupInInerts pty
; case mb_ct of
Just ctev | not (isDerived ctev)
@@ -1403,23 +1413,21 @@ newWantedEvVar loc pty
; return (Cached (ctEvTerm ctev)) }
_ -> do { new_ev <- wrapTcS $ TcM.newEvVar pty
; traceTcS "newWantedEvVar/cache miss" $ ppr new_ev
- ; let ctev = CtWanted { ctev_wloc = loc
- , ctev_pred = pty
+ ; let ctev = CtWanted { ctev_pred = pty
, ctev_evar = new_ev }
; return (Fresh ctev) } }
-newDerived :: WantedLoc -> TcPredType -> TcS (Maybe CtEvidence)
+newDerived :: TcPredType -> TcS (Maybe CtEvidence)
-- Returns Nothing if cached,
-- Just pred if not cached
-newDerived loc pty
+newDerived pty
= do { mb_ct <- lookupInInerts pty
; return (case mb_ct of
Just {} -> Nothing
- Nothing -> Just (CtDerived { ctev_wloc = loc
- , ctev_pred = pty })) }
+ Nothing -> Just (CtDerived { ctev_pred = pty })) }
-instDFunConstraints :: WantedLoc -> TcThetaType -> TcS [MaybeNew]
-instDFunConstraints wl = mapM (newWantedEvVar wl)
+instDFunConstraints :: TcThetaType -> TcS [MaybeNew]
+instDFunConstraints = mapM newWantedEvVar
\end{code}
@@ -1468,18 +1476,18 @@ xCtFlavor :: CtEvidence -- Original flavor
-> XEvTerm -- Instructions about how to manipulate evidence
-> TcS [CtEvidence]
-xCtFlavor (CtGiven { ctev_gloc = gl, ctev_evtm = tm }) ptys xev
+xCtFlavor (CtGiven { ctev_evtm = tm }) ptys xev
= ASSERT( equalLength ptys (ev_decomp xev tm) )
- zipWithM (newGivenEvVar gl) ptys (ev_decomp xev tm)
+ zipWithM newGivenEvVar ptys (ev_decomp xev tm)
-- See Note [Bind new Givens immediately]
-xCtFlavor ctev@(CtWanted { ctev_wloc = wl, ctev_evar = evar }) ptys xev
- = do { new_evars <- mapM (newWantedEvVar wl) ptys
+xCtFlavor ctev@(CtWanted { ctev_evar = evar }) ptys xev
+ = do { new_evars <- mapM newWantedEvVar ptys
; setEvBind evar (ev_comp xev (getEvTerms new_evars))
; return (freshGoals new_evars) }
-xCtFlavor (CtDerived { ctev_wloc = wl }) ptys _xev
- = do { ders <- mapM (newDerived wl) ptys
+xCtFlavor (CtDerived {}) ptys _xev
+ = do { ders <- mapM newDerived ptys
; return (catMaybes ders) }
-----------------------------
@@ -1514,16 +1522,16 @@ Main purpose: create new evidence for new_pred;
-- NB: this allows us to sneak away with ``error'' thunks for
-- coercions that come from derived ids (which don't exist!)
-rewriteCtFlavor (CtDerived { ctev_wloc = wl }) pty_new _co
- = newDerived wl pty_new
+rewriteCtFlavor (CtDerived {}) pty_new _co
+ = newDerived pty_new
-rewriteCtFlavor (CtGiven { ctev_gloc = gl, ctev_evtm = old_tm }) pty_new co
- = do { new_ev <- newGivenEvVar gl pty_new new_tm -- See Note [Bind new Givens immediately]
+rewriteCtFlavor (CtGiven { ctev_evtm = old_tm }) pty_new co
+ = do { new_ev <- newGivenEvVar pty_new new_tm -- See Note [Bind new Givens immediately]
; return (Just new_ev) }
where
new_tm = mkEvCast old_tm (mkTcSymCo co) -- mkEvCase optimises ReflCo
-rewriteCtFlavor ctev@(CtWanted { ctev_wloc = wl, ctev_evar = evar, ctev_pred = old_pred })
+rewriteCtFlavor ctev@(CtWanted { ctev_evar = evar, ctev_pred = old_pred })
new_pred co
| isTcReflCo co -- If just reflexivity then you may re-use the same variable
= return (Just (if old_pred `eqType` new_pred
@@ -1536,7 +1544,7 @@ rewriteCtFlavor ctev@(CtWanted { ctev_wloc = wl, ctev_evar = evar, ctev_pred = o
-- then retain the old type, so that error messages come out mentioning synonyms
| otherwise
- = do { new_evar <- newWantedEvVar wl new_pred
+ = do { new_evar <- newWantedEvVar new_pred
; setEvBind evar (mkEvCast (getEvTerm new_evar) co)
; case new_evar of
Fresh ctev -> return (Just ctev)
@@ -1592,7 +1600,7 @@ matchFam tycon args = wrapTcS $ tcLookupFamInst tycon args
-- Deferring forall equalities as implications
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-deferTcSForAllEq :: (WantedLoc,EvVar) -- Original wanted equality flavor
+deferTcSForAllEq :: (CtLoc,EvVar) -- Original wanted equality flavor
-> ([TyVar],TcType) -- ForAll tvs1 body1
-> ([TyVar],TcType) -- ForAll tvs2 body2
-> TcS ()
@@ -1604,16 +1612,15 @@ deferTcSForAllEq (loc,orig_ev) (tvs1,body1) (tvs2,body2)
phi1 = Type.substTy subst1 body1
phi2 = Type.substTy (zipTopTvSubst tvs2 tys) body2
skol_info = UnifyForAllSkol skol_tvs phi1
- ; mev <- newWantedEvVar loc (mkTcEqPred phi1 phi2)
- ; untch <- getUntouchables
+ ; mev <- newWantedEvVar (mkTcEqPred phi1 phi2)
; coe_inside <- case mev of
Cached ev_tm -> return (evTermCoercion ev_tm)
Fresh ctev -> do { ev_binds_var <- wrapTcS $ TcM.newTcEvBinds
+ ; env <- wrapTcS $ TcM.getLclEnv
; let ev_binds = TcEvBinds ev_binds_var
- new_ct = mkNonCanonical ctev
+ new_ct = mkNonCanonical loc ctev
new_co = evTermCoercion (ctEvTerm ctev)
- new_untch = pushUntouchables untch
- ; loc <- wrapTcS $ TcM.getCtLoc skol_info
+ new_untch = pushUntouchables (tcl_untch env)
; let wc = WC { wc_flat = singleCt new_ct
, wc_impl = emptyBag
, wc_insol = emptyCts }
@@ -1624,7 +1631,8 @@ deferTcSForAllEq (loc,orig_ev) (tvs1,body1) (tvs2,body2)
, ic_wanted = wc
, ic_insol = False
, ic_binds = ev_binds_var
- , ic_loc = loc }
+ , ic_env = env
+ , ic_info = skol_info }
; updTcSImplics (consBag imp)
; return (TcLetCo ev_binds new_co) }
diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index c2eba23318..8afcb3e94b 100644
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@ -445,9 +445,8 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
-- Step 7) Emit an implication
; minimal_bound_ev_vars <- mapM TcMType.newEvVar minimal_flat_preds
- ; gloc <- getCtLoc skol_info
- ; untch <- TcRnMonad.getUntouchables
- ; let implic = Implic { ic_untch = pushUntouchables untch
+ ; lcl_env <- TcRnMonad.getLclEnv
+ ; let implic = Implic { ic_untch = pushUntouchables (tcl_untch lcl_env)
, ic_skols = qtvs_to_return
, ic_fsks = [] -- wanted_tansformed arose only from solveWanteds
-- hence no flatten-skolems (which come from givens)
@@ -455,7 +454,8 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
, ic_wanted = wanted_transformed
, ic_insol = False
, ic_binds = ev_binds_var
- , ic_loc = gloc }
+ , ic_info = skol_info
+ , ic_env = lcl_env }
; emitImplication implic
; traceTc "} simplifyInfer/produced residual implication for quantification" $
@@ -657,15 +657,19 @@ and does not fail if -fwarn-type-errors is on, so that we can continue
compilation. The errors are turned into warnings in `reportUnsolved`.
\begin{code}
-
solveWantedsTcMWithEvBinds :: EvBindsVar
-> WantedConstraints
-> (WantedConstraints -> TcS WantedConstraints)
-> TcM WantedConstraints
+-- Returns a *zonked* result
+-- We zonk when we finish primarily to un-flatten out any
+-- flatten-skolems etc introduced by canonicalisation of
+-- types involving type funuctions. Happily the result
+-- is typically much smaller than the input, indeed it is
+-- often empty.
solveWantedsTcMWithEvBinds ev_binds_var wc tcs_action
- = do { wc1 <- zonkWC ev_binds_var wc
- ; traceTc "solveWantedsTcMWithEvBinds" $ text "zonked wanted=" <+> ppr wc1
- ; wc2 <- runTcSWithEvBinds ev_binds_var (tcs_action wc1)
+ = do { traceTc "solveWantedsTcMWithEvBinds" $ text "wanted=" <+> ppr wc
+ ; wc2 <- runTcSWithEvBinds ev_binds_var (tcs_action wc)
; zonkWC ev_binds_var wc2 }
solveWantedsTcM :: WantedConstraints -> TcM (WantedConstraints, Bag EvBind)
@@ -781,7 +785,8 @@ solveImplication inerts
, ic_fsks = old_fsks
, ic_given = givens
, ic_wanted = wanteds
- , ic_loc = loc })
+ , ic_info = info
+ , ic_env = env })
=
do { traceTcS "solveImplication {" (ppr imp)
@@ -789,7 +794,7 @@ solveImplication inerts
-- NB: 'inerts' has empty inert_fsks
; (new_fsks, residual_wanted)
<- nestImplicTcS ev_binds untch inerts $
- do { solveInteractGiven loc old_fsks givens
+ do { solveInteractGiven (mkGivenLoc info env) old_fsks givens
; residual_wanted <- solve_wanteds wanteds
; more_fsks <- getFlattenSkols
; return (more_fsks ++ old_fsks, residual_wanted) }
@@ -1230,8 +1235,7 @@ newFlatWanteds orig theta
where
inst_to_wanted loc pty
= do { v <- TcMType.newWantedEvVar pty
- ; return $ mkNonCanonical $
+ ; return $ mkNonCanonical loc $
CtWanted { ctev_evar = v
- , ctev_wloc = loc
, ctev_pred = pty } }
\end{code}
diff --git a/compiler/typecheck/TcType.lhs b/compiler/typecheck/TcType.lhs
index cced76753d..758573dd46 100644
--- a/compiler/typecheck/TcType.lhs
+++ b/compiler/typecheck/TcType.lhs
@@ -587,20 +587,11 @@ tidyOpenTyVar env@(_, subst) tyvar
Nothing -> tidyTyVarBndr env tyvar -- Treat it as a binder
---------------
-tidyTyVarOcc :: TidyEnv -> TyVar -> Type
-tidyTyVarOcc env@(_, subst) tv
+tidyTyVarOcc :: TidyEnv -> TyVar -> TyVar
+tidyTyVarOcc (_, subst) tv
= case lookupVarEnv subst tv of
- Nothing -> expand tv
- Just tv' -> expand tv'
- where
- -- Expand FlatSkols, the skolems introduced by flattening process
- -- We don't want to show them in type error messages
- expand tv | isTcTyVar tv
- , FlatSkol ty <- tcTyVarDetails tv
- = WARN( True, text "I DON'T THINK THIS SHOULD EVER HAPPEN" <+> ppr tv <+> ppr ty )
- tidyType env ty
- | otherwise
- = TyVarTy tv
+ Nothing -> tv
+ Just tv' -> tv'
---------------
tidyTypes :: TidyEnv -> [Type] -> [Type]
@@ -609,7 +600,7 @@ tidyTypes env tys = map (tidyType env) tys
---------------
tidyType :: TidyEnv -> Type -> Type
tidyType _ (LitTy n) = LitTy n
-tidyType env (TyVarTy tv) = tidyTyVarOcc env tv
+tidyType env (TyVarTy tv) = TyVarTy (tidyTyVarOcc env tv)
tidyType env (TyConApp tycon tys) = let args = tidyTypes env tys
in args `seqList` TyConApp tycon args
tidyType env (AppTy fun arg) = (AppTy $! (tidyType env fun)) $! (tidyType env arg)
diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs
index 66fcd4ba1c..e34c220598 100644
--- a/compiler/typecheck/TcUnify.lhs
+++ b/compiler/typecheck/TcUnify.lhs
@@ -439,7 +439,7 @@ newImplication skol_info skol_tvs given thing_inside
return (emptyTcEvBinds, result)
else do
{ ev_binds_var <- newTcEvBinds
- ; loc <- getCtLoc skol_info
+ ; env <- getLclEnv
; emitImplication $ Implic { ic_untch = untch
, ic_skols = skol_tvs
, ic_fsks = []
@@ -447,7 +447,8 @@ newImplication skol_info skol_tvs given thing_inside
, ic_wanted = wanted
, ic_insol = insolubleWC wanted
, ic_binds = ev_binds_var
- , ic_loc = loc }
+ , ic_env = env
+ , ic_info = skol_info }
; return (TcEvBinds ev_binds_var, result) } }
\end{code}
@@ -533,9 +534,9 @@ uType_defer items ty1 ty2
= ASSERT( not (null items) )
do { eqv <- newEq ty1 ty2
; loc <- getCtLoc (TypeEqOrigin (last items))
- ; let ctev = CtWanted { ctev_wloc = loc, ctev_evar = eqv
+ ; let ctev = CtWanted { ctev_evar = eqv
, ctev_pred = mkTcEqPred ty1 ty2 }
- ; emitFlat $ mkNonCanonical ctev
+ ; emitFlat $ mkNonCanonical loc ctev
-- Error trace only
-- NB. do *not* call mkErrInfo unless tracing is on, because