import InstEnv ( DFunId, InstEnv, lookupInstEnv, checkFunDeps, extendInstEnv )
import TcIface ( loadImportedInsts )
import TcMType ( zonkTcType, zonkTcTypes, zonkTcPredType,
- zonkTcThetaType, tcInstTyVar, tcInstType, tcInstTyVars
+ zonkTcThetaType, tcInstTyVar, tcInstType
)
-import TcType ( Type, TcType, TcThetaType, TcTyVarSet, TcTyVar,
+import TcType ( Type, TcType, TcThetaType, TcTyVarSet, TcTyVar, TcPredType,
PredType(..), typeKind, mkSigmaTy,
tcSplitForAllTys, tcSplitForAllTys,
tcSplitPhiTy, tcIsTyVarTy, tcSplitDFunTy, tcSplitDFunHead,
tidyType, tidyTypes, tidyFreeTyVars, tcSplitSigmaTy,
pprPred, pprParendType, pprThetaArrow, pprTheta, pprClassPred
)
-import Type ( substTy, substTys, substTyWith, substTheta, zipTopTvSubst )
+import Type ( TvSubst, substTy, substTyVar, substTyWith, substTheta, zipTopTvSubst,
+ notElemTvSubst, extendTvSubstList )
import Unify ( tcMatchTys )
import Kind ( isSubKind )
import Packages ( isHomeModule )
import NameSet ( addOneToNameSet )
import Literal ( inIntRange )
import Var ( TyVar, tyVarKind, setIdType )
-import VarEnv ( TidyEnv, emptyTidyEnv, lookupVarEnv )
+import VarEnv ( TidyEnv, emptyTidyEnv )
import VarSet ( elemVarSet, emptyVarSet, unionVarSet, mkVarSet )
import TysWiredIn ( floatDataCon, doubleDataCon )
import PrelNames ( integerTyConName, fromIntegerName, fromRationalName, rationalTyConName )
; pkg_ie <- loadImportedInsts cls tys'
-- Check functional dependencies
- ; case checkFunDeps (pkg_ie, home_ie) dfun of
+ ; case checkFunDeps (pkg_ie, home_ie) dfun' of
Just dfuns -> funDepErr dfun dfuns
Nothing -> return ()
%************************************************************************
\begin{code}
-data LookupInstResult s
+data LookupInstResult
= NoInstance
| SimpleInst (LHsExpr TcId) -- Just a variable, type application, or literal
| GenInst [Inst] (LHsExpr TcId) -- The expression and its needed insts
-lookupInst :: Inst -> TcM (LookupInstResult s)
+lookupInst :: Inst -> TcM LookupInstResult
-- It's important that lookupInst does not put any new stuff into
-- the LIE. Instead, any Insts needed by the lookup are returned in
-- the LookupInstResult, where they can be further processed by tcSimplify
lookupInst (Dict _ _ _) = returnM NoInstance
-----------------
+instantiate_dfun :: TvSubst -> DFunId -> TcPredType -> InstLoc -> TcM LookupInstResult
instantiate_dfun tenv dfun_id pred loc
= -- tenv is a substitution that instantiates the dfun_id
-- to match the requested result type. However, the dfun
-- Record that this dfun is needed
record_dfun_usage dfun_id `thenM_`
+ getStage `thenM` \ use_stage ->
+ checkWellStaged (ptext SLIT("instance for") <+> quotes (ppr pred))
+ (topIdLvl dfun_id) use_stage `thenM_`
+
-- It's possible that not all the tyvars are in
-- the substitution, tenv. For example:
-- instance C X a => D X where ...
-- (presumably there's a functional dependency in class C)
- -- Hence the mk_ty_arg to instantiate any un-substituted tyvars.
- getStage `thenM` \ use_stage ->
- checkWellStaged (ptext SLIT("instance for") <+> quotes (ppr pred))
- (topIdLvl dfun_id) use_stage `thenM_`
+ -- Hence the open_tvs to instantiate any un-substituted tyvars.
let
(tyvars, rho) = tcSplitForAllTys (idType dfun_id)
- mk_ty_arg tv = case lookupVarEnv tenv tv of
- Just ty -> returnM ty
- Nothing -> tcInstTyVar tv `thenM` \ tc_tv ->
- returnM (mkTyVarTy tc_tv)
+ open_tvs = filter (`notElemTvSubst` tenv) tyvars
in
- mappM mk_ty_arg tyvars `thenM` \ ty_args ->
+ mappM tcInstTyVar open_tvs `thenM` \ open_tvs' ->
let
- dfun_rho = substTy (zipTopTvSubst tyvars ty_args) rho
- -- Since the tyvars are freshly made,
- -- they cannot possibly be captured by
- -- any existing for-alls. Hence zipTopTyVarSubst
+ tenv' = extendTvSubstList tenv open_tvs (mkTyVarTys open_tvs')
+ -- Since the tyvars are freshly made, they cannot possibly be captured by
+ -- any nested for-alls in rho. So the in-scope set is unchanged
+ dfun_rho = substTy tenv' rho
(theta, _) = tcSplitPhiTy dfun_rho
- ty_app = mkHsTyApp (L (instLocSrcSpan loc) (HsVar dfun_id)) ty_args
+ ty_app = mkHsTyApp (L (instLocSrcSpan loc) (HsVar dfun_id))
+ (map (substTyVar tenv') tyvars)
in
if null theta then
returnM (SimpleInst ty_app)
import TcEnv ( TcId, tcLookupLocalIds, tcLookupId, tcExtendIdEnv,
tcExtendTyVarEnv )
import TcPat ( PatCtxt(..), tcPats )
-import TcMType ( newTyFlexiVarTy, newTyFlexiVarTys, zonkTcType, isRigidType )
+import TcMType ( newTyFlexiVarTy, newTyFlexiVarTys, zonkTcType )
import TcType ( TcType, TcTyVar, TcSigmaType, TcRhoType, mkFunTys,
tyVarsOfTypes, tidyOpenTypes, isSigmaTy, mkTyConApp,
liftedTypeKind, openTypeKind, mkArrowKind, mkAppTy )
-- signatures
tcMatchPats pats tys body_ty thing_inside
- = do { do_refinement <- can_refine body_ty
- ; (pats', ex_tvs, res) <- tcPats (LamPat do_refinement) pats tys thing_inside
+ = do { (pats', ex_tvs, res) <- tcPats LamPat pats tys thing_inside
; tcCheckExistentialPat pats' ex_tvs tys body_ty
; returnM (pats', res) }
where
- -- Do GADT refinement if we are doing checking (not inference)
- -- and the body_ty is completely rigid
- -- ToDo: explain why
- can_refine (Infer _) = return False
- can_refine (Check ty) = isRigidType ty
tcCheckExistentialPat :: [LPat TcId] -- Patterns (just for error message)
-> [TcTyVar] -- Existentially quantified tyvars bound by pattern
tcLookupClass, tcLookupDataCon, tcLookupId )
import TcMType ( newTyFlexiVarTy, arityErr, tcSkolTyVars, readMetaTyVar )
import TcType ( TcType, TcTyVar, TcSigmaType, TcTauType, zipTopTvSubst,
- SkolemInfo(PatSkol), isSkolemTyVar, pprSkolemTyVar,
+ SkolemInfo(PatSkol), isSkolemTyVar, isMetaTyVar, pprSkolemTyVar,
TvSubst, mkTvSubst, substTyVar, substTy, MetaDetails(..),
mkTyVarTys, mkClassPred, mkTyConApp, isOverloadedTy )
import VarEnv ( mkVarEnv ) -- ugly
zapExpectedTo, zapToListTy, zapToTyConApp )
import TcHsType ( UserTypeCtxt(..), TcSigInfo( sig_tau ), TcSigFun, tcHsPatSigType )
import TysWiredIn ( stringTy, parrTyCon, tupleTyCon )
-import Unify ( MaybeErr(..), gadtRefineTys, gadtMatchTys )
+import Unify ( MaybeErr(..), gadtRefineTys, BindFlag(..) )
import Type ( substTys, substTheta )
import CmdLineOpts ( opt_IrrefutableTuples )
import TyCon ( TyCon )
%************************************************************************
\begin{code}
-data PatCtxt = LamPat Bool -- Used for lambda, case, do-notation etc
+data PatCtxt = LamPat -- Used for lambda, case, do-notation etc
| LetPat TcSigFun -- Used for let(rec) bindings
- -- True <=> we are checking the case expression,
- -- so can do full-blown refinement
- -- False <=> inferring, do no refinement
-------------------
tcPatBndr :: PatCtxt -> Name -> Expected TcSigmaType -> TcM TcId
-tcPatBndr (LamPat _) bndr_name pat_ty
+tcPatBndr LamPat bndr_name pat_ty
= do { pat_ty' <- zapExpectedType pat_ty argTypeKind
-- If pat_ty is Expected, this returns the appropriate
-- SigmaType. In Infer mode, we create a fresh type variable.
-> TcM a -> TcM a
refineAlt ctxt con ex_tvs ctxt_tys pat_tys thing_inside
= do { old_subst <- getTypeRefinement
- ; let refiner | can_i_refine ctxt = gadtRefineTys
- | otherwise = gadtMatchTys
- ; case refiner ex_tvs old_subst pat_tys ctxt_tys of
+ ; case gadtRefineTys bind_fn old_subst pat_tys ctxt_tys of
Failed msg -> failWithTc (inaccessibleAlt msg)
Succeeded new_subst -> do {
traceTc (text "refineTypes:match" <+> ppr con <+> ppr new_subst)
; setTypeRefinement new_subst thing_inside } }
where
- can_i_refine (LamPat can_refine) = can_refine
- can_i_refine other_ctxt = False
+ bind_fn tv | isMetaTyVar tv = WildCard -- Wobbly types behave as wild cards
+ | otherwise = BindMe
\end{code}
Note [Type matching]
import Name ( getSrcLoc )
import Var ( Id, TyVar )
import Class ( Class, FunDep, classTvsFds )
-import Unify ( tcUnifyTys, tcUnifyTysX )
-import Type ( mkTvSubst, substTy )
+import Unify ( tcUnifyTys, BindFlag(..) )
+import Type ( substTys, notElemTvSubst )
import TcType ( Type, ThetaType, PredType(..), tcEqType,
predTyUnique, mkClassPred, tyVarsOfTypes, tyVarsOfPred )
import VarSet
import VarEnv
import Outputable
import List ( tails )
-import Maybes ( maybeToBool )
+import Maybe ( isJust )
import ListSetOps ( equivClassesByUniq )
\end{code}
-- We can instantiate x to t1, and then we want to force
-- (Tree x) [t1/x] :=: t2
--
--- The same function is also used from InstEnv.badFunDeps, when we need
--- to *unify*; in which case the qtvs are the variables of both ls1 and ls2.
--- However unifying with the qtvs being the left-hand lot *is* just matching,
--- so we can call tcUnifyTys in both cases
- = case tcUnifyTys qtvs ls1 ls2 of
- Nothing -> []
- Just unif | maybeToBool (tcUnifyTysX qtvs unif rs1 rs2)
+-- This function is also used when matching two Insts (rather than an Inst
+-- against an instance decl. In that case, qtvs is empty, and we are doing
+-- an equality check
+--
+-- This function is also used by InstEnv.badFunDeps, which needs to *unify*
+-- For the one-sided matching case, the qtvs are just from the template,
+-- so we get matching
+--
+ = ASSERT2( length tys1 == length tys2 &&
+ length tys1 == length clas_tvs
+ , ppr tys1 <+> ppr tys2 )
+
+ case tcUnifyTys bind_fn ls1 ls2 of
+ Nothing -> []
+ Just subst | isJust (tcUnifyTys bind_fn rs1' rs2')
-- Don't include any equations that already hold.
-- Reason: then we know if any actual improvement has happened,
-- in which case we need to iterate the solver
-- In making this check we must taking account of the fact that any
-- qtvs that aren't already instantiated can be instantiated to anything
-- at all
- -- NB: qtvs, not qtvs' because matchTysX only tries to
- -- look template tyvars up in the substitution
-> []
| otherwise -- Aha! A useful equation
- -> [ (qtvs', map (substTy full_unif) rs1 `zip` map (substTy full_unif) rs2)]
- -- We could avoid this substTy stuff by producing the eqn
- -- (qtvs, ls1++rs1, ls2++rs2)
- -- which will re-do the ls1/ls2 unification when the equation is
- -- executed. What we're doing instead is recording the partial
- -- work of the ls1/ls2 unification leaving a smaller unification problem
+ -> [ (qtvs', zip rs1' rs2')]
+ -- We could avoid this substTy stuff by producing the eqn
+ -- (qtvs, ls1++rs1, ls2++rs2)
+ -- which will re-do the ls1/ls2 unification when the equation is
+ -- executed. What we're doing instead is recording the partial
+ -- work of the ls1/ls2 unification leaving a smaller unification problem
where
- full_unif = mkTvSubst unif
-
- qtvs' = filterVarSet (\v -> not (v `elemVarEnv` unif)) qtvs
+ rs1' = substTys subst rs1
+ rs2' = substTys subst rs2
+ qtvs' = filterVarSet (`notElemTvSubst` subst) qtvs
-- qtvs' are the quantified type variables
-- that have not been substituted out
--
-- we generate the equation
-- ({y}, [y], z)
where
+ bind_fn tv | tv `elemVarSet` qtvs = BindMe
+ | otherwise = Skolem
+
(ls1, rs1) = instFD fd clas_tvs tys1
(ls2, rs2) = instFD fd clas_tvs tys2
import Class ( Class, classTvsFds )
import Var ( Id )
import VarSet
-import Type ( TvSubstEnv )
+import Type ( TvSubst )
import TcType ( Type, tcTyConAppTyCon, tcIsTyVarTy,
tcSplitDFunTy, tyVarsOfTypes, isExistentialTyVar
)
-import Unify ( tcMatchTys, tcUnifyTys )
+import Unify ( tcMatchTys, tcUnifyTys, BindFlag(..) )
import FunDeps ( checkClsFD )
import TyCon ( TyCon )
import Outputable
%* *
%************************************************************************
+A @ClsInstEnv@ all the instances of that class. The @Id@ inside a
+ClsInstEnv mapping is the dfun for that instance.
+
+If class C maps to a list containing the item ([a,b], [t1,t2,t3], dfun), then
+
+ forall a b, C t1 t2 t3 can be constructed by dfun
+
+or, to put it another way, we have
+
+ instance (...) => C t1 t2 t3, witnessed by dfun
+
\begin{code}
type DFunId = Id
type InstEnv = UniqFM ClsInstEnv -- Maps Class to instances for that class
-- NB: use tcIsTyVarTy: don't look through newtypes!!
type InstEnvElt = (TyVarSet, [Type], DFunId)
- -- INVARIANTs: see notes below
+
+-- INVARIANTS:
+-- * [a,b] must be a superset of the free vars of [t1,t2,t3]
+--
+-- * The dfun must itself be quantified over [a,b]
+--
+-- * The template type variables [a,b] are distinct in each item
+-- of a ClsInstEnv (so we can safely unify them)
+
+-- Thus, the @ClassInstEnv@ for @Eq@ might contain the following entry:
+-- [a] ===> dfun_Eq_List :: forall a. Eq a => Eq [a]
+-- The "a" in the pattern must be one of the forall'd variables in
+-- the dfun type.
+
emptyInstEnv :: InstEnv
emptyInstEnv = emptyUFM
%* *
%************************************************************************
-A @ClsInstEnv@ all the instances of that class. The @Id@ inside a
-ClsInstEnv mapping is the dfun for that instance.
-
-If class C maps to a list containing the item ([a,b], [t1,t2,t3], dfun), then
-
- forall a b, C t1 t2 t3 can be constructed by dfun
-
-or, to put it another way, we have
-
- instance (...) => C t1 t2 t3, witnessed by dfun
-
-There is an important consistency constraint in the elements of a ClsInstEnv:
-
- * [a,b] must be a superset of the free vars of [t1,t2,t3]
-
- * The dfun must itself be quantified over [a,b]
-
- * More specific instances come before less specific ones,
- where they overlap
-
-Thus, the @ClassInstEnv@ for @Eq@ might contain the following entry:
- [a] ===> dfun_Eq_List :: forall a. Eq a => Eq [a]
-The "a" in the pattern must be one of the forall'd variables in
-the dfun type.
-
-
Notes on overlapping instances
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
lookupInstEnv :: DynFlags
-> (InstEnv -- External package inst-env
,InstEnv) -- Home-package inst-env
- -> Class -> [Type] -- What we are looking for
- -> ([(TvSubstEnv, InstEnvElt)], -- Successful matches
- [Id]) -- These don't match but do unify
+ -> Class -> [Type] -- What we are looking for
+ -> ([(TvSubst, InstEnvElt)], -- Successful matches
+ [Id]) -- These don't match but do unify
-- The second component of the tuple happens when we look up
-- Foo [a]
-- in an InstEnv that has entries for
pruned_matches | overlap_ok = foldr insert_overlapping [] all_matches
| otherwise = all_matches
-lookup_inst_env :: InstEnv -- The envt
- -> Class -> [Type] -- What we are looking for
- -> Bool -- All the [Type] are tyvars
- -> ([(TvSubstEnv, InstEnvElt)], -- Successful matches
- [Id]) -- These don't match but do unify
+lookup_inst_env :: InstEnv -- The envt
+ -> Class -> [Type] -- What we are looking for
+ -> Bool -- All the [Type] are tyvars
+ -> ([(TvSubst, InstEnvElt)], -- Successful matches
+ [Id]) -- These don't match but do unify
lookup_inst_env env key_cls key_tys key_all_tvs
= case lookupUFM env key_cls of
Nothing -> ([],[]) -- No instances for this class
-- the ClsIE has no instances of that form, so don't bother to search
| otherwise -> find insts [] []
where
- key_vars = filterVarSet not_existential (tyVarsOfTypes key_tys)
- not_existential tv = not (isExistentialTyVar tv)
+ find [] ms us = (ms, us)
+ find (item@(tpl_tyvars, tpl, dfun_id) : rest) ms us
+ = case tcMatchTys tpl_tyvars tpl key_tys of
+ Just subst -> find rest ((subst,item):ms) us
+ Nothing
+ -- Does not match, so next check whether the things unify
+ -- [see notes about overlapping instances above]
+ -> case tcUnifyTys bind_fn tpl key_tys of
+ Just _ -> find rest ms (dfun_id:us)
+ Nothing -> find rest ms us
+
+ bind_fn tv | isExistentialTyVar tv = Skolem
+ | otherwise = BindMe
-- The key_tys can contain skolem constants, and we can guarantee that those
-- are never going to be instantiated to anything, so we should not involve
-- them in the unification test. Example:
-- g x = op x
-- on the grounds that the correct instance depends on the instantiation of 'a'
- find [] ms us = (ms, us)
- find (item@(tpl_tyvars, tpl, dfun_id) : rest) ms us
- = case tcMatchTys tpl_tyvars tpl key_tys of
- Just subst -> find rest ((subst,item):ms) us
- Nothing
- -- Does not match, so next check whether the things unify
- -- [see notes about overlapping instances above]
- -> ASSERT2( not (key_vars `intersectsVarSet` tpl_tyvars),
- (ppr key_cls <+> ppr key_tys <+> ppr key_all_tvs) $$
- (ppr dfun_id <+> ppr tpl_tyvars <+> ppr tpl)
- )
- -- Unification will break badly if the variables overlap
- -- They shouldn't because we allocate separate uniques for them
- case tcUnifyTys (key_vars `unionVarSet` tpl_tyvars) key_tys tpl of
- Just _ -> find rest ms (dfun_id:us)
- Nothing -> find rest ms us
-
-insert_overlapping :: (TvSubstEnv, InstEnvElt) -> [(TvSubstEnv, InstEnvElt)]
- -> [(TvSubstEnv, InstEnvElt)]
+insert_overlapping :: (TvSubst, InstEnvElt) -> [(TvSubst, InstEnvElt)]
+ -> [(TvSubst, InstEnvElt)]
-- Add a new solution, knocking out strictly less specific ones
insert_overlapping new_item [] = [new_item]
insert_overlapping new_item (item:items)
seqType, seqTypes,
-- Type substitutions
- TvSubst(..), -- Representation visible to a few friends
- TvSubstEnv, emptyTvSubst,
- mkTvSubst, zipTvSubst, zipTopTvSubst, mkTopTvSubst,
+ TvSubstEnv, emptyTvSubstEnv, -- Representation widely visible
+ TvSubst(..), emptyTvSubst, -- Representation visible to a few friends
+ mkTvSubst, zipTvSubst, zipTopTvSubst, mkTopTvSubst, notElemTvSubst,
getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope,
extendTvSubst, extendTvSubstList, isInScope, composeTvSubst,
-- in the middle of matching, and unification (see Types.Unify)
-- So you have to look at the context to know if it's idempotent or
-- apply-once or whatever
+emptyTvSubstEnv :: TvSubstEnv
+emptyTvSubstEnv = emptyVarEnv
composeTvSubst :: InScopeSet -> TvSubstEnv -> TvSubstEnv -> TvSubstEnv
-- (compose env1 env2)(x) is env1(env2(x)); i.e. apply env2 then env1
isInScope :: Var -> TvSubst -> Bool
isInScope v (TvSubst in_scope _) = v `elemInScopeSet` in_scope
+notElemTvSubst :: TyVar -> TvSubst -> Bool
+notElemTvSubst tv (TvSubst _ env) = not (tv `elemVarEnv` env)
+
setTvSubstEnv :: TvSubst -> TvSubstEnv -> TvSubst
setTvSubstEnv (TvSubst in_scope _) env = TvSubst in_scope env
-- Matching and unification
tcMatchTys, tcMatchTyX, tcMatchPreds, MatchEnv(..),
- tcUnifyTys, tcUnifyTysX,
+ tcUnifyTys,
- gadtRefineTys, gadtMatchTys, coreRefineTys,
+ gadtRefineTys, BindFlag(..),
+
+ coreRefineTys,
-- Re-export
MaybeErr(..)
import VarSet
import Kind ( isSubKind )
import Type ( typeKind, tyVarsOfType, tyVarsOfTypes, tyVarsOfTheta,
- TvSubstEnv, TvSubst(..), substTy, tcEqTypeX )
+ TvSubstEnv, emptyTvSubstEnv, TvSubst(..), substTy, tcEqTypeX )
import TypeRep ( Type(..), PredType(..), funTyCon )
import Util ( snocView )
import ErrUtils ( Message )
tcMatchTys :: TyVarSet -- Template tyvars
-> [Type] -- Template
-> [Type] -- Target
- -> Maybe TvSubstEnv -- One-shot; in principle the template
+ -> Maybe TvSubst -- One-shot; in principle the template
-- variables could be free in the target
tcMatchTys tmpls tys1 tys2
- = match_tys (ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope_tyvars})
- emptyTvSubstEnv
- tys1 tys2
+ = case match_tys menv emptyTvSubstEnv tys1 tys2 of
+ Just subst_env -> Just (TvSubst in_scope subst_env)
+ Nothing -> Nothing
where
- in_scope_tyvars = mkInScopeSet (tmpls `unionVarSet` tyVarsOfTypes tys2)
+ menv = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
+ in_scope = mkInScopeSet (tmpls `unionVarSet` tyVarsOfTypes tys2)
-- We're assuming that all the interesting
-- tyvars in tys1 are in tmpls
menv = ME { me_tmpls = mkVarSet tmpls, me_env = mkRnEnv2 in_scope_tyvars }
in_scope_tyvars = mkInScopeSet (tyVarsOfTheta ps1 `unionVarSet` tyVarsOfTheta ps2)
+-- This one is called from the expression matcher, which already has a MatchEnv in hand
tcMatchTyX :: MatchEnv
-> TvSubstEnv -- Substitution to extend
-> Type -- Template
%************************************************************************
%* *
- The workhorse
+ Unification
%* *
%************************************************************************
\begin{code}
-gadtRefineTys, gadtMatchTys
- :: [TyVar] -- Try to unify these
- -> TvSubstEnv -- Not idempotent
- -> [Type] -> [Type]
- -> MaybeErr Message TvSubstEnv -- Not idempotent
--- This one is used by the type checker. Neither the input nor result
--- substitition is idempotent
-gadtRefineTys ex_tvs subst tys1 tys2
- = initUM (tryToBind (mkVarSet ex_tvs)) (unify_tys subst tys1 tys2)
+tcUnifyTys :: (TyVar -> BindFlag)
+ -> [Type] -> [Type]
+ -> Maybe TvSubst -- A regular one-shot substitution
+-- The two types may have common type variables, and indeed do so in the
+-- second call to tcUnifyTys in FunDeps.checkClsFD
+tcUnifyTys bind_fn tys1 tys2
+ = maybeErrToMaybe $ initUM bind_fn $
+ do { subst_env <- unify_tys emptyTvSubstEnv tys1 tys2
-gadtMatchTys ex_tvs subst tys1 tys2
- = initUM (bindOnly (mkVarSet ex_tvs)) (unify_tys subst tys1 tys2)
+ -- Find the fixed point of the resulting non-idempotent substitution
+ ; let in_scope = mkInScopeSet (tvs1 `unionVarSet` tvs2)
+ subst = TvSubst in_scope subst_env_fixpt
+ subst_env_fixpt = mapVarEnv (substTy subst) subst_env
+ ; return subst }
+ where
+ tvs1 = tyVarsOfTypes tys1
+ tvs2 = tyVarsOfTypes tys2
----------------------------
coreRefineTys :: InScopeSet -- Superset of free vars of either type
; return subst_env_fixpt }
----------------------------
-tcUnifyTys :: TyVarSet -> [Type] -> [Type] -> Maybe TvSubstEnv
-tcUnifyTys bind_these tys1 tys2
- = maybeErrToMaybe $ initUM (bindOnly bind_these) $
- unify_tys emptyTvSubstEnv tys1 tys2
-
-tcUnifyTysX :: TyVarSet -> TvSubstEnv -> [Type] -> [Type] -> Maybe TvSubstEnv
-tcUnifyTysX bind_these subst tys1 tys2
- = maybeErrToMaybe $ initUM (bindOnly bind_these) $
- unify_tys subst tys1 tys2
+gadtRefineTys
+ :: (TyVar -> BindFlag) -- Try to unify these
+ -> TvSubstEnv -- Not idempotent
+ -> [Type] -> [Type]
+ -> MaybeErr Message TvSubstEnv -- Not idempotent
+-- This one is used by the type checker. Neither the input nor result
+-- substitition is idempotent
+gadtRefineTys bind_fn subst tys1 tys2
+ = initUM bind_fn (unify_tys subst tys1 tys2)
----------------------------
-tryToBind, bindOnly :: TyVarSet -> TyVar -> BindFlag
+tryToBind :: TyVarSet -> TyVar -> BindFlag
tryToBind tv_set tv | tv `elemVarSet` tv_set = BindMe
| otherwise = AvoidMe
-
-bindOnly tv_set tv | tv `elemVarSet` tv_set = BindMe
- | otherwise = DontBindMe
-
-emptyTvSubstEnv :: TvSubstEnv
-emptyTvSubstEnv = emptyVarEnv
\end{code}
-> UM TvSubstEnv
uVar swap subst tv1 ty
- = -- check to see whether tv1 is refined
+ = -- Check to see whether tv1 is refined by the substitution
case (lookupVarEnv subst tv1) of
- -- yes, call back into unify'
+ -- Yes, call back into unify'
Just ty' | swap -> unify subst ty ty'
| otherwise -> unify subst ty' ty
-- No, continue
= do { b1 <- tvBindFlag tv1
; b2 <- tvBindFlag tv2
; case (b1,b2) of
- (DontBindMe, DontBindMe) -> failWith (misMatch ty1 ty2)
- (DontBindMe, _) -> bindTv subst tv2 ty1
- (BindMe, _) -> bindTv subst tv1 ty2
- (AvoidMe, BindMe) -> bindTv subst tv2 ty1
- (AvoidMe, _) -> bindTv subst tv1 ty2
- }
+ (BindMe, _) -> bind tv1 ty2
- | k1 `isSubKind` k2 -- Must update tv2
- = do { b2 <- tvBindFlag tv2
- ; case b2 of
- DontBindMe -> failWith (misMatch ty1 ty2)
- other -> bindTv subst tv2 ty1
- }
+ (AvoidMe, BindMe) -> bind tv2 ty1
+ (AvoidMe, _) -> bind tv1 ty2
- | k2 `isSubKind` k1 -- Must update tv1
- = do { b1 <- tvBindFlag tv1
- ; case b1 of
- DontBindMe -> failWith (misMatch ty1 ty2)
- other -> bindTv subst tv1 ty2
+ (WildCard, WildCard) -> return subst
+ (WildCard, Skolem) -> return subst
+ (WildCard, _) -> bind tv2 ty1
+
+ (Skolem, WildCard) -> return subst
+ (Skolem, Skolem) -> failWith (misMatch ty1 ty2)
+ (Skolem, _) -> bind tv2 ty1
}
+ | k1 `isSubKind` k2 = bindTv subst tv2 ty1 -- Must update tv2
+ | k2 `isSubKind` k1 = bindTv subst tv1 ty2 -- Must update tv1
+
| otherwise = failWith (kindMisMatch tv1 ty2)
where
ty1 = TyVarTy tv1
k1 = tyVarKind tv1
k2 = tyVarKind tv2
+ bind tv ty = return (extendVarEnv subst tv ty)
uUnrefined subst tv1 ty2 -- ty2 is not a type variable
- -- Do occurs check...
| tv1 `elemVarSet` substTvSet subst (tyVarsOfType ty2)
- = failWith (occursCheck tv1 ty2)
- -- And a kind check...
- | k2 `isSubKind` k1
- = do { b1 <- tvBindFlag tv1
- ; case b1 of -- And check that tv1 is bindable
- DontBindMe -> failWith (misMatch ty1 ty2)
- other -> bindTv subst tv1 ty2
- }
+ = failWith (occursCheck tv1 ty2) -- Occurs check
+ | not (k2 `isSubKind` k1)
+ = failWith (kindMisMatch tv1 ty2) -- Kind check
| otherwise
- = pprTrace "kind" (ppr tv1 <+> ppr k1 $$ ppr ty2 <+> ppr k2) $
- failWith (kindMisMatch tv1 ty2)
+ = bindTv subst tv1 ty2
where
- ty1 = TyVarTy tv1
k1 = tyVarKind tv1
k2 = typeKind ty2
Nothing -> unitVarSet tv
Just ty -> substTvSet subst (tyVarsOfType ty)
-bindTv subst tv ty = return (extendVarEnv subst tv ty)
+bindTv subst tv ty -- ty is not a type variable
+ = do { b <- tvBindFlag tv
+ ; case b of
+ Skolem -> failWith (misMatch (TyVarTy tv) ty)
+ WildCard -> return subst
+ other -> return (extendVarEnv subst tv ty)
+ }
\end{code}
%************************************************************************
%************************************************************************
\begin{code}
-data BindFlag = BindMe | AvoidMe | DontBindMe
+data BindFlag
+ = BindMe -- A regular type variable
+ | AvoidMe -- Like BindMe but, given the choice, avoid binding it
+
+ | Skolem -- This type variable is a skolem constant
+ -- Don't bind it; it only matches itself
+
+ | WildCard -- This type variable matches anything,
+ -- and does not affect the substitution
newtype UM a = UM { unUM :: (TyVar -> BindFlag)
-> MaybeErr Message a }
projects / ghc-hetmet.git / commitdiff