Commit fe6ddf00 authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

A bunch more simplification and refactoring to the constraint solver

* Instead of Untouchables being a [Unique], it is simply an Int
  indicating the depth of nesting.  This works fine now that
  floatEqualities is promoting the floated unification variables
  to the outer level

* Remove the inert_tv_eqs (InScopeSet) from InertCans.  It wasn't
  being used.  See Note [Shadowing in a constraint] in TcRnTypes

* Rename inert_frozen to inert_insols

* Some simple refactoring in
     TcErrors.reportFlatsAndInsols
     TcInteract.kickOutRewritable
     TsSimplify.floatEqualities
parent b737a453
......@@ -641,7 +641,7 @@ flattenTyVar d f ctxt tv
where
flatten_from_inerts
= do { ieqs <- getInertEqs
; let mco = tv_eq_subst (fst ieqs) tv -- co : v ~ ty
; 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
......@@ -818,7 +818,7 @@ canEqAppTy d fl s1 t1 s2 t2
; canEvVarsCreated d ctevs }
canEqFailure :: SubGoalDepth -> CtEvidence -> TcS StopOrContinue
canEqFailure d fl = emitFrozenError fl d >> return Stop
canEqFailure d fl = do { emitFrozenError fl d; return Stop }
------------------------
emitKindConstraint :: Ct -> TcS StopOrContinue
......
......@@ -139,27 +139,25 @@ 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 })
= reportTidyWanteds ctxt tidy_insols tidy_flats implics
= reportTidyWanteds ctxt tidy_all implics
where
env = cec_tidy ctxt
tidy_insols = mapBag (tidyCt env) insols
tidy_flats = mapBag (tidyCt env) flats
tidy_all = mapBag (tidyCt env) (insols `unionBags` flats)
-- All the Derived ones have been filtered out alrady
-- by the constraint solver. This is ok; we don't want
-- to report unsolved Derived goals as error
-- See Note [Do not report derived but soluble errors]
reportTidyWanteds :: ReportErrCtxt -> Bag Ct -> Bag Ct -> Bag Implication -> TcM ()
reportTidyWanteds ctxt insols flats implics
reportTidyWanteds :: ReportErrCtxt -> Cts -> Bag Implication -> TcM ()
reportTidyWanteds ctxt flats implics
| Just ev_binds_var <- cec_defer ctxt
= do { -- Defer errors to runtime
-- See Note [Deferring coercion errors to runtime] in TcSimplify
mapBagM_ (deferToRuntime ev_binds_var ctxt mkFlatErr)
(flats `unionBags` insols)
mapBagM_ (deferToRuntime ev_binds_var ctxt mkFlatErr) flats
; mapBagM_ (reportImplic ctxt) implics }
| otherwise
= do { reportInsolsAndFlats ctxt insols flats
= do { reportFlats ctxt flats
; mapBagM_ (reportImplic ctxt) implics }
......@@ -183,8 +181,8 @@ deferToRuntime ev_binds_var ctxt mk_err_msg ct
| otherwise -- Do not set any evidence for Given/Derived
= return ()
reportInsolsAndFlats :: ReportErrCtxt -> Cts -> Cts -> TcM ()
reportInsolsAndFlats ctxt insols flats
reportFlats :: ReportErrCtxt -> Cts -> TcM ()
reportFlats ctxt flats -- Here 'flats' includes insolble goals
= tryReporters
[ -- First deal with things that are utterly wrong
-- Like Int ~ Bool (incl nullary TyCons)
......@@ -198,7 +196,7 @@ reportInsolsAndFlats ctxt insols flats
, ("Unambiguous", unambiguous, reportFlatErrs ctxt) ]
(reportAmbigErrs ctxt)
(bagToList (insols `unionBags` flats))
(bagToList flats)
where
utterly_wrong, skolem_eq, unambiguous :: Ct -> PredTree -> Bool
......
......@@ -283,32 +283,25 @@ Case 2: Functional Dependencies
\begin{code}
spontaneousSolveStage :: SimplifierStage
spontaneousSolveStage workItem
= do { mSolve <- trySpontaneousSolve workItem
; spont_solve mSolve }
where spont_solve SPCantSolve
| CTyEqCan { cc_tyvar = tv, cc_ev = fl } <- workItem
-- Unsolved equality
= do { wl <- modifyInertTcS (kickOutRewritable (ctEvFlavour fl) tv)
; traceTcS "kickOutRewritableInerts" $
vcat [ text "WorkItem (unsolved) =" <+> ppr workItem
, text "Kicked out =" <+> ppr wl ]
; updWorkListTcS (appendWorkList wl)
; insertInertItemTcS workItem
; return Stop }
| otherwise
= continueWith workItem
spont_solve (SPSolved new_tv)
-- 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) $
ptext (sLit "Spontaneously solved:") <+> ppr workItem
; wl <- modifyInertTcS (kickOutRewritable Given new_tv)
; traceTcS "kickOutRewritableInerts" $ ptext (sLit "Kicked out =") <+> ppr wl
; updWorkListTcS (appendWorkList wl)
; return Stop }
= do { mb_solved <- trySpontaneousSolve workItem
; case mb_solved of
SPCantSolve
| CTyEqCan { cc_tyvar = tv, cc_ev = fl } <- workItem
-- Unsolved equality
-> do { kickOutRewritable (ctEvFlavour fl) tv
; insertInertItemTcS workItem
; return Stop }
| otherwise
-> continueWith workItem
SPSolved new_tv
-- 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) $
ptext (sLit "Spontaneously solved:") <+> ppr workItem
; kickOutRewritable Given new_tv
; return Stop } }
\end{code}
Note [Spontaneously solved in TyBinds]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......@@ -326,45 +319,44 @@ and only record them in the TyBinds of the TcS monad. The flattener is now consu
these binds /and/ the inerts for potentially unsolved or other given equalities.
\begin{code}
kickOutRewritable :: CtFlavour -- Flavour of the equality that is
-- being added to the inert set
-> TcTyVar -- The new equality is tv ~ ty
-> InertSet -> (WorkList,InertSet)
-> TcS ()
kickOutRewritable new_flav new_tv
is@(IS { inert_cans = IC { inert_eqs = tv_eqs
, inert_eq_tvs = inscope
, inert_dicts = dictmap
, inert_funeqs = funeqmap
, inert_irreds = irreds }
, inert_frozen = frozen })
= (kicked_out, remaining)
= do { wl <- modifyInertTcS kick_out
; traceTcS "kickOutRewritable" $
vcat [ text "tv = " <+> ppr new_tv
, ptext (sLit "Kicked out =") <+> ppr wl]
; updWorkListTcS (appendWorkList wl) }
where
rest_out = fro_out `andCts` dicts_out `andCts` irs_out
kicked_out = WorkList { wl_eqs = varEnvElts tv_eqs_out
, wl_funeqs = foldrBag insertDeque emptyDeque feqs_out
, wl_rest = bagToList rest_out }
remaining = is { inert_cans = IC { inert_eqs = tv_eqs_in
, inert_eq_tvs = inscope
-- keep the same, safe and cheap
, inert_dicts = dicts_in
, inert_funeqs = feqs_in
, inert_irreds = irs_in }
, inert_frozen = fro_in }
kick_out :: InertSet -> (WorkList, InertSet)
kick_out (is@(IS { inert_cans = IC { inert_eqs = tv_eqs
, inert_dicts = dictmap
, inert_funeqs = funeqmap
, inert_irreds = irreds } }))
= (kicked_out, is { inert_cans = inert_cans_in })
-- NB: Notice that don't rewrite
-- inert_solved_dicts, and inert_solved_funeqs
-- optimistically. But when we lookup we have to take the
-- subsitution into account
where
inert_cans_in = IC { inert_eqs = tv_eqs_in
, inert_dicts = dicts_in
, inert_funeqs = feqs_in
, inert_irreds = irs_in }
kicked_out = WorkList { wl_eqs = varEnvElts tv_eqs_out
, wl_funeqs = foldrBag insertDeque emptyDeque feqs_out
, wl_rest = bagToList (dicts_out `andCts` irs_out) }
(tv_eqs_out, tv_eqs_in) = partitionVarEnv kick_out_eq tv_eqs
(feqs_out, feqs_in) = partCtFamHeadMap kick_out_ct funeqmap
(dicts_out, dicts_in) = partitionCCanMap kick_out_ct dictmap
(irs_out, irs_in) = partitionBag kick_out_ct irreds
(tv_eqs_out, tv_eqs_in) = partitionVarEnv kick_out_eq tv_eqs
(feqs_out, feqs_in) = partCtFamHeadMap kick_out funeqmap
(dicts_out, dicts_in) = partitionCCanMap kick_out dictmap
(irs_out, irs_in) = partitionBag kick_out irreds
(fro_out, fro_in) = partitionBag kick_out frozen
kick_out inert_ct = new_flav `canRewrite` (ctFlavour inert_ct) &&
(new_tv `elemVarSet` tyVarsOfCt inert_ct)
kick_out_ct inert_ct = new_flav `canRewrite` (ctFlavour inert_ct) &&
(new_tv `elemVarSet` tyVarsOfCt inert_ct)
-- NB: tyVarsOfCt will return the type
-- variables /and the kind variables/ that are
-- directly visible in the type. Hence we will
......@@ -374,7 +366,8 @@ kickOutRewritable new_flav new_tv
-- constraints that mention type variables whose
-- kinds could contain this variable!
kick_out_eq inert_ct = kick_out inert_ct && not (ctFlavour inert_ct `canRewrite` new_flav)
kick_out_eq inert_ct = kick_out_ct inert_ct &&
not (ctFlavour inert_ct `canRewrite` new_flav)
-- If also the inert can rewrite the subst then there is no danger of
-- occurs check errors sor keep it there. No need to rewrite the inert equality
-- (as we did in the past) because of point (8) of
......
......@@ -859,10 +859,10 @@ data Ct
| CIrredEvCan { -- These stand for yet-unknown predicates
cc_ev :: CtEvidence, -- See Note [Ct/evidence invariant]
cc_ty :: Xi, -- cc_ty is flat hence it may only be of the form (tv xi1 xi2 ... xin)
-- 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_ty :: Xi, -- cc_ty is flat hence it may only be of the form (tv xi1 xi2 ... xin)
-- 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]
}
......@@ -882,7 +882,7 @@ data Ct
| CFunEqCan { -- F xis ~ xi
-- Invariant: * isSynFamilyTyCon cc_fun
-- * typeKind (F xis) `compatKind` typeKind xi
cc_ev :: CtEvidence, -- See Note [Ct/evidence invariant]
cc_ev :: CtEvidence, -- See Note [Ct/evidence invariant]
cc_fun :: TyCon, -- A type function
cc_tyargs :: [Xi], -- Either under-saturated or exactly saturated
cc_rhs :: Xi, -- *never* over-saturated (because if so
......@@ -893,8 +893,8 @@ data Ct
}
| CNonCanonical { -- See Note [NonCanonical Semantics]
cc_ev :: CtEvidence,
cc_depth :: SubGoalDepth
cc_ev :: CtEvidence,
cc_depth :: SubGoalDepth
}
\end{code}
......@@ -1094,6 +1094,7 @@ data Implication
ic_skols :: [TcTyVar], -- Introduced skolems
-- See Note [Skolems in an implication]
-- See Note [Shadowing in a constraint]
ic_fsks :: [TcTyVar], -- Extra flatten-skolems introduced by the flattening
-- done by canonicalisation.
......@@ -1128,6 +1129,18 @@ instance Outputable Implication where
, ppr (ctLocSpan loc) ])
\end{code}
Note [Shadowing in a constraint]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We assume NO SHADOWING in a constraint. Specifically
* The unification variables are all implicitly quantified at top
level, and are all unique
* The skolem varibles bound in ic_skols are all freah when the
implication is created.
So we can safely substitute. For example, if we have
forall a. a~Int => ...(forall b. ...a...)...
we can push the (a~Int) constraint inwards in the "givens" without
worrying that 'b' might clash.
Note [Skolems in an implication]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The skolems in an implication are not there to perform a skolem escape
......
......@@ -454,8 +454,6 @@ data InertCans
-- a |-> ct,co
-- Then ct = CTyEqCan { cc_tyvar = a, cc_rhs = xi }
-- And co : a ~ xi
, inert_eq_tvs :: InScopeSet
-- Superset of the type variables of inert_eqs
, inert_dicts :: CCanMap Class
-- Dictionaries only, index is the class
-- NB: index is /not/ the whole type because FD reactions
......@@ -535,7 +533,7 @@ data InertSet
-- Canonical Given, Wanted, Derived (no Solved)
-- Sometimes called "the inert set"
, inert_frozen :: Cts
, inert_insols :: Cts
-- Frozen errors (as non-canonicals)
, inert_fsks :: [TcTyVar] -- Flatten-skolems allocated in this local scope
......@@ -575,18 +573,17 @@ instance Outputable InertCans where
instance Outputable InertSet where
ppr is = vcat [ ppr $ inert_cans is
, text "Frozen errors =" <+> -- Clearly print frozen errors
braces (vcat (map ppr (Bag.bagToList $ inert_frozen is)))
braces (vcat (map ppr (Bag.bagToList $ inert_insols is)))
, text "Solved dicts" <+> int (sizePredMap (inert_solved_dicts is))
, text "Solved funeqs" <+> int (sizeFamHeadMap (inert_solved_funeqs is))]
emptyInert :: InertSet
emptyInert
= IS { inert_cans = IC { inert_eqs = emptyVarEnv
, inert_eq_tvs = emptyInScopeSet
, inert_dicts = emptyCCanMap
, inert_funeqs = FamHeadMap emptyTM
, inert_irreds = emptyCts }
, inert_frozen = emptyCts
, inert_insols = emptyCts
, inert_fsks = []
, inert_solved_dicts = PredMap emptyTM
, inert_solved_funeqs = FamHeadMap emptyTM }
......@@ -594,14 +591,10 @@ emptyInert
insertInertItem :: Ct -> InertSet -> InertSet
-- Add a new inert element to the inert set.
insertInertItem item is
| isCNonCanonical item
-- NB: this may happen if we decide to kick some frozen error
-- out to rewrite him. Frozen errors are just NonCanonicals
= is { inert_frozen = inert_frozen is `Bag.snocBag` item }
| otherwise
-- A canonical Given, Wanted, or Derived
= is { inert_cans = upd_inert_cans (inert_cans is) item }
= -- A canonical Given, Wanted, or Derived
ASSERT2( not (isCNonCanonical item), ppr item )
-- Can't be CNonCanonical, because they only land in inert_insols
is { inert_cans = upd_inert_cans (inert_cans is) item }
where upd_inert_cans :: InertCans -> Ct -> InertCans
-- Precondition: item /is/ canonical
......@@ -614,10 +607,8 @@ insertInertItem item is
eqs' = extendVarEnv_C upd_err (inert_eqs ics)
(cc_tyvar item) item
inscope' = extendInScopeSetSet (inert_eq_tvs ics)
(tyVarsOfCt item)
in ics { inert_eqs = eqs', inert_eq_tvs = inscope' }
in ics { inert_eqs = eqs' }
| isCIrredEvCan item -- Presently-irreducible evidence
= ics { inert_irreds = inert_irreds ics `Bag.snocBag` item }
......@@ -689,17 +680,15 @@ updInertTcS upd
prepareInertsForImplications :: InertSet -> InertSet
-- See Note [Preparing inert set for implications]
prepareInertsForImplications is
= is { inert_cans = getGivens (inert_cans is)
, inert_fsks = []
, inert_frozen = emptyCts }
= is { inert_cans = getGivens (inert_cans is)
, inert_fsks = []
, inert_insols = emptyCts }
where
getGivens (IC { inert_eq_tvs = eq_tvs
, inert_eqs = eqs
getGivens (IC { inert_eqs = eqs
, inert_irreds = irreds
, inert_funeqs = FamHeadMap funeqs
, inert_dicts = dicts })
= IC { inert_eq_tvs = eq_tvs
, inert_eqs = filterVarEnv_Directly (\_ ct -> isGivenCt ct) eqs
= IC { inert_eqs = filterVarEnv_Directly (\_ ct -> isGivenCt ct) eqs
, inert_funeqs = FamHeadMap (mapTM given_from_wanted funeqs)
, inert_irreds = Bag.filterBag isGivenCt irreds
, inert_dicts = keepGivenCMap dicts }
......@@ -759,10 +748,9 @@ alpha. (In general we can't float class constraints out just in case
\begin{code}
getInertEqs :: TcS (TyVarEnv Ct, InScopeSet)
getInertEqs :: TcS (TyVarEnv Ct)
getInertEqs = do { inert <- getTcSInerts
; let ics = inert_cans inert
; return (inert_eqs ics, inert_eq_tvs ics) }
; return (inert_eqs (inert_cans inert)) }
getInertUnsolved :: TcS (Cts, Cts)
-- Return (unsolved-wanteds, insolubles)
......@@ -779,7 +767,7 @@ getInertUnsolved
unsolved_flats = unsolved_eqs `unionBags` unsolved_irreds `unionBags`
unsolved_dicts `unionBags` unsolved_funeqs
; return (unsolved_flats, inert_frozen is) }
; return (unsolved_flats, inert_insols is) }
where
add_if_unsolved ct cts
| is_unsolved ct = cts `extendCts` ct
......@@ -801,7 +789,7 @@ checkAllSolved
; return (not (unsolved_eqs || unsolved_irreds
|| unsolved_dicts || unsolved_funeqs
|| not (isEmptyBag (inert_frozen is)))) }
|| not (isEmptyBag (inert_insols is)))) }
extractRelevantInerts :: Ct -> TcS Cts
-- Returns the constraints from the inert set that are 'relevant' to react with
......@@ -959,6 +947,9 @@ panicTcS doc = pprPanic "TcCanonical" doc
traceTcS :: String -> SDoc -> TcS ()
traceTcS herald doc = wrapTcS (TcM.traceTc herald doc)
instance HasDynFlags TcS where
getDynFlags = wrapTcS getDynFlags
bumpStepCountTcS :: TcS ()
bumpStepCountTcS = TcS $ \env -> do { let ref = tcs_count env
; n <- TcM.readTcRef ref
......@@ -1157,21 +1148,17 @@ emitFrozenError :: CtEvidence -> SubGoalDepth -> TcS ()
-- Emits a non-canonical constraint that will stand for a frozen error in the inerts.
emitFrozenError fl depth
= do { traceTcS "Emit frozen error" (ppr (ctEvPred fl))
; inert_ref <- getTcSInertsRef
; wrapTcS $ do
{ inerts <- TcM.readTcRef inert_ref
; let old_insols = inert_frozen inerts
ct = CNonCanonical { cc_ev = fl, cc_depth = depth }
inerts_new = inerts { inert_frozen = extendCts old_insols ct }
this_pred = ctEvPred fl
already_there = not (isWanted fl) && anyBag (eqType this_pred . ctPred) old_insols
; updInertTcS add_insol }
where
add_insol inerts@(IS { inert_insols = old_insols })
| already_there = inerts
| otherwise = inerts { inert_insols = extendCts old_insols insol_ct }
where
already_there = not (isWanted fl) && anyBag (eqType this_pred . ctPred) old_insols
-- See Note [Do not add duplicate derived insolubles]
; unless already_there $
TcM.writeTcRef inert_ref inerts_new } }
instance HasDynFlags TcS where
getDynFlags = wrapTcS getDynFlags
insol_ct = CNonCanonical { cc_ev = fl, cc_depth = depth }
this_pred = ctEvPred fl
getTcEvBinds :: TcS EvBindsVar
getTcEvBinds = TcS (return . tcs_ev_binds)
......
......@@ -802,10 +802,6 @@ solveNestedImplications implics
; (floated_eqs, unsolved_implics)
<- flatMapBagPairM (solveImplication thinner_inerts) implics
; promoteFloatedUnificationVars floated_eqs
-- Performs some unifications, adding to monadically-carried ty_binds
-- These will be used when processing floated_eqs later
-- ... and we are back in the original TcS inerts
-- Notice that the original includes the _insoluble_flats so it was safe to ignore
-- them in the beginning of this function.
......@@ -829,64 +825,57 @@ solveImplication inerts
, ic_given = givens
, ic_wanted = wanteds
, ic_loc = loc })
= nestImplicTcS ev_binds untch inerts $
=
do { traceTcS "solveImplication {" (ppr imp)
-- Solve the nested constraints
; solveInteractGiven loc old_fsks givens
; residual_wanted <- solve_wanteds wanteds
; new_fsks <- getFlattenSkols
; let all_fsks = new_fsks ++ old_fsks
(floated_eqs, final_wanted)
= floatEqualities (skols ++ all_fsks) givens residual_wanted
res_implic | isEmptyWC final_wanted
-- NB: 'inerts' has empty inert_fsks
; (new_fsks, residual_wanted)
<- nestImplicTcS ev_binds untch inerts $
do { solveInteractGiven loc old_fsks givens
; residual_wanted <- solve_wanteds wanteds
; more_fsks <- getFlattenSkols
; return (more_fsks ++ old_fsks, residual_wanted) }
; (floated_eqs, final_wanted)
<- floatEqualities (skols ++ new_fsks) givens residual_wanted
; let res_implic | isEmptyWC final_wanted
= emptyBag
| otherwise
= unitBag imp { ic_fsks = all_fsks
, ic_wanted = dropDerivedWC final_wanted
, ic_insol = insolubleWC final_wanted }
= unitBag (imp { ic_fsks = new_fsks
, ic_wanted = dropDerivedWC final_wanted
, ic_insol = insolubleWC final_wanted })
; evbinds <- getTcEvBindsMap
; traceTcS "solveImplication end }" $ vcat
[ text "floated_eqs =" <+> ppr floated_eqs
, text "new_fsks =" <+> ppr all_fsks
, text "new_fsks =" <+> ppr new_fsks
, text "res_implic =" <+> ppr res_implic
, text "implication evbinds = " <+> ppr (evBindMapBinds evbinds) ]
; return (floated_eqs, res_implic) }
\end{code}
Note [Floating equalities]
\begin{code}
promoteFloatedUnificationVars :: Cts -> TcS ()
promoteFloatedUnificationVars cts
= do { untch <- TcSMonad.getUntouchables
; let tvs = filter (isFloatedTouchableMetaTyVar untch) $
varSetElems (tyVarsOfCts cts)
; mapM_ (promote_tv untch) tvs
; ty_binds <- getTcSTyBindsMap
; traceTcS "promoteFloated" (vcat [ text "Ctxt untoucables =" <+> ppr untch
, text "Floated eqs =" <+> ppr cts
, text "Promoted tvs =" <+> ppr tvs
, text "Ty binds =" <+> ppr ty_binds])
; return () }
where
promote_tv untch tv
= do { cloned_tv <- TcSMonad.cloneMetaTyVar tv
; let rhs_tv = setMetaTyVarUntouchables cloned_tv untch
; setWantedTyBind tv (mkTyVarTy rhs_tv) }
floatEqualities :: [TcTyVar] -> [EvVar] -> WantedConstraints -> (Cts, WantedConstraints)
floatEqualities :: [TcTyVar] -> [EvVar] -> WantedConstraints
-> TcS (Cts, WantedConstraints)
-- Post: The returned FlavoredEvVar's are only Wanted or Derived
-- and come from the input wanted ev vars or deriveds
-- Also performs some unifications, adding to monadically-carried ty_binds
-- These will be used when processing floated_eqs later
floatEqualities skols can_given wanteds@(WC { wc_flat = flats })
| hasEqualities can_given
= (emptyBag, wanteds) -- Note [Float Equalities out of Implications]
= return (emptyBag, wanteds) -- Note [Float Equalities out of Implications]
| otherwise
= (float_eqs, wanteds { wc_flat = remaining_flats })
= do { untch <- TcSMonad.getUntouchables
; mapM_ (promote_tv untch) (varSetElems (tyVarsOfCts float_eqs))
; ty_binds <- getTcSTyBindsMap
; traceTcS "floatEqualities" (vcat [ text "Ctxt untoucables =" <+> ppr untch
, text "Floated eqs =" <+> ppr float_eqs
, text "Ty binds =" <+> ppr ty_binds])
; return (float_eqs, wanteds { wc_flat = remaining_flats }) }
where
(float_eqs, remaining_flats) = partitionBag is_floatable flats
skol_set = growSkols wanteds (mkVarSet skols)
......@@ -897,6 +886,14 @@ floatEqualities skols can_given wanteds@(WC { wc_flat = flats })
where
pred = ctPred ct
promote_tv untch tv
| isFloatedTouchableMetaTyVar untch tv
= do { cloned_tv <- TcSMonad.cloneMetaTyVar tv
; let rhs_tv = setMetaTyVarUntouchables cloned_tv untch
; setWantedTyBind tv (mkTyVarTy rhs_tv) }
| otherwise
= return ()
growSkols :: WantedConstraints -> VarSet -> VarSet
-- Find all the type variables that might possibly be unified
-- with a type that mentions a skolem. This test is very conservative.
......
......@@ -319,6 +319,31 @@ vanillaSkolemTv = SkolemTv False -- Might be instantiated
superSkolemTv = SkolemTv True -- Treat this as a completely distinct type
-------------------------
newtype Untouchables = Untouchables Int
noUntouchables :: Untouchables
noUntouchables = Untouchables 0 -- 0 = outermost level
pushUntouchables :: Unique -> Untouchables -> Untouchables
pushUntouchables _ (Untouchables us) = Untouchables (us+1)
isFloatedTouchable :: Untouchables -> Untouchables -> Bool
isFloatedTouchable (Untouchables ctxt_untch) (Untouchables tv_untch)
= ctxt_untch < tv_untch
isTouchable :: Untouchables -> Untouchables -> Bool
isTouchable (Untouchables ctxt_untch) (Untouchables tv_untch)
= ctxt_untch == tv_untch -- NB: invariant ctxt_untch >= tv_untch
-- So <= would be equivalent
checkTouchableInvariant :: Untouchables -> Untouchables -> Bool
checkTouchableInvariant (Untouchables ctxt_untch) (Untouchables tv_untch)
= ctxt_untch >= tv_untch
instance Outputable Untouchables where
ppr (Untouchables us) = ppr us
{- OLD
newtype Untouchables = Untouchables [Unique]
noUntouchables :: Untouchables
......@@ -343,6 +368,8 @@ isTouchable (Untouchables ctxt_untch) (Untouchables tv_untch)
instance Outputable Untouchables where
ppr (Untouchables us) = pprWithCommas ppr us
-}
-----------------------------
data MetaDetails
......@@ -705,7 +732,10 @@ isTouchableMetaTyVar :: Untouchables -> TcTyVar -> Bool
isTouchableMetaTyVar ctxt_untch tv
= ASSERT2( isTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
MetaTv { mtv_untch = tv_untch } -> isTouchable ctxt_untch tv_untch
MetaTv { mtv_untch = tv_untch }
-> ASSERT2( checkTouchableInvariant ctxt_untch tv_untch,
ppr tv $$ ppr tv_untch $$ ppr ctxt_untch )
isTouchable ctxt_untch tv_untch
_ -> False
isFloatedTouchableMetaTyVar :: Untouchables -> TcTyVar -> Bool
......
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