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
; 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
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 }
| 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)
, ("Unambiguous", unambiguous, reportFlatErrs ctxt) ]
(reportAmbigErrs ctxt)
- (bagToList (insols `unionBags` flats))
+ (bagToList flats)
where
utterly_wrong, skolem_eq, unambiguous :: Ct -> PredTree -> Bool
\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]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
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
-- 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
| 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]
}
| 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
}
| CNonCanonical { -- See Note [NonCanonical Semantics]
- cc_ev :: CtEvidence,
- cc_depth :: SubGoalDepth
+ cc_ev :: CtEvidence,
+ cc_depth :: SubGoalDepth
}
\end{code}
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.
, 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
-- 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
-- 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
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 }
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
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 }
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 }
\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)
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
; 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
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
-- 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)
; (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.
, 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)
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.
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
instance Outputable Untouchables where
ppr (Untouchables us) = pprWithCommas ppr us
+-}
+
-----------------------------
data MetaDetails
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
git.haskell.org / ghc.git / commitdiff
