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

Yet another major refactoring of the constraint solver

This is the result of Simon and Dimitrios doing a code walk through.
There is no change in behaviour, but the structure is much better.
Main changes:

* Given constraints contain an EvTerm not an EvVar

* Correspondingly, TcEvidence is a recursive types that uses
  EvTerms rather than EvVars

* Rename CtFlavor to CtEvidence

* Every CtEvidence has a ctev_pred field.  And use record fields
  consistently for CtEvidence

* The solved-constraint fields of InertSet (namely inert_solved and
  inert_solved_funeqs) contain CtEvidence, not Ct

There is a long cascade of follow-on changes.
parent 4f2dfe1e
......@@ -187,15 +187,7 @@ mkCast (Coercion e_co) co
-- The guard here checks that g has a (~#) on both sides,
-- otherwise decomposeCo fails. Can in principle happen
-- with unsafeCoerce
= Coercion new_co
where
-- g :: (s1 ~# s2) ~# (t1 ~# t2)
-- g1 :: s1 ~# t1
-- g2 :: s2 ~# t2
new_co = mkSymCo g1 `mkTransCo` e_co `mkTransCo` g2
[_reflk, g1, g2] = decomposeCo 3 co
-- Remember, (~#) :: forall k. k -> k -> *
-- so it takes *three* arguments, not two
= Coercion (mkCoCast e_co co)
mkCast (Cast expr co2) co
= ASSERT(let { Pair from_ty _to_ty = coercionKind co;
......
......@@ -726,39 +726,51 @@ sccEvBinds bs = stronglyConnCompFromEdgedVertices edges
edges = foldrBag ((:) . mk_node) [] bs
mk_node :: EvBind -> (EvBind, EvVar, [EvVar])
mk_node b@(EvBind var term) = (b, var, evVarsOfTerm term)
mk_node b@(EvBind var term) = (b, var, varSetElems (evVarsOfTerm term))
---------------------------------------
dsEvTerm :: MonadThings m => EvTerm -> m CoreExpr
dsEvTerm (EvId v) = return (Var v)
dsEvTerm (EvCast v co)
= return $ dsTcCoercion co $ mkCast (Var v) -- 'v' is always a lifted evidence variable so it is
-- unnecessary to call varToCoreExpr v here.
dsEvTerm (EvCast tm co)
= do { tm' <- dsEvTerm tm
; return $ dsTcCoercion co $ mkCast tm' }
-- 'v' is always a lifted evidence variable so it is
-- unnecessary to call varToCoreExpr v here.
dsEvTerm (EvKindCast v co)
= return $ dsTcCoercion co $ (\_ -> Var v)
= do { v' <- dsEvTerm v
; return $ dsTcCoercion co $ (\_ -> v') }
dsEvTerm (EvDFunApp df tys vars) = return (Var df `mkTyApps` tys `mkVarApps` vars)
dsEvTerm (EvDFunApp df tys tms) = do { tms' <- mapM dsEvTerm tms
; return (Var df `mkTyApps` tys `mkApps` tms') }
dsEvTerm (EvCoercion co) = return $ dsTcCoercion co mkEqBox
dsEvTerm (EvTupleSel v n)
= ASSERT( isTupleTyCon tc )
return $
Case (Var v) (mkWildValBinder (varType v)) (tys !! n) [(DataAlt dc, xs, Var v')]
where
(tc, tys) = splitTyConApp (evVarPred v)
Just [dc] = tyConDataCons_maybe tc
v' = v `setVarType` ty_want
xs = map mkWildValBinder tys_before ++ v' : map mkWildValBinder tys_after
(tys_before, ty_want:tys_after) = splitAt n tys
dsEvTerm (EvTupleMk vs) = return $ Var (dataConWorkId dc) `mkTyApps` tys `mkVarApps` vs
where dc = tupleCon ConstraintTuple (length vs)
tys = map varType vs
= do { tm' <- dsEvTerm v
; let scrut_ty = exprType tm'
(tc, tys) = splitTyConApp scrut_ty
Just [dc] = tyConDataCons_maybe tc
xs = mkTemplateLocals tys
the_x = xs !! n
; ASSERT( isTupleTyCon tc )
return $
Case tm' (mkWildValBinder scrut_ty) (idType the_x) [(DataAlt dc, xs, Var the_x)] }
dsEvTerm (EvTupleMk tms)
= do { tms' <- mapM dsEvTerm tms
; let tys = map exprType tms'
; return $ Var (dataConWorkId dc) `mkTyApps` tys `mkApps` tms' }
where
dc = tupleCon ConstraintTuple (length tms)
dsEvTerm (EvSuperClass d n)
= return $ Var sc_sel_id `mkTyApps` tys `App` Var d
= do { d' <- dsEvTerm d
; let (cls, tys) = getClassPredTys (exprType d')
sc_sel_id = classSCSelId cls n -- Zero-indexed
; return $ Var sc_sel_id `mkTyApps` tys `App` d' }
where
sc_sel_id = classSCSelId cls n -- Zero-indexed
(cls, tys) = getClassPredTys (evVarPred d)
dsEvTerm (EvDelayedError ty msg) = return $ Var errorId `mkTyApps` [ty] `mkApps` [litMsg]
where
errorId = rUNTIME_ERROR_ID
......@@ -816,6 +828,7 @@ ds_tc_coercion subst tc_co
go (TcNthCo n co) = mkNthCo n (go co)
go (TcInstCo co ty) = mkInstCo (go co) ty
go (TcLetCo bs co) = ds_tc_coercion (ds_co_binds bs) co
go (TcCastCo co1 co2) = mkCoCast (go co1) (go co2)
go (TcCoVarCo v) = ds_ev_id subst v
ds_co_binds :: TcEvBinds -> CvSubst
......
......@@ -83,10 +83,11 @@ emitWanteds :: CtOrigin -> TcThetaType -> TcM [EvVar]
emitWanteds origin theta = mapM (emitWanted origin) theta
emitWanted :: CtOrigin -> TcPredType -> TcM EvVar
emitWanted origin pred = do { loc <- getCtLoc origin
; ev <- newWantedEvVar pred
; emitFlat (mkNonCanonical (Wanted loc ev))
; return ev }
emitWanted origin pred
= do { loc <- getCtLoc origin
; ev <- newWantedEvVar pred
; emitFlat (mkNonCanonical (Wanted { ctev_wloc = loc, ctev_pred = pred, ctev_evar = ev }))
; return ev }
newMethodFromName :: CtOrigin -> Name -> TcRhoType -> TcM (HsExpr TcId)
-- Used when Name is the wired-in name for a wired-in class method,
......@@ -530,7 +531,7 @@ tyVarsOfCt (CFunEqCan { cc_tyargs = tys, cc_rhs = xi }) = tyVarsOfTypes (xi:tys)
tyVarsOfCt (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
tyVarsOfCt (CIPCan { cc_ip_ty = ty }) = tyVarsOfType ty
tyVarsOfCt (CIrredEvCan { cc_ty = ty }) = tyVarsOfType ty
tyVarsOfCt (CNonCanonical { cc_flavor = fl }) = tyVarsOfType (ctFlavPred fl)
tyVarsOfCt (CNonCanonical { cc_ev = fl }) = tyVarsOfType (ctEvPred fl)
tyVarsOfCDict :: Ct -> TcTyVarSet
tyVarsOfCDict (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
......@@ -564,24 +565,22 @@ tyVarsOfBag tvs_of = foldrBag (unionVarSet . tvs_of) emptyVarSet
---------------- Tidying -------------------------
tidyCt :: TidyEnv -> Ct -> Ct
-- Used only in error reporting
-- Also converts it to non-canonical
tidyCt env ct
= CNonCanonical { cc_flavor = tidy_flavor env (cc_flavor ct)
= CNonCanonical { cc_ev = tidy_flavor env (cc_ev ct)
, cc_depth = cc_depth ct }
where tidy_flavor :: TidyEnv -> CtFlavor -> CtFlavor
tidy_flavor env (Given { flav_gloc = gloc, flav_evar = evar })
= Given { flav_gloc = tidyGivenLoc env gloc
, flav_evar = tidyEvVar env evar }
tidy_flavor env (Solved { flav_gloc = gloc
, flav_evar = evar })
= Solved { flav_gloc = tidyGivenLoc env gloc
, flav_evar = tidyEvVar env evar }
tidy_flavor env (Wanted { flav_wloc = wloc
, flav_evar = evar })
= Wanted { flav_wloc = wloc -- Interesting: no tidying needed?
, flav_evar = tidyEvVar env evar }
tidy_flavor env (Derived { flav_wloc = wloc, flav_der_pty = pty })
= Derived { flav_wloc = wloc, flav_der_pty = tidyType env pty }
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@(Given { ctev_gloc = gloc, ctev_pred = pred })
= ctev { ctev_gloc = tidyGivenLoc env gloc
, ctev_pred = tidyType env pred }
tidy_flavor env ctev@(Wanted { ctev_pred = pred })
= ctev { ctev_pred = tidyType env pred }
tidy_flavor env ctev@(Derived { ctev_pred = pred })
= ctev { ctev_pred = tidyType env pred }
tidyEvVar :: TidyEnv -> EvVar -> EvVar
tidyEvVar env var = setVarType var (tidyType env (varType var))
......@@ -604,6 +603,10 @@ tidySkolemInfo env (UnifyForAllSkol skol_tvs ty)
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
......@@ -611,9 +614,9 @@ substCt subst ct
| pty <- ctPred ct
, sty <- substTy subst pty
= if sty `eqType` pty then
ct { cc_flavor = substFlavor subst (cc_flavor ct) }
ct { cc_ev = substFlavor subst (cc_ev ct) }
else
CNonCanonical { cc_flavor = substFlavor subst (cc_flavor ct)
CNonCanonical { cc_ev = substFlavor subst (cc_ev ct)
, cc_depth = cc_depth ct }
substWC :: TvSubst -> WantedConstraints -> WantedConstraints
......@@ -637,21 +640,16 @@ substImplication subst implic@(Implic { ic_skols = tvs
substEvVar :: TvSubst -> EvVar -> EvVar
substEvVar subst var = setVarType var (substTy subst (varType var))
substFlavor :: TvSubst -> CtFlavor -> CtFlavor
substFlavor subst (Given { flav_gloc = gloc, flav_evar = evar })
= Given { flav_gloc = substGivenLoc subst gloc
, flav_evar = substEvVar subst evar }
substFlavor subst (Solved { flav_gloc = gloc, flav_evar = evar })
= Solved { flav_gloc = substGivenLoc subst gloc
, flav_evar = substEvVar subst evar }
substFlavor subst (Wanted { flav_wloc = wloc, flav_evar = evar })
= Wanted { flav_wloc = wloc
, flav_evar = substEvVar subst evar }
substFlavor subst (Derived { flav_wloc = wloc, flav_der_pty = pty })
= Derived { flav_wloc = wloc
, flav_der_pty = substTy subst pty }
substFlavor :: TvSubst -> CtEvidence -> CtEvidence
substFlavor subst ctev@(Given { ctev_gloc = gloc, ctev_pred = pred })
= ctev { ctev_gloc = substGivenLoc subst gloc
, ctev_pred = substTy subst pred }
substFlavor subst ctev@(Wanted { ctev_pred = pred })
= ctev { ctev_pred = substTy subst pred }
substFlavor subst ctev@(Derived { ctev_pred = pty })
= ctev { ctev_pred = substTy subst pty }
substGivenLoc :: TvSubst -> GivenLoc -> GivenLoc
substGivenLoc subst (CtLoc skol span ctxt)
......
......@@ -173,26 +173,26 @@ EvBinds, so we are again good.
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
canonicalize :: Ct -> TcS StopOrContinue
canonicalize ct@(CNonCanonical { cc_flavor = fl, cc_depth = d })
canonicalize ct@(CNonCanonical { cc_ev = fl, cc_depth = d })
= do { traceTcS "canonicalize (non-canonical)" (ppr ct)
; {-# SCC "canEvVar" #-}
canEvVar d fl (classifyPredType (ctPred ct)) }
canonicalize (CDictCan { cc_depth = d
, cc_flavor = fl
, cc_ev = fl
, cc_class = cls
, cc_tyargs = xis })
= {-# SCC "canClass" #-}
canClass d fl cls xis -- Do not add any superclasses
canonicalize (CTyEqCan { cc_depth = d
, cc_flavor = fl
, cc_ev = fl
, cc_tyvar = tv
, cc_rhs = xi })
= {-# SCC "canEqLeafTyVarLeftRec" #-}
canEqLeafTyVarLeftRec d fl tv xi
canonicalize (CFunEqCan { cc_depth = d
, cc_flavor = fl
, cc_ev = fl
, cc_fun = fn
, cc_tyargs = xis1
, cc_rhs = xi2 })
......@@ -200,18 +200,18 @@ canonicalize (CFunEqCan { cc_depth = d
canEqLeafFunEqLeftRec d fl (fn,xis1) xi2
canonicalize (CIPCan { cc_depth = d
, cc_flavor = fl
, cc_ev = fl
, cc_ip_nm = nm
, cc_ip_ty = xi })
= canIP d fl nm xi
canonicalize (CIrredEvCan { cc_flavor = fl
canonicalize (CIrredEvCan { cc_ev = fl
, cc_depth = d
, cc_ty = xi })
= canIrred d fl xi
canEvVar :: SubGoalDepth
-> CtFlavor
-> CtEvidence
-> PredTree
-> TcS StopOrContinue
-- Called only for non-canonical EvVars
......@@ -233,15 +233,16 @@ canEvVar d fl pred_classifier
\begin{code}
canTuple :: SubGoalDepth -- Depth
-> CtFlavor -> [PredType] -> TcS StopOrContinue
-> CtEvidence -> [PredType] -> TcS StopOrContinue
canTuple d fl tys
= do { traceTcS "can_pred" (text "TuplePred!")
; let xcomp = EvTupleMk
xdecomp x = zipWith (\_ i -> EvTupleSel x i) tys [0..]
; xCtFlavor fl tys (XEvTerm xcomp xdecomp) what_next }
where what_next fls = mapM_ add_to_work fls >> return Stop
add_to_work fl = addToWork $ canEvVar d fl (classifyPredType (ctFlavPred fl))
; ctevs <- xCtFlavor fl tys (XEvTerm xcomp xdecomp)
; mapM_ add_to_work ctevs
; return Stop }
where
add_to_work fl = addToWork $ canEvVar d fl (classifyPredType (ctEvPred fl))
\end{code}
......@@ -253,7 +254,7 @@ canTuple d fl tys
\begin{code}
canIP :: SubGoalDepth -- Depth
-> CtFlavor
-> CtEvidence
-> IPName Name -> Type -> TcS StopOrContinue
-- Precondition: EvVar is implicit parameter evidence
canIP d fl nm ty
......@@ -264,7 +265,7 @@ canIP d fl nm ty
; mb <- rewriteCtFlavor fl xi co
; case mb of
Just new_fl -> let IPPred _ xi_in = classifyPredType xi
in continueWith $ CIPCan { cc_flavor = new_fl
in continueWith $ CIPCan { cc_ev = new_fl
, cc_ip_nm = nm, cc_ip_ty = xi_in
, cc_depth = d }
Nothing -> return Stop }
......@@ -291,7 +292,7 @@ flattened in the first place to facilitate comparing them.)
\begin{code}
canClass, canClassNC
:: SubGoalDepth -- Depth
-> CtFlavor
-> CtEvidence
-> Class -> [Type] -> TcS StopOrContinue
-- Precondition: EvVar is class evidence
......@@ -314,14 +315,14 @@ canClass d fl cls tys
; case mb of
Just new_fl ->
let (ClassPred cls xis_for_dict) = classifyPredType (ctFlavPred new_fl)
let (ClassPred cls xis_for_dict) = classifyPredType (ctEvPred new_fl)
in continueWith $
CDictCan { cc_flavor = new_fl
CDictCan { cc_ev = new_fl
, cc_tyargs = xis_for_dict, cc_class = cls, cc_depth = d }
Nothing -> return Stop }
emitSuperclasses :: Ct -> TcS StopOrContinue
emitSuperclasses ct@(CDictCan { cc_depth = d, cc_flavor = fl
emitSuperclasses ct@(CDictCan { cc_depth = d, cc_ev = fl
, 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.
......@@ -399,20 +400,19 @@ happen.
\begin{code}
newSCWorkFromFlavored :: SubGoalDepth -- Depth
-> CtFlavor -> Class -> [Xi] -> TcS ()
-> CtEvidence -> Class -> [Xi] -> TcS ()
-- Returns superclasses, see Note [Adding superclasses]
newSCWorkFromFlavored d flavor cls xis
| isDerived flavor
= return () -- Deriveds don't yield more superclasses because we will
-- add them transitively in the case of wanteds.
| isSolved flavor
= return ()
| isGiven flavor
= do { let sc_theta = immSuperClasses cls xis
xev = XEvTerm { ev_comp = panic "Can't compose for given!"
, ev_decomp = \x->zipWith (\_ i->EvSuperClass x i) sc_theta [0..] }
; xCtFlavor flavor sc_theta xev (emit_sc_flavs d) }
, ev_decomp = \x -> zipWith (\_ i -> EvSuperClass x i) sc_theta [0..] }
; ctevs <- xCtFlavor flavor sc_theta xev
; emit_sc_flavs d ctevs }
| isEmptyVarSet (tyVarsOfTypes xis)
= return () -- Wanteds/Derived with no variables yield no deriveds.
......@@ -422,15 +422,17 @@ newSCWorkFromFlavored d flavor cls xis
= do { let sc_rec_theta = transSuperClasses cls xis
impr_theta = filter is_improvement_pty sc_rec_theta
xev = panic "Derived's are not supposed to transform evidence!"
; xCtFlavor (Derived (flav_wloc flavor) (ctFlavPred flavor)) impr_theta xev $
emit_sc_flavs d }
der_ev = Derived { ctev_wloc = ctev_wloc flavor, ctev_pred = ctev_pred flavor }
; ctevs <- xCtFlavor der_ev impr_theta xev
; emit_sc_flavs d ctevs }
emit_sc_flavs :: SubGoalDepth -> [CtFlavor] -> TcS ()
emit_sc_flavs :: SubGoalDepth -> [CtEvidence] -> TcS ()
emit_sc_flavs d fls
= do { traceTcS "newSCWorkFromFlavored" $
text "Emitting superclass work:" <+> ppr sc_cts
; updWorkListTcS $ appendWorkListCt sc_cts }
where sc_cts = map (\fl -> CNonCanonical { cc_flavor = fl, cc_depth = d }) fls
where
sc_cts = map (\fl -> CNonCanonical { cc_ev = fl, cc_depth = d }) fls
is_improvement_pty :: PredType -> Bool
-- Either it's an equality, or has some functional dependency
......@@ -454,7 +456,7 @@ is_improvement_pty ty = go (classifyPredType ty)
\begin{code}
canIrred :: SubGoalDepth -- Depth
-> CtFlavor -> TcType -> TcS StopOrContinue
-> CtEvidence -> TcType -> TcS StopOrContinue
-- Precondition: ty not a tuple and no other evidence form
canIrred d fl ty
= do { traceTcS "can_pred" (text "IrredPred = " <+> ppr ty)
......@@ -468,9 +470,9 @@ canIrred d fl ty
Just new_fl
| no_flattening
-> continueWith $
CIrredEvCan { cc_flavor = new_fl, cc_ty = xi, cc_depth = d }
CIrredEvCan { cc_ev = new_fl, cc_ty = xi, cc_depth = d }
| otherwise
-> canEvVar d new_fl (classifyPredType (ctFlavPred new_fl))
-> canEvVar d new_fl (classifyPredType (ctEvPred new_fl))
Nothing -> return Stop }
\end{code}
......@@ -529,7 +531,7 @@ data FlattenMode = FMSubstOnly
-- Flatten a bunch of types all at once.
flattenMany :: SubGoalDepth -- Depth
-> FlattenMode
-> CtFlavor -> [Type] -> TcS ([Xi], [TcCoercion])
-> CtEvidence -> [Type] -> TcS ([Xi], [TcCoercion])
-- Coercions :: Xi ~ Type
-- Returns True iff (no flattening happened)
-- NB: The EvVar inside the flavor is unused, we merely want Given/Solved/Derived/Wanted info
......@@ -546,7 +548,7 @@ flattenMany d f ctxt tys
-- constraints. See Note [Flattening] for more detail.
flatten :: SubGoalDepth -- Depth
-> FlattenMode
-> CtFlavor -> TcType -> TcS (Xi, TcCoercion)
-> CtEvidence -> TcType -> TcS (Xi, TcCoercion)
-- Postcondition: Coercion :: Xi ~ TcType
flatten d f ctxt ty
| Just ty' <- tcView ty
......@@ -595,7 +597,8 @@ flatten d f fl (TyConApp tc tys)
do { flat_cache <- getFlatCache
; case lookupTM fam_ty flat_cache of
Just ct
| cc_flavor ct `canRewrite` fl
| let ctev = cc_ev ct
, ctev `canRewrite` fl
-> -- You may think that we can just return (cc_rhs ct) but not so.
-- return (mkTcCoVarCo (ctId ct), cc_rhs ct, [])
-- The cached constraint resides in the cache so we have to flatten
......@@ -606,42 +609,42 @@ flatten d f fl (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 (cc_flavor ct) rhs_xi
; let final_co = mkTcCoVarCo (ctId ct) `mkTcTransCo` (mkTcSymCo co)
; (flat_rhs_xi,co) <- flatten (cc_depth ct) f ctev rhs_xi
; let final_co = evTermCoercion (ctEvTerm ctev)
`mkTcTransCo` mkTcSymCo co
; return (final_co, flat_rhs_xi,[]) }
_ | isGivenOrSolved fl -- Given or Solved: make new flatten skolem
_ | isGiven fl -- Given: make new flatten skolem
-> do { traceTcS "flatten/flat-cache miss" $ empty
; rhs_xi_var <- newFlattenSkolemTy fam_ty
; mg <- newGivenEvVar (mkTcEqPred fam_ty rhs_xi_var)
(EvCoercion (mkTcReflCo fam_ty))
; case mg of
Fresh eqv ->
do { let new_fl = Given (flav_gloc fl) eqv
ct = CFunEqCan { cc_flavor = new_fl
, cc_fun = tc
, cc_tyargs = xi_args
, cc_rhs = rhs_xi_var
, cc_depth = d }
-- Update the flat cache
; updFlatCache ct
; return (mkTcCoVarCo eqv, rhs_xi_var, [ct]) }
Cached {} -> panic "flatten TyConApp, var must be fresh!" }
; let co = mkTcReflCo fam_ty
new_fl = Given { ctev_gloc = ctev_gloc fl
, ctev_pred = mkTcEqPred fam_ty rhs_xi_var
, ctev_evtm = EvCoercion co }
ct = CFunEqCan { cc_ev = new_fl
, cc_fun = tc
, cc_tyargs = xi_args
, cc_rhs = rhs_xi_var
, cc_depth = d }
-- Update the flat cache
; updFlatCache ct
; return (co, rhs_xi_var, [ct]) }
| otherwise -- Wanted or Derived: make new unification variable
-> do { traceTcS "flatten/flat-cache miss" $ empty
; rhs_xi_var <- newFlexiTcSTy (typeKind fam_ty)
; mw <- newWantedEvVar (mkTcEqPred fam_ty rhs_xi_var)
; let pred = mkTcEqPred fam_ty rhs_xi_var
wloc = ctev_wloc fl
; mw <- newWantedEvVar wloc pred
; case mw of
Fresh eqv ->
do { let new_fl = Wanted (flav_wloc fl) eqv
ct = CFunEqCan { cc_flavor = new_fl
Fresh ctev ->
do { let ct = CFunEqCan { cc_ev = ctev
, cc_fun = tc
, cc_tyargs = xi_args
, cc_rhs = rhs_xi_var
, cc_depth = d }
-- Update the flat cache: just an optimisation!
; updFlatCache ct
; return (mkTcCoVarCo eqv, rhs_xi_var, [ct]) }
; return (evTermCoercion (ctEvTerm ctev), rhs_xi_var, [ct]) }
Cached {} -> panic "flatten TyConApp, var must be fresh!" }
}
-- Emit the flat constraints
......@@ -691,7 +694,7 @@ flatten d _f ctxt ty@(ForAllTy {})
\begin{code}
flattenTyVar :: SubGoalDepth
-> FlattenMode
-> CtFlavor -> TcTyVar -> TcS (Xi, TcCoercion)
-> CtEvidence -> TcTyVar -> TcS (Xi, TcCoercion)
-- "Flattening" a type variable means to apply the substitution to it
flattenTyVar d f ctxt tv
= do { ieqs <- getInertEqs
......@@ -709,13 +712,15 @@ flattenTyVar d f ctxt tv
Just (co,ty) ->
do { (ty_final,co') <- flatten d f ctxt ty
; return (ty_final, co' `mkTcTransCo` mkTcSymCo co) } }
where tv_eq_subst subst tv
| Just ct <- lookupVarEnv subst tv
, cc_flavor ct `canRewrite` ctxt
= Just (mkTcCoVarCo (ctId ct),cc_rhs ct)
-- NB: even if ct is Derived we are not going to
-- touch the actual coercion so we are fine.
| otherwise = Nothing
where
tv_eq_subst subst tv
| Just ct <- lookupVarEnv subst tv
, let ctev = cc_ev ct
, ctev `canRewrite` ctxt
= Just (evTermCoercion (ctEvTerm ctev), cc_rhs ct)
-- NB: even if ct is Derived we are not going to
-- touch the actual coercion so we are fine.
| otherwise = Nothing
\end{code}
Note [Non-idempotent inert substitution]
......@@ -765,13 +770,13 @@ addToWork tcs_action = tcs_action >>= stop_or_emit
\begin{code}
canEqEvVarsCreated :: SubGoalDepth
-> [CtFlavor] -> TcS StopOrContinue
-> [CtEvidence] -> TcS StopOrContinue
canEqEvVarsCreated _d [] = return Stop
canEqEvVarsCreated d (quad:quads)
= mapM_ (addToWork . do_quad) quads >> do_quad quad
-- Add all but one to the work list
-- and return the first (if any) for futher processing
where do_quad fl = let EqPred ty1 ty2 = classifyPredType $ ctFlavPred fl
where do_quad fl = let EqPred ty1 ty2 = classifyPredType $ ctEvPred fl
in canEqNC d fl ty1 ty2
-- Note the "NC": these are fresh equalities so we must be
-- careful to add their kind constraints
......@@ -779,7 +784,7 @@ canEqEvVarsCreated d (quad:quads)
-------------------------
canEqNC, canEq
:: SubGoalDepth
-> CtFlavor
-> CtEvidence
-> Type -> Type -> TcS StopOrContinue
canEqNC d fl ty1 ty2
......@@ -790,7 +795,7 @@ canEq _d fl ty1 ty2
| eqType ty1 ty2 -- Dealing with equality here avoids
-- later spurious occurs checks for a~a
= if isWanted fl then
setEvBind (flav_evar fl) (EvCoercion (mkTcReflCo ty1)) >> return Stop
setEvBind (ctev_evar fl) (EvCoercion (mkTcReflCo ty1)) >> return Stop
else
return Stop
......@@ -823,11 +828,11 @@ canEq d fl ty1 ty2
-- Fail straight away for better error messages
then canEqFailure d fl
else
let xcomp xs = EvCoercion (mkTcTyConAppCo tc1 (map mkTcCoVarCo xs))
xdecomp x = zipWith (\_ i -> EvCoercion $ mkTcNthCo i (mkTcCoVarCo x)) tys1 [0..]
xev = XEvTerm xcomp xdecomp
in xCtFlavor fl (zipWith mkTcEqPred tys1 tys2) xev (canEqEvVarsCreated d)
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
; canEqEvVarsCreated d ctevs }
-- See Note [Equality between type applications]
-- Note [Care with type applications] in TcUnify
......@@ -839,7 +844,7 @@ canEq d fl ty1 ty2 -- e.g. F a b ~ Maybe c
canEq d fl s1@(ForAllTy {}) s2@(ForAllTy {})
| tcIsForAllTy s1, tcIsForAllTy s2
, Wanted loc orig_ev <- fl
, Wanted { ctev_wloc = loc, ctev_evar = orig_ev } <- fl
= do { let (tvs1,body1) = tcSplitForAllTys s1
(tvs2,body2) = tcSplitForAllTys s2
; if not (equalLength tvs1 tvs2) then
......@@ -857,12 +862,12 @@ canEq d fl _ _ = canEqFailure d fl
------------------------
-- Type application
canEqAppTy :: SubGoalDepth
-> CtFlavor
-> CtEvidence
-> Type -> Type -> Type -> Type
-> TcS StopOrContinue
canEqAppTy d fl s1 t1 s2 t2
= ASSERT( not (isKind t1) && not (isKind t2) )
if isGivenOrSolved fl then
if isGiven fl then
do { traceTcS "canEq (app case)" $
text "Ommitting decomposition of given equality between: "
<+> ppr (AppTy s1 t1) <+> text "and" <+> ppr (AppTy s2 t2)
......@@ -870,14 +875,14 @@ canEqAppTy d fl s1 t1 s2 t2
-- because we no longer have 'left' and 'right'
; return Stop }
else
let xevcomp [x,y] = EvCoercion (mkTcAppCo (mkTcCoVarCo x) (mkTcCoVarCo y))
xevcomp _ = error "canEqAppTy: can't happen" -- Can't happen
xev = XEvTerm { ev_comp = xevcomp
, ev_decomp = error "canEqAppTy: can't happen" }
in xCtFlavor fl [mkTcEqPred s1 s2, mkTcEqPred t1 t2] xev $
canEqEvVarsCreated d
canEqFailure :: SubGoalDepth -> CtFlavor -> TcS StopOrContinue
do { let xevcomp [x,y] = EvCoercion (mkTcAppCo (evTermCoercion x) (evTermCoercion y))
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
; canEqEvVarsCreated d ctevs }
canEqFailure :: SubGoalDepth -> CtEvidence -> TcS StopOrContinue
canEqFailure d fl = emitFrozenError fl d >> return Stop
------------------------
......@@ -885,12 +890,12 @@ emitKindConstraint :: Ct -> TcS StopOrContinue
emitKindConstraint ct
= case ct of
CTyEqCan { cc_depth = d
, cc_flavor = fl, cc_tyvar = tv
, cc_ev = fl, cc_tyvar = tv
, cc_rhs = ty }
-> emit_kind_constraint d fl (mkTyVarTy tv) ty
CFunEqCan { cc_depth = d
, cc_flavor = fl
, cc_ev = fl
, cc_fun = fn, cc_tyargs = xis1
, cc_rhs = xi2 }
-> emit_kind_constraint d fl (mkTyConApp fn xis1) xi2
......@@ -904,41 +909,43 @@ emitKindConstraint ct
| otherwise
= ASSERT( isKind k1 && isKind k2 )
do { kev <-
do { mw <- newWantedEvVar (mkEqPred k1 k2)
do { mw <- newWantedEvVar kind_co_wloc (mkEqPred k1 k2)
; case mw of
Cached x -> return x
Fresh x -> addToWork (canEq d (kind_co_fl x) k1 k2) >> return x }
; let xcomp [x] = mkEvKindCast x (mkTcCoVarCo kev)
Cached ev_tm -> return ev_tm
Fresh ctev -> do { addToWork (canEq d ctev k1 k2)
; return (ctEvTerm ctev) } }
; let xcomp [x] = mkEvKindCast x (evTermCoercion kev)
xcomp _ = panic "emit_kind_constraint:can't happen"
xdecomp x = [mkEvKindCast x (mkTcCoVarCo kev)]
xdecomp x = [mkEvKindCast x (evTermCoercion kev)]
xev = XEvTerm xcomp xdecomp
in xCtFlavor_cache False fl [mkTcEqPred ty1 ty2] xev what_next }
; ctevs <- xCtFlavor_cache False fl [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)
-- (T :: *)
-- Equality is: (alpha ~ T), so we will emitConstraint (kappa0 ~ *) but
-- we don't want to say that (alpha ~ T) is now Solved!
where
what_next [new_fl] = continueWith (ct { cc_flavor = new_fl })
what_next _ = return Stop
; case ctevs of
[] -> return Stop
[new_ctev] -> continueWith (ct { cc_ev = new_ctev })
_ -> panic "emitKindConstraint" }
where
k1 = typeKind ty1
k2 = typeKind ty2
ctxt = mkKindErrorCtxtTcS ty1 k1 ty2 k2