Commit 2d8374a8 authored by dimitris's avatar dimitris

Updates to the constraint solver to be able to handle implication

constraint generation during solveInteractCts, needed for polytype
equality decomposition. More commentary to follow.
parent 1bfb9798
......@@ -8,13 +8,13 @@
module TcCanonical(
canonicalize, flatten, flattenMany,
FlattenMode (..),
StopOrContinue (..)
) where
#include "HsVersions.h"
import BasicTypes ( IPName )
import TcErrors
import TcRnTypes
import TcType
import Type
......@@ -26,7 +26,6 @@ import TypeRep
import Name ( Name )
import Var
import VarEnv
-- import Util( equalLength )
import Outputable
import Control.Monad ( when, unless )
import MonadUtils
......@@ -37,6 +36,9 @@ import VarSet
import TcSMonad
import FastString
import Util ( equalLength )
import TysWiredIn ( eqTyCon )
import Data.Maybe ( isJust, fromMaybe )
......@@ -258,7 +260,7 @@ canIP d fl nm ty
= -- Note [Canonical implicit parameter constraints] explains why it's
-- possible in principle to not flatten, but since flattening applies
-- the inert substitution we choose to flatten anyway.
do { (xi,co) <- flatten d fl (mkIPPred nm ty)
do { (xi,co) <- flatten d FMFullFlatten fl (mkIPPred nm ty)
; mb <- rewriteCtFlavor fl xi co
; case mb of
Just new_fl -> let IPPred _ xi_in = classifyPredType xi
......@@ -304,7 +306,7 @@ canClassNC d fl cls tys
canClass d fl cls tys
= do { -- sctx <- getTcSContext
; (xis, cos) <- flattenMany d fl tys
; (xis, cos) <- flattenMany d FMFullFlatten fl tys
; let co = mkTcTyConAppCo (classTyCon cls) cos
xi = mkClassPred cls xis
......@@ -458,7 +460,7 @@ canIrred :: SubGoalDepth -- Depth
-- Precondition: ty not a tuple and no other evidence form
canIrred d fl ty
= do { traceTcS "can_pred" (text "IrredPred = " <+> ppr ty)
; (xi,co) <- flatten d fl ty -- co :: xi ~ ty
; (xi,co) <- flatten d FMFullFlatten fl 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
......@@ -485,7 +487,8 @@ Note [Flattening]
~~~~~~~~~~~~~~~~~~~~
flatten ty ==> (xi, cc)
where
xi has no type functions
xi has no type functions, unless they appear under ForAlls
cc = Auxiliary given (equality) constraints constraining
the fresh type variables in xi. Evidence for these
is always the identity coercion, because internally the
......@@ -522,17 +525,21 @@ unexpanded synonym.
\begin{code}
data FlattenMode = FMSubstOnly
| FMFullFlatten
-- Flatten a bunch of types all at once.
flattenMany :: SubGoalDepth -- Depth
-> FlattenMode
-> CtFlavor -> [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
flattenMany d ctxt tys
flattenMany d f ctxt tys
= -- pprTrace "flattenMany" empty $
go tys
where go [] = return ([],[])
go (ty:tys) = do { (xi,co) <- flatten d ctxt ty
go (ty:tys) = do { (xi,co) <- flatten d f ctxt ty
; (xis,cos) <- go tys
; return (xi:xis,co:cos) }
......@@ -540,33 +547,34 @@ flattenMany d ctxt tys
-- the new type-function-free type, and a collection of new equality
-- constraints. See Note [Flattening] for more detail.
flatten :: SubGoalDepth -- Depth
-> FlattenMode
-> CtFlavor -> TcType -> TcS (Xi, TcCoercion)
-- Postcondition: Coercion :: Xi ~ TcType
flatten d ctxt ty
flatten d f ctxt ty
| Just ty' <- tcView ty
= do { (xi, co) <- flatten d ctxt ty'
= do { (xi, co) <- flatten d f ctxt ty'
; return (xi,co) }
flatten _ _ xi@(LitTy {}) = return (xi, mkTcReflCo xi)
flatten _ _ _ xi@(LitTy {}) = return (xi, mkTcReflCo xi)
flatten d ctxt (TyVarTy tv)
= flattenTyVar d ctxt tv
flatten d f ctxt (TyVarTy tv)
= flattenTyVar d f ctxt tv
flatten d ctxt (AppTy ty1 ty2)
= do { (xi1,co1) <- flatten d ctxt ty1
; (xi2,co2) <- flatten d ctxt ty2
flatten d f ctxt (AppTy ty1 ty2)
= do { (xi1,co1) <- flatten d f ctxt ty1
; (xi2,co2) <- flatten d f ctxt ty2
; return (mkAppTy xi1 xi2, mkTcAppCo co1 co2) }
flatten d ctxt (FunTy ty1 ty2)
= do { (xi1,co1) <- flatten d ctxt ty1
; (xi2,co2) <- flatten d ctxt ty2
flatten d f ctxt (FunTy ty1 ty2)
= do { (xi1,co1) <- flatten d f ctxt ty1
; (xi2,co2) <- flatten d f ctxt ty2
; return (mkFunTy xi1 xi2, mkTcFunCo co1 co2) }
flatten d fl (TyConApp tc tys)
flatten d f fl (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 fl tys
= do { (xis,cos) <- flattenMany d f fl tys
; return (mkTyConApp tc xis, mkTcTyConAppCo tc cos) }
-- Otherwise, it's a type function application, and we have to
......@@ -574,7 +582,7 @@ flatten d fl (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 fl tys
do { (xis, cos) <- flattenMany d f fl tys
; let (xi_args, xi_rest) = splitAt (tyConArity tc) xis
-- The type function might be *over* saturated
-- in which case the remaining arguments should
......@@ -582,30 +590,34 @@ flatten d fl (TyConApp tc tys)
fam_ty = mkTyConApp tc xi_args
; (ret_co, rhs_xi, ct) <-
do { flat_cache <- getFlatCache
; case lookupTM fam_ty flat_cache of
Just ct
| cc_flavor ct `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
-- the rhs to make sure we have applied any inert substitution to it.
-- Alternatively we could be applying the inert substitution to the
-- cache as well when we interact an equality with the inert.
-- The design choice is: do we keep the flat cache rewritten or not?
-- 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) (cc_flavor ct) rhs_xi
; let final_co = mkTcCoVarCo (ctId ct) `mkTcTransCo` (mkTcSymCo co)
; return (final_co, flat_rhs_xi,[]) }
case f of
FMSubstOnly ->
return (mkTcReflCo fam_ty, fam_ty, [])
FMFullFlatten ->
do { flat_cache <- getFlatCache
; case lookupTM fam_ty flat_cache of
Just ct
| cc_flavor ct `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
-- the rhs to make sure we have applied any inert substitution to it.
-- Alternatively we could be applying the inert substitution to the
-- cache as well when we interact an equality with the inert.
-- The design choice is: do we keep the flat cache rewritten or not?
-- 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)
; return (final_co, flat_rhs_xi,[]) }
_ | isGivenOrSolved fl -- Given or Solved: 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
_ | isGivenOrSolved fl -- Given or Solved: 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
......@@ -617,11 +629,11 @@ flatten d fl (TyConApp tc tys)
; updFlatCache ct
; return (mkTcCoVarCo eqv, rhs_xi_var, [ct]) }
Cached {} -> panic "flatten TyConApp, var must be fresh!" }
| 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)
; case mw of
| 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)
; case mw of
Fresh eqv ->
do { let new_fl = Wanted (flav_wloc fl) eqv
ct = CFunEqCan { cc_flavor = new_fl
......@@ -633,7 +645,7 @@ flatten d fl (TyConApp tc tys)
; updFlatCache ct
; return (mkTcCoVarCo eqv, rhs_xi_var, [ct]) }
Cached {} -> panic "flatten TyConApp, var must be fresh!" }
}
}
-- Emit the flat constraints
; updWorkListTcS $ appendWorkListEqs ct
; let (cos_args, cos_rest) = splitAt (tyConArity tc) cos
......@@ -644,12 +656,16 @@ flatten d fl (TyConApp tc tys)
)
}
flatten d ctxt ty@(ForAllTy {})
flatten d _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
; return (mkForAllTys tvs rho', foldr mkTcForAllCo co tvs) }
{- DELETEME
; when (under_families tvs rho) $ wrapErrTcS $ flattenForAllErrorTcS ctxt ty
; (rho', co) <- flatten d ctxt rho
; (rho', co) <- flatten d FMSubstOnly ctxt rho
-- Only do substitutions, not flattening under ForAlls
; return (mkForAllTys tvs rho', foldr mkTcForAllCo co tvs) }
-- DV: Simon and I have a better plan here related to #T5934 and that plan is to
......@@ -670,18 +686,22 @@ flatten d ctxt ty@(ForAllTy {})
go bound (FunTy arg res) = go bound arg || go bound res
go bound (AppTy fun arg) = go bound fun || go bound arg
go bound (ForAllTy tv ty) = go (bound `extendVarSet` tv) ty
-}
\end{code}
\begin{code}
flattenTyVar :: SubGoalDepth -> CtFlavor -> TcTyVar -> TcS (Xi, TcCoercion)
flattenTyVar :: SubGoalDepth
-> FlattenMode
-> CtFlavor -> TcTyVar -> TcS (Xi, TcCoercion)
-- "Flattening" a type variable means to apply the substitution to it
flattenTyVar d ctxt tv
flattenTyVar d f ctxt tv
= do { ieqs <- getInertEqs
; let mco = tv_eq_subst (fst 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 ctxt knd
; (new_knd,_kind_co) <- flatten d f ctxt knd
; let ty = mkTyVarTy (setVarType tv new_knd)
; return (ty, mkTcReflCo ty) }
-- NB recursive call.
......@@ -689,7 +709,7 @@ flattenTyVar d ctxt tv
-- 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 ctxt 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
......@@ -820,13 +840,20 @@ canEq d fl ty1 ty2 -- e.g. F a b ~ Maybe c
= canEqAppTy d fl s1 t1 s2 t2
canEq d fl s1@(ForAllTy {}) s2@(ForAllTy {})
| tcIsForAllTy s1, tcIsForAllTy s2,
Wanted {} <- fl
= canEqFailure d fl
| tcIsForAllTy s1, tcIsForAllTy s2
, Wanted loc orig_ev <- fl
= do { let (tvs1,body1) = tcSplitForAllTys s1
(tvs2,body2) = tcSplitForAllTys s2
; if not (equalLength tvs1 tvs2) then
canEqFailure d fl
else
do { traceTcS "Creating implication for polytype equality" $ ppr fl
; deferTcSForAllEq (loc,orig_ev) (tvs1,body1) (tvs2,body2)
; return Stop } }
| otherwise
= do { traceTcS "Ommitting decomposition of given polytype equality" (pprEq s1 s2)
= do { traceTcS "Ommitting decomposition of given polytype equality" $
pprEq s1 s2
; return Stop }
canEq d fl _ _ = canEqFailure d fl
------------------------
......@@ -1168,8 +1195,8 @@ canEqLeafFunEqLeftRec d fl (fn,tys1) ty2 -- fl :: F tys1 ~ ty2
= do { traceTcS "canEqLeafFunEqLeftRec" $ pprEq (mkTyConApp fn tys1) ty2
; (xis1,cos1) <-
{-# SCC "flattenMany" #-}
flattenMany d fl tys1 -- Flatten type function arguments
-- cos1 :: xis1 ~ tys1
flattenMany d FMFullFlatten fl tys1 -- Flatten type function arguments
-- cos1 :: xis1 ~ tys1
; let fam_head = mkTyConApp fn xis1
-- Fancy higher-dimensional coercion between equalities!
......@@ -1194,7 +1221,7 @@ canEqLeafFunEqLeft d fl (fn,xis1) s2
do { traceTcS "canEqLeafFunEqLeft" $ pprEq (mkTyConApp fn xis1) s2
; (xi2,co2) <-
{-# SCC "flatten" #-}
flatten d fl s2 -- co2 :: xi2 ~ s2
flatten d FMFullFlatten fl s2 -- co2 :: xi2 ~ s2
; let fam_head = mkTyConApp fn xis1
-- Fancy coercion between equalities! But it should just work!
......@@ -1216,7 +1243,7 @@ canEqLeafTyVarLeftRec :: SubGoalDepth
-> TcTyVar -> TcType -> TcS StopOrContinue
canEqLeafTyVarLeftRec d fl tv s2 -- fl :: tv ~ s2
= do { traceTcS "canEqLeafTyVarLeftRec" $ pprEq (mkTyVarTy tv) s2
; (xi1,co1) <- flattenTyVar d fl tv -- co1 :: xi1 ~ tv
; (xi1,co1) <- flattenTyVar d FMFullFlatten fl tv -- co1 :: xi1 ~ tv
; let is_still_var = isJust (getTyVar_maybe xi1)
; traceTcS "canEqLeafTyVarLeftRec2" $ empty
......@@ -1243,8 +1270,8 @@ canEqLeafTyVarLeft :: SubGoalDepth -- Depth
canEqLeafTyVarLeft d fl tv s2 -- eqv : tv ~ s2
= do { let tv_ty = mkTyVarTy tv
; traceTcS "canEqLeafTyVarLeft" (pprEq tv_ty s2)
; (xi2, co2) <- flatten d fl s2 -- Flatten RHS co : xi2 ~ s2
; (xi2, co2) <- flatten d FMFullFlatten fl s2 -- Flatten RHS co:xi2 ~ s2
; traceTcS "canEqLeafTyVarLeft" (nest 2 (vcat [ text "tv =" <+> ppr tv
, text "s2 =" <+> ppr s2
, text "xi2 =" <+> ppr xi2]))
......
......@@ -91,12 +91,21 @@ If in Step 1 no such element exists, we have exceeded our context-stack
depth and will simply fail.
\begin{code}
solveInteractCts :: [Ct] -> TcS ()
solveInteractCts :: [Ct] -> TcS (Bag Implication)
-- Returns a bag of residual implications that have arisen while solving
-- this particular worklist.
solveInteractCts cts
= do { traceTcS "solveInteractCtS" (vcat [ text "cts =" <+> ppr cts ])
; updWorkListTcS (appendWorkListCt cts) >> solveInteract }
solveInteractGiven :: GivenLoc -> [EvVar] -> TcS ()
; updWorkListTcS (appendWorkListCt cts) >> solveInteract
; impls <- getTcSImplics
; updTcSImplics (const emptyBag) -- Nullify residual implications
; return impls }
solveInteractGiven :: GivenLoc -> [EvVar] -> TcS (Bag Implication)
-- 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 evs
= solveInteractCts (map mk_noncan evs)
where mk_noncan ev = CNonCanonical { cc_flavor = Given gloc ev
......@@ -1614,9 +1623,9 @@ lkpFunEqCache fam_head
, cc_fun = tc, cc_tyargs = xis
, cc_rhs = xi}))
= ASSERT (isSolved fl)
do { (xis_subst,cos) <- flattenMany d fl xis
do { (xis_subst,cos) <- flattenMany d FMFullFlatten fl xis
-- cos :: xis_subst ~ xis
; (xi_subst,co) <- flatten d fl xi
; (xi_subst,co) <- flatten d FMFullFlatten fl xi
-- co :: xi_subst ~ xi
; let flat_fam_head = mkTyConApp tc xis_subst
......
......@@ -831,10 +831,15 @@ instance Outputable WhereFrom where
\begin{code}
-- Types without any type functions inside. However, note that xi
-- types CAN contain unexpanded type synonyms; however, the
-- (transitive) expansions of those type synonyms will not contain any
-- type functions.
-- The syntax of xi types:
-- xi ::= a | T xis | xis -> xis | ... | forall a. tau
-- Two important notes:
-- (i) No type families, unless we are under a ForAll
-- (ii) Note that xi types can contain unexpanded type synonyms;
-- however, the (transitive) expansions of those type synonyms
-- will not contain any type functions, unless we are under a ForAll.
-- We enforce the structure of Xi types when we flatten (TcCanonical)
type Xi = Type -- In many comments, "xi" ranges over Xi
type Cts = Bag Ct
......
......@@ -18,6 +18,8 @@ module TcSMonad (
getTcSWorkList, updWorkListTcS, updWorkListTcS_return, keepWanted,
getTcSWorkListTvs,
getTcSImplics, updTcSImplics, emitTcSImplication,
Ct(..), Xi, tyVarsOfCt, tyVarsOfCts, tyVarsOfCDicts,
emitFrozenError,
......@@ -42,6 +44,7 @@ module TcSMonad (
-- Getting and setting the flattening cache
getFlatCache, updFlatCache, addToSolved,
deferTcSForAllEq,
setEvBind,
XEvTerm(..),
......@@ -136,6 +139,7 @@ import Unique
import UniqFM
import Maybes ( orElse )
import Control.Monad( when )
import StaticFlags( opt_PprStyle_Debug )
import Data.IORef
......@@ -783,8 +787,11 @@ data TcSEnv
tcs_count :: IORef Int, -- Global step count
tcs_inerts :: IORef InertSet, -- Current inert set
tcs_worklist :: IORef WorkList -- Current worklist
tcs_worklist :: IORef WorkList, -- Current worklist
-- Residual implication constraints that are generated
-- while solving the current worklist.
tcs_implics :: IORef (Bag Implication)
}
type TcsUntouchables = (Untouchables,TcTyVarSet)
......@@ -884,6 +891,7 @@ runTcS :: SimplContext
runTcS context untouch is wl tcs
= do { ty_binds_var <- TcM.newTcRef emptyVarEnv
; ev_binds_var <- TcM.newTcEvBinds
; impl_var <- TcM.newTcRef emptyBag
; step_count <- TcM.newTcRef 0
; inert_var <- TcM.newTcRef is
......@@ -896,7 +904,8 @@ runTcS context untouch is wl tcs
, tcs_count = step_count
, tcs_ic_depth = 0
, tcs_inerts = inert_var
, tcs_worklist = wl_var }
, tcs_worklist = wl_var
, tcs_implics = impl_var }
-- Run the computation
; res <- unTcS tcs env
......@@ -930,7 +939,8 @@ nestImplicTcS ref (inner_range, inner_tcs) (TcS thing_inside)
, tcs_ic_depth = idepth
, tcs_context = ctxt
, tcs_inerts = inert_var
, tcs_worklist = wl_var } ->
, tcs_worklist = wl_var
, tcs_implics = _impl_var } ->
do { let inner_untch = (inner_range, outer_tcs `unionVarSet` inner_tcs)
-- The inner_range should be narrower than the outer one
-- (thus increasing the set of untouchables) but
......@@ -940,6 +950,10 @@ nestImplicTcS ref (inner_range, inner_tcs) (TcS thing_inside)
-- Inherit the inerts from the outer scope
; orig_inerts <- TcM.readTcRef inert_var
; new_inert_var <- TcM.newTcRef orig_inerts
-- Inherit residual implications from outer scope (?) or create
-- fresh var?
-- ; orig_implics <- TcM.readTcRef impl_var
; new_implics_var <- TcM.newTcRef emptyBag
; let nest_env = TcSEnv { tcs_ev_binds = ref
, tcs_ty_binds = ty_binds
......@@ -951,6 +965,7 @@ nestImplicTcS ref (inner_range, inner_tcs) (TcS thing_inside)
, tcs_worklist = wl_var
-- NB: worklist is going to be empty anyway,
-- so reuse the same ref cell
, tcs_implics = new_implics_var
}
; thing_inside nest_env }
......@@ -996,6 +1011,13 @@ getTcSWorkListRef = TcS (return . tcs_worklist)
getTcSInerts :: TcS InertSet
getTcSInerts = getTcSInertsRef >>= wrapTcS . (TcM.readTcRef)
getTcSImplicsRef :: TcS (IORef (Bag Implication))
getTcSImplicsRef = TcS (return . tcs_implics)
getTcSImplics :: TcS (Bag Implication)
getTcSImplics = getTcSImplicsRef >>= wrapTcS . (TcM.readTcRef)
getTcSWorkList :: TcS WorkList
getTcSWorkList = getTcSWorkListRef >>= wrapTcS . (TcM.readTcRef)
......@@ -1020,6 +1042,18 @@ updWorkListTcS_return f
; let (res,new_work) = f wl_curr
; wrapTcS (TcM.writeTcRef wl_var new_work)
; return res }
updTcSImplics :: (Bag Implication -> Bag Implication) -> TcS ()
updTcSImplics f
= do { impl_ref <- getTcSImplicsRef
; implics <- wrapTcS (TcM.readTcRef impl_ref)
; let new_implics = f implics
; wrapTcS (TcM.writeTcRef impl_ref new_implics) }
emitTcSImplication :: Implication -> TcS ()
emitTcSImplication imp = updTcSImplics (consBag imp)
emitFrozenError :: CtFlavor -> SubGoalDepth -> TcS ()
-- Emits a non-canonical constraint that will stand for a frozen error in the inerts.
......@@ -1486,6 +1520,54 @@ matchFam :: TyCon -> [Type] -> TcS (Maybe (FamInst, [Type]))
matchFam tycon args = wrapTcS $ tcLookupFamInst tycon args
\end{code}
\begin{code}
-- Deferring forall equalities as implications
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
deferTcSForAllEq :: (WantedLoc,EvVar) -- Original wanted equality flavor
-> ([TyVar],TcType) -- ForAll tvs1 body1
-> ([TyVar],TcType) -- ForAll tvs2 body2
-> TcS ()
-- Some of this functionality is repeated from TcUnify,
-- consider having a single place where we create fresh implications.
deferTcSForAllEq (loc,orig_ev) (tvs1,body1) (tvs2,body2)
= do { (subst1, skol_tvs) <- wrapTcS $ TcM.tcInstSkolTyVars tvs1
; let tys = mkTyVarTys skol_tvs
phi1 = Type.substTy subst1 body1
phi2 = Type.substTy (zipTopTvSubst tvs2 tys) body2
skol_info = UnifyForAllSkol skol_tvs phi1
; mev <- newWantedEvVar (mkTcEqPred phi1 phi2)
; let new_fl = Wanted loc (mn_thing mev)
new_ct = mkNonCanonical new_fl
new_co = mkTcCoVarCo (mn_thing mev)
; coe_inside <- if isFresh mev then
do { ev_binds_var <- wrapTcS $ TcM.newTcEvBinds
; let ev_binds = TcEvBinds ev_binds_var
; lcl_env <- wrapTcS $ TcM.getLclTypeEnv
; loc <- wrapTcS $ TcM.getCtLoc skol_info
; untch <- getUntouchables
; let wc = WC { wc_flat = singleCt new_ct
, wc_impl = emptyBag
, wc_insol = emptyCts }
imp = Implic { ic_untch = fst untch
-- What about TcS touchables?
, ic_env = lcl_env
, ic_skols = skol_tvs
, ic_given = []
, ic_wanted = wc
, ic_insol = False
, ic_binds = ev_binds_var
, ic_loc = loc }
; updTcSImplics (consBag imp)
; return (TcLetCo ev_binds new_co) }
else (return new_co)
; setEvBind orig_ev $
EvCoercion (foldr mkTcForAllCo coe_inside skol_tvs)
}
\end{code}
-- Rewriting with respect to the inert equalities
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......
......@@ -384,8 +384,9 @@ simplifyWithApprox wanted
= do { traceTcS "simplifyApproxLoop" (ppr wanted)
; let all_flats = wc_flat wanted `unionBags` keepWanted (wc_insol wanted)
; solveInteractCts $ bagToList all_flats
; unsolved_implics <- simpl_loop 1 (wc_impl wanted)
; implics_from_flats <- solveInteractCts $ bagToList all_flats
; unsolved_implics <- simpl_loop 1 (wc_impl wanted `unionBags`
implics_from_flats)
; let (residual_implics,floats) = approximateImplications unsolved_implics
......@@ -777,11 +778,11 @@ solve_wanteds wanted@(WC { wc_flat = flats, wc_impl = implics, wc_insol = insols
-- wrong anyway!
; let all_flats = flats `unionBags` keepWanted insols
; solveInteractCts $ bagToList all_flats
; impls_from_flats <- solveInteractCts $ bagToList all_flats
-- solve_wanteds iterates when it is able to float equalities
-- out of one or more of the implications.
; unsolved_implics <- simpl_loop 1 implics
; unsolved_implics <- simpl_loop 1 (implics `unionBags` impls_from_flats)
; (insoluble_flats,unsolved_flats) <- extractUnsolvedTcS
......@@ -832,8 +833,9 @@ simpl_loop n implics
, text "unsolved_implics =" <+> ppr unsolved_implics ]
; if isEmptyBag improve_eqs then return unsolved_implics
else do { solveInteractCts $ bagToList improve_eqs
; simpl_loop (n+1) unsolved_implics } }
else do { impls_from_eqs <- solveInteractCts $ bagToList improve_eqs
; simpl_loop (n+1) (unsolved_implics `unionBags`
impls_from_eqs)} }
solveNestedImplications :: Bag Implication
-> TcS (Cts, Bag Implication)
......@@ -855,7 +857,9 @@ solveNestedImplications implics
-- Push the unsolved wanteds inwards, but as givens
; traceTcS "solveWanteds: preparing inerts for implications {" $
vcat [ppr tcs_untouchables, ppr pushed_givens]
; solveInteractCts pushed_givens
; impls_from_givens <- solveInteractCts pushed_givens
; MASSERT (isEmptyBag impls_from_givens)
; traceTcS "solveWanteds: } now doing nested implications {" empty
; flatMapBagPairM (solveImplication tcs_untouchables) implics }
......@@ -904,8 +908,9 @@ solveImplication tcs_untouchables
do { traceTcS "solveImplication {" (ppr imp)
-- Solve flat givens
; solveInteractGiven loc givens
; impls_from_givens <- solveInteractGiven loc givens
; MASSERT (isEmptyBag impls_from_givens)
-- Simplify the wanteds
; WC { wc_flat = unsolved_flats
, wc_impl = unsolved_implics
......@@ -1395,8 +1400,13 @@ disambigGroup (default_ty:default_tys) group
in return [ CNonCanonical { cc_flavor = dfl, cc_depth = 0 } ] }
; traceTcS "disambigGroup (solving) {"
(text "trying to solve constraints along with default equations ...")
; solveInteractCts (derived_eq ++ wanteds)
(text "trying to solve constraints along with default equations ...")
; implics_from_defaulting <-
solveInteractCts (derived_eq ++ wanteds)
; MASSERT (isEmptyBag implics_from_defaulting)
-- Ignore implics: I don't think that a defaulting equation can cause
-- new implications to be emitted. Maybe we have to revisit this.
; (_,unsolved) <- extractUnsolvedTcS
; traceTcS "disambigGroup (solving) }"
(text "disambigGroup unsolved =" <+> ppr (keepWanted unsolved))
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment