Commit 2bbdd00c authored by Simon Peyton Jones's avatar Simon Peyton Jones

Orient TyVar/TyVar equalities with deepest on the left

Trac #15009 showed that, for Given TyVar/TyVar equalities, we really
want to orient them with the deepest-bound skolem on the left. As it
happens, we also want to do the same for Wanteds, but for a different
reason (more likely to be touchable).  Either way, deepest wins:
see TcUnify Note [Deeper level on the left].

This observation led me to some significant changes:

* A SkolemTv already had a TcLevel, but the level wasn't really being
  used.   Now it is!

* I updated added invariant (SkolInf) to TcType
  Note [TcLevel and untouchable type variables], documenting that
  the level number of all the ic_skols should be the same as the
  ic_tclvl of the implication

* FlatSkolTvs and FlatMetaTvs previously had a dummy level-number of
  zero, which messed the scheme up.   Now they get a level number the
  same way as all other TcTyVars, instead of being a special case.

* To make sure that FlatSkolTvs and FlatMetaTvs are untouchable (which
  was previously done via their magic zero level) isTouchableMetaTyVar
  just tests for those two cases.

* TcUnify.swapOverTyVars is the crucial orientation function; see the
  new Note [TyVar/TyVar orientation].  I completely rewrote this function,
  and it's now much much easier to understand.

I ended up doing some related refactoring, of course

* I noticed that tcImplicitTKBndrsX and tcExplicitTKBndrsX were doing
  a lot of useless work in the case where there are no skolems; I
  added a fast-patch

* Elminate the un-used tcExplicitTKBndrsSig; and thereby get rid of
  the higher-order parameter to tcExpliciTKBndrsX.

* Replace TcHsType.emitTvImplication with TcUnify.checkTvConstraints,
  by analogy with TcUnify.checkConstraints.

* Inline TcUnify.buildImplication into its only call-site in
  TcUnify.checkConstraints

* TcS.buildImplication becomes TcS.CheckConstraintsTcS, with a
  simpler API

* Now that we have NoEvBindsVar we have no need of termEvidenceAllowed;
  nuke the latter, adding Note [No evidence bindings] to TcEvidence.
parent efe40544
......@@ -747,14 +747,9 @@ can_eq_nc_forall ev eq_rel s1 s2
empty_subst2 = mkEmptyTCvSubst (getTCvInScope subst1)
; (implic, _ev_binds, all_co) <- buildImplication skol_info skol_tvs [] $
go skol_tvs empty_subst2 bndrs2
-- We have nowhere to put these bindings
-- but TcSimplify.setImplicationStatus
-- checks that we don't actually use them
-- when skol_info = UnifyForAllSkol
; updWorkListTcS (extendWorkListImplic implic)
; all_co <- checkConstraintsTcS skol_info skol_tvs $
go skol_tvs empty_subst2 bndrs2
; setWantedEq orig_dest all_co
; stopWith ev "Deferred polytype equality" } }
......@@ -1757,24 +1752,6 @@ canEqTyVarTyVar, are these
substituted out Note [Elminate flat-skols]
fsk ~ a
Note [Eliminate flat-skols]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have [G] Num (F [a])
then we flatten to
[G] Num fsk
[G] F [a] ~ fsk
where fsk is a flatten-skolem (FlatSkolTv). Suppose we have
type instance F [a] = a
then we'll reduce the second constraint to
[G] a ~ fsk
and then replace all uses of 'a' with fsk. That's bad because
in error messages intead of saying 'a' we'll say (F [a]). In all
places, including those where the programmer wrote 'a' in the first
place. Very confusing! See Trac #7862.
Solution: re-orient a~fsk to fsk~a, so that we preferentially eliminate
the fsk.
Note [Equalities with incompatible kinds]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
What do we do when we have an equality
......
......@@ -413,10 +413,9 @@ reportImplic ctxt implic@(Implic { ic_skols = tvs, ic_telescope = m_telescope
, ic_given = map (tidyEvVar env1) given
, ic_info = info' }
ctxt1 | NoEvBindsVar{} <- evb = noDeferredBindings ctxt
| termEvidenceAllowed info = ctxt
| otherwise = noDeferredBindings ctxt
| otherwise = ctxt
-- If we go inside an implication that has no term
-- evidence (i.e. unifying under a forall), we can't defer
-- evidence (e.g. unifying under a forall), we can't defer
-- type errors. You could imagine using the /enclosing/
-- bindings (in cec_binds), but that may not have enough stuff
-- in scope for the bindings to be well typed. So we just
......
......@@ -401,10 +401,9 @@ data EvBindsVar
-- See Note [Tracking redundant constraints] in TcSimplify
}
| NoEvBindsVar { -- used when we're solving only for equalities,
-- which don't have bindings
| NoEvBindsVar { -- See Note [No evidence bindings]
-- see above for comments
-- See above for comments on ebv_uniq, evb_tcvs
ebv_uniq :: Unique,
ebv_tcvs :: IORef CoVarSet
}
......@@ -415,6 +414,21 @@ instance Data.Data TcEvBinds where
gunfold _ _ = error "gunfold"
dataTypeOf _ = Data.mkNoRepType "TcEvBinds"
{- Note [No evidence bindings]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Class constraints etc give rise to /term/ bindings for evidence, and
we have nowhere to put term bindings in /types/. So in some places we
use NoEvBindsVar (see newNoTcEvBinds) to signal that no term-level
evidence bindings are allowed. Notebly ():
- Places in types where we are solving kind constraints (all of which
are equalities); see solveEqualities, solveLocalEqualities,
checkTvConstraints
- When unifying forall-types
-}
-----------------
newtype EvBindMap
= EvBindMap {
......
......@@ -18,8 +18,8 @@ module TcHsType (
tcHsDeriv, tcHsVectInst,
tcHsTypeApp,
UserTypeCtxt(..),
tcImplicitTKBndrs, tcImplicitTKBndrsX, tcImplicitTKBndrsSig,
tcExplicitTKBndrs, tcExplicitTKBndrsX, tcExplicitTKBndrsSig,
tcImplicitTKBndrs, tcImplicitTKBndrsX,
tcExplicitTKBndrs,
kcExplicitTKBndrs, kcImplicitTKBndrs,
-- Type checking type and class decls
......@@ -247,11 +247,12 @@ tc_hs_sig_type_and_gen skol_info (HsIB { hsib_ext
-- kind variables floating about, immediately prior to
-- kind generalisation
-- We use "InKnot", because this is called on class method sigs
-- in the knot
-- We use the "InKnot" zonker, because this is called
-- on class method sigs in the knot
; ty1 <- zonkPromoteTypeInKnot $ mkSpecForAllTys tkvs ty
; kvs <- kindGeneralize ty1
; zonkSigType (mkInvForAllTys kvs ty1) }
tc_hs_sig_type_and_gen _ (XHsImplicitBndrs _) _ = panic "tc_hs_sig_type_and_gen"
tc_hs_sig_type :: SkolemInfo -> LHsSigType GhcRn -> Kind -> TcM Type
......@@ -267,6 +268,7 @@ tc_hs_sig_type skol_info (HsIB { hsib_ext = HsIBRn { hsib_vars = sig_vars }
-- need to promote any remaining metavariables; test case:
-- dependent/should_fail/T14066e.
; zonkPromoteType (mkSpecForAllTys tkvs ty) }
tc_hs_sig_type _ (XHsImplicitBndrs _) _ = panic "tc_hs_sig_type"
-----------------
......@@ -395,7 +397,7 @@ Answer: we use the same rule as for value bindings:
* Additionally, we attempt to generalise if we have NoMonoLocalBinds
Trac #13337 shows the problem if we kind-generalise an open type (i.e.
one that mentions in-scope tpe variable
one that mentions in-scope type variable
foo :: forall k (a :: k) proxy. (Typeable k, Typeable a)
=> proxy a -> String
foo _ = case eqT :: Maybe (k :~: Type) of
......@@ -407,7 +409,7 @@ but (Int :: Type). Since (:~:) is kind-homogeneous, this requires
k ~ *, which is true in the Refl branch of the outer case.
That equality will be solved if we allow it to float out to the
implication constraint for the Refl match, bnot not if we aggressively
implication constraint for the Refl match, but not not if we aggressively
attempt to solve all equalities the moment they occur; that is, when
checking (Maybe (a :~: Int)). (NB: solveEqualities fails unless it
solves all the kind equalities, which is the right thing at top level.)
......@@ -1766,24 +1768,31 @@ tcImplicitTKBndrsX :: (Name -> Kind -> TcM TcTyVar) -- new_tv function
-> [Name]
-> TcM a
-> TcM ([TcTyVar], a) -- these tyvars are dependency-ordered
-- Returned TcTyVars have the supplied HsTyVarBndrs,
-- but may be in different order to the original [Name]
-- * Guarantees to call solveLocalEqualities to unify
-- all constraints from thing_inside.
--
-- * Returned TcTyVars have the supplied HsTyVarBndrs,
-- but may be in different order to the original [Name]
-- (because of sorting to respect dependency)
-- Returned TcTyVars have zonked kinds
-- See Note [Keeping scoped variables in order: Implicit]
--
-- * Returned TcTyVars have zonked kinds
-- See Note [Keeping scoped variables in order: Implicit]
tcImplicitTKBndrsX new_tv m_kind skol_info tv_names thing_inside
| null tv_names -- Short cut for the common case where there
-- are no implicit type variables to bind
= do { result <- solveLocalEqualities thing_inside
; return ([], result) }
| otherwise
= do { (skol_tvs, result)
<- solveLocalEqualities $
do { (inner_tclvl, wanted, (skol_tvs, result))
<- pushLevelAndCaptureConstraints $
do { tv_pairs <- mapM (tcHsTyVarName new_tv m_kind) tv_names
; let must_scope_tvs = [ tv | (tv, False) <- tv_pairs ]
; result <- tcExtendTyVarEnv must_scope_tvs $
thing_inside
; return (map fst tv_pairs, result) }
checkTvConstraints skol_info Nothing $
do { tv_pairs <- mapM (tcHsTyVarName new_tv m_kind) tv_names
; let must_scope_tvs = [ tv | (tv, False) <- tv_pairs ]
; result <- tcExtendTyVarEnv must_scope_tvs $
thing_inside
; return (map fst tv_pairs, result) }
; emitTvImplication inner_tclvl skol_tvs Nothing wanted skol_info
; return (skol_tvs, result) }
; skol_tvs <- mapM zonkTcTyCoVarBndr skol_tvs
-- use zonkTcTyCoVarBndr because a skol_tv might be a SigTv
......@@ -1812,24 +1821,8 @@ tcExplicitTKBndrs :: SkolemInfo
-> [LHsTyVarBndr GhcRn]
-> TcM a
-> TcM ([TcTyVar], a)
-- No cloning: returned TyVars have the same Name as the incoming LHsTyVarBndrs
tcExplicitTKBndrs = tcExplicitTKBndrsX newSkolemTyVar
-- | This brings a bunch of tyvars into scope as SigTvs, where they can unify
-- with other type *variables* only.
tcExplicitTKBndrsSig :: SkolemInfo
-> [LHsTyVarBndr GhcRn]
-> TcM a
-> TcM ([TcTyVar], a)
tcExplicitTKBndrsSig = tcExplicitTKBndrsX newSigTyVar
tcExplicitTKBndrsX :: (Name -> Kind -> TcM TyVar)
-> SkolemInfo
-> [LHsTyVarBndr GhcRn]
-> TcM a
-> TcM ([TcTyVar], a)
-- See also Note [Associated type tyvar names] in Class
tcExplicitTKBndrsX new_tv skol_info hs_tvs thing_inside
tcExplicitTKBndrs skol_info hs_tvs thing_inside
-- This function brings into scope a telescope of binders as written by
-- the user. At first blush, it would then seem that we should bring
-- them into scope one at a time, bumping the TcLevel each time.
......@@ -1840,11 +1833,16 @@ tcExplicitTKBndrsX new_tv skol_info hs_tvs thing_inside
-- notice that the telescope is out of order. That's what we do here,
-- following the logic of tcImplicitTKBndrsX.
-- See also Note [Keeping scoped variables in order: Explicit]
= do { (inner_tclvl, wanted, (skol_tvs, result))
<- pushLevelAndCaptureConstraints $
bind_tvbs hs_tvs
--
-- No cloning: returned TyVars have the same Name as the incoming LHsTyVarBndrs
| null hs_tvs -- Short cut that avoids creating an implication
-- constraint in the common case where none is needed
= do { result <- thing_inside
; return ([], result) }
; emitTvImplication inner_tclvl skol_tvs (Just doc) wanted skol_info
| otherwise
= do { (skol_tvs, result) <- checkTvConstraints skol_info (Just doc) $
bind_tvbs hs_tvs
; traceTc "tcExplicitTKBndrs" $
vcat [ text "Hs vars:" <+> ppr hs_tvs
......@@ -1856,7 +1854,7 @@ tcExplicitTKBndrsX new_tv skol_info hs_tvs thing_inside
bind_tvbs [] = do { result <- thing_inside
; return ([], result) }
bind_tvbs (L _ tvb : tvbs)
= do { (tv, in_scope) <- tcHsTyVarBndr new_tv tvb
= do { (tv, in_scope) <- tcHsTyVarBndr newSkolemTyVar tvb
; (if in_scope then id else tcExtendTyVarEnv [tv]) $
do { (tvs, result) <- bind_tvbs tvbs
; return (tv : tvs, result) }}
......@@ -1874,28 +1872,6 @@ kcExplicitTKBndrs (L _ hs_tv : hs_tvs) thing_inside
; tcExtendTyVarEnv [tv] $
kcExplicitTKBndrs hs_tvs thing_inside }
-- | Build and emit an Implication appropriate for type-checking a type.
-- This assumes all constraints will be equality constraints, and
-- so does not create an EvBindsVar
emitTvImplication :: TcLevel -- of the constraints
-> [TcTyVar] -- skolems
-> Maybe SDoc -- user-written telescope, if present
-> WantedConstraints
-> SkolemInfo
-> TcM ()
emitTvImplication inner_tclvl skol_tvs m_telescope wanted skol_info
= do { tc_lcl_env <- getLclEnv
; ev_binds <- newNoTcEvBinds
; let implic = newImplication { ic_tclvl = inner_tclvl
, ic_skols = skol_tvs
, ic_telescope = m_telescope
, ic_no_eqs = True
, ic_wanted = wanted
, ic_binds = ev_binds
, ic_info = skol_info
, ic_env = tc_lcl_env }
; emitImplication implic }
tcHsTyVarBndr :: (Name -> Kind -> TcM TyVar)
-> HsTyVarBndr GhcRn -> TcM (TcTyVar, Bool)
-- Return a TcTyVar, built using the provided function
......
......@@ -512,13 +512,24 @@ tcInstSkolTyVars' overlappable subst tvs
; instSkolTyCoVarsX (mkTcSkolTyVar lvl loc overlappable) subst tvs }
mkTcSkolTyVar :: TcLevel -> SrcSpan -> Bool -> TcTyCoVarMaker gbl lcl
mkTcSkolTyVar lvl loc overlappable old_name kind
-- Allocates skolems whose level is ONE GREATER THAN the passed-in tc_lvl
-- See Note [Skolem level allocation]
mkTcSkolTyVar tc_lvl loc overlappable old_name kind
= do { uniq <- newUnique
; let name = mkInternalName uniq (getOccName old_name) loc
; return (mkTcTyVar name kind details) }
where
details = SkolemTv (pushTcLevel lvl) overlappable
-- NB: skolems bump the level
details = SkolemTv (pushTcLevel tc_lvl) overlappable
-- pushTcLevel: see Note [Skolem level allocation]
{- Note [Skolem level allocation]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We generally allocate skolems /before/ calling pushLevelAndCaptureConstraints.
So we want their level to the level of the soon-to-be-created implication,
which has a level one higher than the current level. Hence the pushTcLevel.
It feels like a slight hack. Applies also to vanillaSkolemTv.
-}
------------------
freshenTyVarBndrs :: [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyVar])
......@@ -569,9 +580,10 @@ newFskTyVar :: TcType -> TcM TcTyVar
newFskTyVar fam_ty
= do { uniq <- newUnique
; ref <- newMutVar Flexi
; tclvl <- getTcLevel
; let details = MetaTv { mtv_info = FlatSkolTv
, mtv_ref = ref
, mtv_tclvl = fmvTcLevel }
, mtv_tclvl = tclvl }
name = mkMetaTyVarName uniq (fsLit "fsk")
; return (mkTcTyVar name (typeKind fam_ty) details) }
......@@ -624,9 +636,10 @@ newFmvTyVar :: TcType -> TcM TcTyVar
newFmvTyVar fam_ty
= do { uniq <- newUnique
; ref <- newMutVar Flexi
; tclvl <- getTcLevel
; let details = MetaTv { mtv_info = FlatMetaTv
, mtv_ref = ref
, mtv_tclvl = fmvTcLevel }
, mtv_tclvl = tclvl }
name = mkMetaTyVarName uniq (fsLit "s")
; return (mkTcTyVar name (typeKind fam_ty) details) }
......
......@@ -636,9 +636,9 @@ tcPatSynMatcher (L loc name) lpat
(args, arg_tys) pat_ty
= do { rr_name <- newNameAt (mkTyVarOcc "rep") loc
; tv_name <- newNameAt (mkTyVarOcc "r") loc
; let rr_tv = mkTcTyVar rr_name runtimeRepTy vanillaSkolemTv
; let rr_tv = mkTyVar rr_name runtimeRepTy
rr = mkTyVarTy rr_tv
res_tv = mkTcTyVar tv_name (tYPE rr) vanillaSkolemTv
res_tv = mkTyVar tv_name (tYPE rr)
res_ty = mkTyVarTy res_tv
is_unlifted = null args && null prov_dicts
(cont_args, cont_arg_tys)
......@@ -686,7 +686,7 @@ tcPatSynMatcher (L loc name) lpat
}
match = mkMatch (mkPrefixFunRhs (L loc name)) []
(mkHsLams (rr_tv:res_tv:univ_tvs)
req_dicts body')
req_dicts body')
(noLoc (EmptyLocalBinds noExt))
mg :: MatchGroup GhcTc (LHsExpr GhcTc)
mg = MG{ mg_alts = L (getLoc match) [match]
......
......@@ -106,7 +106,6 @@ module TcRnTypes(
SkolemInfo(..), pprSigSkolInfo, pprSkolInfo,
termEvidenceAllowed,
CtEvidence(..), TcEvDest(..),
mkKindLoc, toKindLoc, mkGivenLoc,
......@@ -3228,14 +3227,6 @@ data SkolemInfo
instance Outputable SkolemInfo where
ppr = pprSkolInfo
termEvidenceAllowed :: SkolemInfo -> Bool
-- Whether an implication constraint with this SkolemInfo
-- is permitted to have term-level evidence. There is
-- only one that is not, associated with unifiying
-- forall-types
termEvidenceAllowed (UnifyForAllSkol {}) = False
termEvidenceAllowed _ = True
pprSkolInfo :: SkolemInfo -> SDoc
-- Complete the sentence "is a rigid type variable bound by..."
pprSkolInfo (SigSkol cx ty _) = pprSigSkolInfo cx ty
......
......@@ -16,7 +16,7 @@ module TcSMonad (
TcS, runTcS, runTcSDeriveds, runTcSWithEvBinds,
failTcS, warnTcS, addErrTcS,
runTcSEqualities,
nestTcS, nestImplicTcS, setEvBindsTcS, buildImplication,
nestTcS, nestImplicTcS, setEvBindsTcS, checkConstraintsTcS,
runTcPluginTcS, addUsedGRE, addUsedGREs,
......@@ -1950,8 +1950,12 @@ getNoGivenEqs tclvl skol_tvs
-- outer context but were refined to an insoluble by
-- a local equality; so do /not/ add ct_given_here.
; traceTcS "getNoGivenEqs" (vcat [ ppr has_given_eqs, ppr inerts
, ppr insols])
; traceTcS "getNoGivenEqs" $
vcat [ if has_given_eqs then text "May have given equalities"
else text "No given equalities"
, text "Skols:" <+> ppr skol_tvs
, text "Inerts:" <+> ppr inerts
, text "Insols:" <+> ppr insols]
; return (not has_given_eqs, insols) }
where
eqs_given_here :: EqualCtList -> Bool
......@@ -2094,6 +2098,10 @@ b) 'a' will have been completely substituted out in the inert set,
returned as part of 'fsks'
For an example, see Trac #9211.
See also TcUnify Note [Deeper level on the left] for how we ensure
that the right variable is on the left of the equality when both are
tyvars.
-}
removeInertCts :: [Ct] -> InertCans -> InertCans
......@@ -2704,40 +2712,40 @@ nestTcS (TcS thing_inside)
; return res }
buildImplication :: SkolemInfo
-> [TcTyVar] -- Skolems
-> [EvVar] -- Givens
-> TcS result
-> TcS (Bag Implication, TcEvBinds, result)
-- Just like TcUnify.buildImplication, but in the TcS monnad,
checkConstraintsTcS :: SkolemInfo
-> [TcTyVar] -- Skolems
-> TcS result
-> TcS result
-- Just like TcUnify.checkTvConstraints, but in the TcS monnad,
-- using the work-list to gather the constraints
buildImplication skol_info skol_tvs givens (TcS thing_inside)
= TcS $ \ env ->
checkConstraintsTcS skol_info skol_tvs (TcS thing_inside)
= TcS $ \ tcs_env ->
do { new_wl_var <- TcM.newTcRef emptyWorkList
; tc_lvl <- TcM.getTcLevel
; let new_tclvl = pushTcLevel tc_lvl
; let new_tcs_env = tcs_env { tcs_worklist = new_wl_var }
; res <- TcM.setTcLevel new_tclvl $
thing_inside (env { tcs_worklist = new_wl_var })
; (res, new_tclvl) <- TcM.pushTcLevelM $
thing_inside new_tcs_env
; wl@WL { wl_eqs = eqs } <- TcM.readTcRef new_wl_var
; if null eqs
then return (emptyBag, emptyTcEvBinds, res)
else
do { env <- TcM.getLclEnv
; ev_binds_var <- TcM.newTcEvBinds
; let wc = ASSERT2( null (wl_funeqs wl) && null (wl_rest wl) &&
null (wl_implics wl), ppr wl )
WC { wc_simple = listToCts eqs
, wc_impl = emptyBag }
imp = newImplication { ic_tclvl = new_tclvl
, ic_skols = skol_tvs
, ic_given = givens
, ic_wanted = wc
, ic_binds = ev_binds_var
, ic_env = env
, ic_info = skol_info }
; return (unitBag imp, TcEvBinds ev_binds_var, res) } }
; ASSERT2( null (wl_funeqs wl) && null (wl_rest wl) &&
null (wl_implics wl), ppr wl )
unless (null eqs) $
do { tcl_env <- TcM.getLclEnv
; ev_binds_var <- TcM.newNoTcEvBinds
; let wc = WC { wc_simple = listToCts eqs
, wc_impl = emptyBag }
imp = newImplication { ic_tclvl = new_tclvl
, ic_skols = skol_tvs
, ic_wanted = wc
, ic_binds = ev_binds_var
, ic_env = tcl_env
, ic_info = skol_info }
-- Add the implication to the work-list
; TcM.updTcRef (tcs_worklist tcs_env)
(extendWorkListImplic (unitBag imp)) }
; return res }
{-
Note [Propagate the solved dictionaries]
......@@ -2778,9 +2786,7 @@ getWorkListImplics
updWorkListTcS :: (WorkList -> WorkList) -> TcS ()
updWorkListTcS f
= do { wl_var <- getTcSWorkListRef
; wl_curr <- wrapTcS (TcM.readTcRef wl_var)
; let new_work = f wl_curr
; wrapTcS (TcM.writeTcRef wl_var new_work) }
; wrapTcS (TcM.updTcRef wl_var f)}
emitWorkNC :: [CtEvidence] -> TcS ()
emitWorkNC evs
......
......@@ -1725,19 +1725,13 @@ neededEvVars :: Implication -> TcS Implication
-- - From the 'needed' set, delete ev_bndrs, the binders of the
-- evidence bindings, to give the final needed variables
--
neededEvVars implic@(Implic { ic_info = info
, ic_given = givens
neededEvVars implic@(Implic { ic_given = givens
, ic_binds = ev_binds_var
, ic_wanted = WC { wc_impl = implics }
, ic_need_inner = old_needs })
= do { ev_binds <- TcS.getTcEvBindsMap ev_binds_var
; tcvs <- TcS.getTcEvTyCoVars ev_binds_var
-- Check that there are no term-level evidence bindings
-- in the cases where we have no place to put them
; MASSERT2( termEvidenceAllowed info || isEmptyEvBindMap ev_binds
, ppr info $$ ppr ev_binds )
; let seeds1 = foldrBag add_implic_seeds old_needs implics
seeds2 = foldEvBindMap add_wanted seeds1 ev_binds
seeds3 = seeds2 `unionVarSet` tcvs
......
......@@ -30,7 +30,7 @@ module TcType (
-- TcLevel
TcLevel(..), topTcLevel, pushTcLevel, isTopTcLevel,
strictlyDeeperThan, sameDepthAs, fmvTcLevel,
strictlyDeeperThan, sameDepthAs,
tcTypeLevel, tcTyVarLevel, maxTcLevel,
promoteSkolem, promoteSkolemX, promoteSkolemsX,
--------------------------------
......@@ -44,7 +44,7 @@ module TcType (
isAmbiguousTyVar, metaTyVarRef, metaTyVarInfo,
isFlexi, isIndirect, isRuntimeUnkSkol,
metaTyVarTcLevel, setMetaTyVarTcLevel, metaTyVarTcLevel_maybe,
isTouchableMetaTyVar, isTouchableOrFmv,
isTouchableMetaTyVar,
isFloatedTouchableMetaTyVar,
findDupSigTvs, mkTyVarNamePairs,
......@@ -282,8 +282,6 @@ However, the type checker and constraint solver can encounter type
variables that use the 'TyVar' variant of Var.Var, for a couple of
reasons:
- When unifying or flattening under (forall a. ty)
- When typechecking a class decl, say
class C (a :: k) where
foo :: T a -> Int
......@@ -295,7 +293,10 @@ reasons:
See calls to tcExtendTyVarEnv for other places that ordinary
TyVars are bought into scope, and hence may show up in the types
and inds generated by TcHsType.
and kinds generated by TcHsType.
- The pattern-match overlap checker calls the constraint solver,
long afer TcTyVars have been zonked away
It's convenient to simply treat these TyVars as skolem constants,
which of course they are. So
......@@ -503,6 +504,8 @@ we would need to enforce the separation.
data TcTyVarDetails
= SkolemTv -- A skolem
TcLevel -- Level of the implication that binds it
-- See TcUnify Note [Deeper level on the left] for
-- how this level number is used
Bool -- True <=> this skolem type variable can be overlapped
-- when looking up instances
-- See Note [Binding when looking up instances] in InstEnv
......@@ -516,8 +519,10 @@ data TcTyVarDetails
vanillaSkolemTv, superSkolemTv :: TcTyVarDetails
-- See Note [Binding when looking up instances] in InstEnv
vanillaSkolemTv = SkolemTv (pushTcLevel topTcLevel) False -- Might be instantiated
superSkolemTv = SkolemTv (pushTcLevel topTcLevel) True -- Treat this as a completely distinct type
vanillaSkolemTv = SkolemTv topTcLevel False -- Might be instantiated
superSkolemTv = SkolemTv topTcLevel True -- Treat this as a completely distinct type
-- The choice of level number here is a bit dodgy, but
-- topTcLevel works in the places that vanillaSkolemTv is used
-----------------------------
data MetaDetails
......@@ -689,9 +694,13 @@ Note [TcLevel and untouchable type variables]
(ImplicInv) The level number (ic_tclvl) of an Implication is
STRICTLY GREATER THAN that of its parent
(GivenInv) The level number of a unification variable appearing
in the 'ic_given' of an implication I should be
STRICTLY LESS THAN the ic_tclvl of I
(SkolInv) The level number of the skolems (ic_skols) of an
Implication is equal to the level of the implication
itself (ic_tclvl)
(GivenInv) The level number of a unification variable appearing
in the 'ic_given' of an implication I should be
STRICTLY LESS THAN the ic_tclvl of I
(WantedInv) The level number of a unification variable appearing
in the 'ic_wanted' of an implication I should be
......@@ -699,7 +708,8 @@ Note [TcLevel and untouchable type variables]
See Note [WantedInv]
* A unification variable is *touchable* if its level number
is EQUAL TO that of its immediate parent implication.
is EQUAL TO that of its immediate parent implication,
and it is a TauTv or SigTv (but /not/ FlatMetaTv or FlatSkolTv
Note [WantedInv]
~~~~~~~~~~~~~~~~
......@@ -749,28 +759,21 @@ Note [TcLevel assignment]
~~~~~~~~~~~~~~~~~~~~~~~~~
We arrange the TcLevels like this
0 Level for all flatten meta-vars
1 Top level
2 First-level implication constraints
3 Second-level implication constraints
0 Top level
1 First-level implication constraints
2 Second-level implication constraints
...etc...
The flatten meta-vars are all at level 0, just to make them untouchable.
-}
maxTcLevel :: TcLevel -> TcLevel -> TcLevel
maxTcLevel (TcLevel a) (TcLevel b) = TcLevel (a `max` b)
fmvTcLevel :: TcLevel
-- See Note [TcLevel assignment]
fmvTcLevel = TcLevel 0
topTcLevel :: TcLevel
-- See Note [TcLevel assignment]
topTcLevel = TcLevel 1 -- 1 = outermost level
topTcLevel = TcLevel 0 -- 0 = outermost level
isTopTcLevel :: TcLevel -> Bool
isTopTcLevel (TcLevel 1) = True
isTopTcLevel (TcLevel 0) = True
isTopTcLevel _ = False
pushTcLevel :: TcLevel -> TcLevel
......@@ -1172,37 +1175,25 @@ tcIsTcTyVar :: TcTyVar -> Bool
-- See Note [TcTyVars in the typechecker]
tcIsTcTyVar tv = isTyVar tv
isTouchableOrFmv :: TcLevel -> TcTyVar -> Bool
isTouchableOrFmv ctxt_tclvl tv
= ASSERT2( tcIsTcTyVar tv, ppr tv )