import qualified Type ( substTy )
import Type ( Type, tyVarsOfType, mkTyVarTy,
- TvSubstEnv, TvSubst(..), substTyVar )
+ TvSubstEnv, TvSubst(..), substTyVarBndr )
import VarSet
import VarEnv
import Var ( setVarUnique, isId, mustHaveLocalBinding )
-- Extend the substitution if the unique has changed,
-- or there's some useful occurrence information
- -- See the notes with substTyVar for the delSubstEnv
+ -- See the notes with substTyVarBndr for the delSubstEnv
occ_info = occInfo old_info
new_env | new_id /= old_id || isFragileOcc occ_info
= extendVarEnv env old_id (DoneId new_id occ_info)
\begin{code}
subst_tv :: Subst -> TyVar -> (Subst, TyVar)
--- Unpackage and re-package for substTyVar
+-- Unpackage and re-package for substTyVarBndr
subst_tv (Subst in_scope id_env tv_env) tv
- = case substTyVar (TvSubst in_scope tv_env) tv of
+ = case substTyVarBndr (TvSubst in_scope tv_env) tv of
(TvSubst in_scope' tv_env', tv')
-> (Subst in_scope' id_env tv_env', tv')
new_id = maybeModifyIdInfo (substIdInfo keep_fragile rec_subst) id2
-- Extend the substitution if the unique has changed
- -- See the notes with substTyVar for the delSubstEnv
+ -- See the notes with substTyVarBndr for the delSubstEnv
new_env | new_id /= old_id
= extendVarEnv env old_id (DoneId new_id (idOccInfo old_id))
| otherwise
import VarSet
import VarEnv
import TcType ( TvSubstEnv )
-import Unify ( matchTyX, MatchEnv(..) )
+import Unify ( tcMatchTyX, MatchEnv(..) )
import BasicTypes ( Activation, CompilerPhase, isActive )
import Outputable
\begin{code}
------------------------------------------
match_ty menv (tv_subst, id_subst) ty1 ty2
- = do { tv_subst' <- Unify.matchTyX menv tv_subst ty1 ty2
+ = do { tv_subst' <- Unify.tcMatchTyX menv tv_subst ty1 ty2
; return (tv_subst', id_subst) }
\end{code}
pprPred, pprParendType, pprThetaArrow, pprTheta, pprClassPred
)
import Type ( substTy, substTys, substTyWith, substTheta, zipTopTvSubst )
-import Unify ( matchTys )
+import Unify ( tcMatchTys )
import Kind ( isSubKind )
import Packages ( isHomeModule )
import HscTypes ( ExternalPackageState(..) )
; let { tys' = substTys tenv tys
; (matches, _) = lookupInstEnv dflags (pkg_ie, home_ie) cls tys'
; dup_dfuns = [dup_dfun | (_, (_, dup_tys, dup_dfun)) <- matches,
- isJust (matchTys (mkVarSet tvs) tys' dup_tys)] }
+ isJust (tcMatchTys (mkVarSet tvs) tys' dup_tys)] }
-- Find memebers of the match list which
-- dfun itself matches. If the match is 2-way, it's a duplicate
; case dup_dfuns of
-- Local environment
tcExtendKindEnv,
- tcExtendTyVarEnv, tcExtendTyVarEnv2,
+ tcExtendTyVarEnv, tcExtendTyVarEnv2, tcExtendTyVarEnv3,
tcExtendIdEnv, tcExtendIdEnv1, tcExtendIdEnv2,
tcLookup, tcLookupLocated, tcLookupLocalIds,
tcLookupId, tcLookupTyVar,
import TcIface ( tcImportDecl )
import TcRnMonad
import TcMType ( zonkTcType, zonkTcTyVar, zonkTcTyVarsAndFV )
-import TcType ( Type, TcKind, TcTyVar, TcTyVarSet,
+import TcType ( Type, TcKind, TcTyVar, TcTyVarSet, TcType,
tyVarsOfType, tyVarsOfTypes, tcSplitDFunTy, mkGenTyConApp,
- getDFunTyKey, tcTyConAppTyCon,
+ getDFunTyKey, tcTyConAppTyCon, tcGetTyVar, mkTyVarTy,
tidyOpenType, tidyOpenTyVar, pprTyThingCategory
)
import qualified Type ( getTyVar_maybe )
Nothing -> tcLookupGlobal name `thenM` \ thing ->
returnM (AGlobal thing)
-tcLookupTyVar :: Name -> TcM Id
+tcLookupTyVar :: Name -> TcM TcTyVar
tcLookupTyVar name
= tcLookup name `thenM` \ thing ->
case thing of
- ATyVar tv -> returnM tv
- other -> pprPanic "tcLookupTyVar" (ppr name)
+ ATyVar _ ty -> returnM (tcGetTyVar "tcLookupTyVar" ty)
+ other -> pprPanic "tcLookupTyVar" (ppr name)
tcLookupId :: Name -> TcM Id
-- Used when we aren't interested in the binding level
tcExtendTyVarEnv :: [TyVar] -> TcM r -> TcM r
tcExtendTyVarEnv tvs thing_inside
- = tc_extend_tv_env [(getName tv, ATyVar tv) | tv <- tvs] tvs thing_inside
+ = tc_extend_tv_env [ATyVar tv (mkTyVarTy tv) | tv <- tvs] thing_inside
tcExtendTyVarEnv2 :: [(TyVar,TcTyVar)] -> TcM r -> TcM r
tcExtendTyVarEnv2 tv_pairs thing_inside
- = tc_extend_tv_env [(getName tv1, ATyVar tv2) | (tv1,tv2) <- tv_pairs]
- [tv | (_,tv) <- tv_pairs]
- thing_inside
+ = tc_extend_tv_env [ATyVar tv1 (mkTyVarTy tv2) | (tv1,tv2) <- tv_pairs] thing_inside
-tc_extend_tv_env binds tyvars thing_inside
+tcExtendTyVarEnv3 :: [(TyVar,TcType)] -> TcM r -> TcM r
+tcExtendTyVarEnv3 ty_pairs thing_inside
+ = tc_extend_tv_env [ATyVar tv1 ty2 | (tv1,ty2) <- ty_pairs] thing_inside
+
+tc_extend_tv_env binds thing_inside
= getLclEnv `thenM` \ env@(TcLclEnv {tcl_env = le,
tcl_tyvars = gtvs,
tcl_rdr = rdr_env}) ->
let
- le' = extendNameEnvList le binds
- rdr_env' = extendLocalRdrEnv rdr_env (map fst binds)
- new_tv_set = mkVarSet tyvars
+ names = [getName tv | ATyVar tv _ <- binds]
+ rdr_env' = extendLocalRdrEnv rdr_env names
+ le' = extendNameEnvList le (names `zip` binds)
+ new_tv_set = tyVarsOfTypes [ty | ATyVar _ ty <- binds]
in
-- It's important to add the in-scope tyvars to the global tyvar set
-- as well. Consider
in
returnM (tidy_env', Just msg)
-find_thing ignore_it tidy_env (ATyVar tv)
- = zonkTcTyVar tv `thenM` \ tv_ty ->
+find_thing ignore_it tidy_env (ATyVar tv ty)
+ = zonkTcType ty `thenM` \ tv_ty ->
if ignore_it tv_ty then
returnM (tidy_env, Nothing)
else let
ptext SLIT("used as a") <+> text expected)
where
pp_thing (AGlobal thing) = pprTyThingCategory thing
- pp_thing (ATyVar _) = ptext SLIT("Type variable")
+ pp_thing (ATyVar _ _) = ptext SLIT("Type variable")
pp_thing (ATcId _ _ _) = ptext SLIT("Local identifier")
\end{code}
import TcArrows ( tcProc )
import TcMatches ( tcMatchesCase, tcMatchLambda, tcDoStmts, tcThingWithSig, TcMatchCtxt(..) )
import TcHsType ( tcHsSigType, UserTypeCtxt(..) )
-import TcPat ( badFieldCon )
-import TcMType ( tcInstTyVars, tcInstType, newTyFlexiVarTy, zonkTcType, readMetaTyVar )
+import TcPat ( badFieldCon, refineTyVars )
+import TcMType ( tcInstTyVars, tcInstType, newTyFlexiVarTy, zonkTcType )
import TcType ( Type, TcTyVar, TcType, TcSigmaType, TcRhoType, MetaDetails(..),
tcSplitFunTys, tcSplitTyConApp, mkTyVarTys,
isSigmaTy, mkFunTy, mkTyConApp, tyVarsOfTypes, isLinearPred,
Infer _ -> do -- Type check args first, then
-- refine result type, then do tcResult
{ the_app' <- tcArgs fun fun' args expected_arg_tys
- ; actual_res_ty' <- refineResultTy fun_tvs actual_res_ty
+ ; subst <- refineTyVars fun_tvs
+ ; let actual_res_ty' = substTy subst actual_res_ty
; co_fn <- tcResult fun args res_ty actual_res_ty'
; traceTc (text "tcApp: infer" <+> vcat [ppr fun <+> ppr args, ppr the_app',
ppr actual_res_ty, ppr actual_res_ty'])
| otherwise = appCtxt fun args
in
returnM (env2, message)
-
-----------------
-refineResultTy :: [TcTyVar] -- Newly instantiated meta-tyvars of the function
- -> TcType -- Result type, instantiated with those tyvars
- -> TcM TcType -- Refined result type
--- De-wobblify the result type, by taking account what we learned
--- from type-checking the arguments. Just one level of de-wobblification
--- though. What a hack!
-refineResultTy tvs res_ty
- = do { mb_prs <- mapM mk_pr tvs
- ; let subst = mkTopTvSubst (catMaybes mb_prs)
- ; return (substTy subst res_ty) }
- where
- mk_pr tv = do { details <- readMetaTyVar tv
- ; case details of
- Indirect ty -> return (Just (tv,ty))
- other -> return Nothing
- }
\end{code}
tcLookup name `thenM` \ thing ->
traceTc (text "lk2" <+> ppr name <+> ppr thing) `thenM_`
case thing of
- ATyVar tv -> returnM (tyVarKind tv)
+ ATyVar tv _ -> returnM (tyVarKind tv)
AThing kind -> returnM kind
AGlobal (ATyCon tc) -> returnM (tyConKind tc)
other -> wrongThingErr "type" thing name
ds_var_app name arg_tys
= tcLookup name `thenM` \ thing ->
case thing of
- ATyVar tv -> returnM (mkAppTys (mkTyVarTy tv) arg_tys)
+ ATyVar _ ty -> returnM (mkAppTys ty arg_tys)
AGlobal (ATyCon tc) -> returnM (mkGenTyConApp tc arg_tys)
-- AThing _ -> tcLookupTyCon name `thenM` \ tc ->
-- returnM (mkGenTyConApp tc arg_tys)
\section[TcPat]{Typechecking patterns}
\begin{code}
-module TcPat ( tcPat, tcPats, PatCtxt(..), badFieldCon, polyPatSig ) where
+module TcPat ( tcPat, tcPats, PatCtxt(..), badFieldCon, polyPatSig, refineTyVars ) where
#include "HsVersions.h"
import Id ( Id, idType, mkLocalId )
import Name ( Name )
import TcSimplify ( tcSimplifyCheck, bindInstsOfLocalFuns )
-import TcEnv ( newLocalName, tcExtendIdEnv1, tcExtendTyVarEnv,
+import TcEnv ( newLocalName, tcExtendIdEnv1, tcExtendTyVarEnv3,
tcLookupClass, tcLookupDataCon, tcLookupId )
-import TcMType ( newTyFlexiVarTy, arityErr, tcSkolTyVars )
+import TcMType ( newTyFlexiVarTy, arityErr, tcSkolTyVars, readMetaTyVar )
import TcType ( TcType, TcTyVar, TcSigmaType, TcTauType, zipTopTvSubst,
SkolemInfo(PatSkol), isSkolemTyVar, pprSkolemTyVar,
+ TvSubst, mkTvSubst, substTyVar, substTy, MetaDetails(..),
mkTyVarTys, mkClassPred, mkTyConApp, isOverloadedTy )
+import VarEnv ( mkVarEnv ) -- ugly
import Kind ( argTypeKind, liftedTypeKind )
import TcUnify ( tcSubPat, Expected(..), zapExpectedType,
zapExpectedTo, zapToListTy, zapToTyConApp )
import TcHsType ( UserTypeCtxt(..), TcSigInfo( sig_tau ), TcSigFun, tcHsPatSigType )
import TysWiredIn ( stringTy, parrTyCon, tupleTyCon )
-import Unify ( MaybeErr(..), tcRefineTys, tcMatchTys )
+import Unify ( MaybeErr(..), gadtRefineTys, gadtMatchTys )
import Type ( substTys, substTheta )
import CmdLineOpts ( opt_IrrefutableTuples )
import TyCon ( TyCon )
integralClassName )
import BasicTypes ( isBoxed )
import SrcLoc ( Located(..), SrcSpan, noLoc, unLoc, getLoc )
+import Maybes ( catMaybes )
import ErrUtils ( Message )
import Outputable
import FastString
= do { -- See Note [Pattern coercions] below
(sig_tvs, sig_ty) <- tcHsPatSigType PatSigCtxt sig
; tcSubPat sig_ty pat_ty
- ; (pat', tvs, res) <- tcExtendTyVarEnv sig_tvs $
- tc_lpat ctxt pat (Check sig_ty) thing_inside
+ ; subst <- refineTyVars sig_tvs -- See note [Type matching]
+ ; let tv_binds = [(tv, substTyVar subst tv) | tv <- sig_tvs]
+ sig_ty' = substTy subst sig_ty
+ ; (pat', tvs, res)
+ <- tcExtendTyVarEnv3 tv_binds $
+ tc_lpat ctxt pat (Check sig_ty') thing_inside
+
; return (SigPatOut pat' sig_ty, tvs, res) }
tc_pat ctxt pat@(TypePat ty) pat_ty thing_inside
-> 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 = tcRefineTys
- | otherwise = tcMatchTys
+ ; let refiner | can_i_refine ctxt = gadtRefineTys
+ | otherwise = gadtMatchTys
; case refiner ex_tvs old_subst pat_tys ctxt_tys of
Failed msg -> failWithTc (inaccessibleAlt msg)
Succeeded new_subst -> do {
can_i_refine other_ctxt = False
\end{code}
+Note [Type matching]
+~~~~~~~~~~~~~~~~~~~~
+This little function @refineTyVars@ is a little tricky. Suppose we have a pattern type
+signature
+ f = \(x :: Term a) -> body
+Then 'a' should be bound to a wobbly type. But if we have
+ f :: Term b -> some-type
+ f = \(x :: Term a) -> body
+then 'a' should be bound to the rigid type 'b'. So we want to
+ * instantiate the type sig with fresh meta tyvars (e.g. \alpha)
+ * unify with the type coming from the context
+ * read out whatever information has been gleaned
+ from that unificaiton (e.g. unifying \alpha with 'b')
+ * and replace \alpha by 'b' in the type, when typechecking the
+ pattern inside the type sig (x in this case)
+It amounts to combining rigid info from the context and from the sig.
+
+Exactly the same thing happens for 'smart function application'.
+
+\begin{code}
+refineTyVars :: [TcTyVar] -- Newly instantiated meta-tyvars of the function
+ -> TcM TvSubst -- Substitution mapping any of the meta-tyvars that
+ -- has been unifies to what it was instantiated to
+-- Just one level of de-wobblification though. What a hack!
+refineTyVars tvs
+ = do { mb_prs <- mapM mk_pr tvs
+ ; return (mkTvSubst (mkVarEnv (catMaybes mb_prs))) }
+ where
+ mk_pr tv = do { details <- readMetaTyVar tv
+ ; case details of
+ Indirect ty -> return (Just (tv,ty))
+ other -> return Nothing
+ }
+\end{code}
+
%************************************************************************
%* *
Note [Pattern coercions]
GenAvailInfo(..), AvailInfo,
availName, IsBootInterface, Deprecations )
import Packages ( PackageId )
-import Type ( Type, TvSubstEnv )
+import Type ( Type, TvSubstEnv, pprParendType )
import TcType ( TcTyVarSet, TcType, TcTauType, TcThetaType, SkolemInfo,
TcPredType, TcKind, tcCmpPred, tcCmpType, tcCmpTypes )
import InstEnv ( DFunId, InstEnv )
data TcTyThing
= AGlobal TyThing -- Used only in the return type of a lookup
+
| ATcId TcId ThLevel ProcLevel -- Ids defined in this module; may not be fully zonked
- | ATyVar TyVar -- Type variables
+
+ | ATyVar TyVar TcType -- Type variables; tv -> type. It can't just be a TyVar
+ -- that is mutated to point to the type it is bound to,
+ -- because that would make it a wobbly type, and we
+ -- want pattern-bound lexically-scoped type variables to
+ -- be able to stand for rigid types
+
| AThing TcKind -- Used temporarily, during kind checking, for the
-- tycons and clases in this recursive group
instance Outputable TcTyThing where -- Debugging only
ppr (AGlobal g) = text "AGlobal" <+> ppr g
ppr (ATcId g tl pl) = text "ATcId" <+> ppr g <+> ppr tl <+> ppr pl
- ppr (ATyVar t) = text "ATyVar" <+> ppr t
+ ppr (ATyVar tv ty) = text "ATyVar" <+> ppr tv <+> pprParendType ty
ppr (AThing k) = text "AThing" <+> ppr k
\end{code}
; fix <- reifyFixity (idName id)
; return (TH.VarI (reifyName id) ty2 Nothing fix) }
-reifyThing (ATyVar tv)
- = do { ty1 <- zonkTcTyVar tv
+reifyThing (ATyVar tv ty)
+ = do { ty1 <- zonkTcType ty
; ty2 <- reifyType ty1
; return (TH.TyVarI (reifyName tv) ty2) }
mkTvSubst, zipTvSubst, zipTopTvSubst, mkTopTvSubst,
getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope,
extendTvSubst, extendTvSubstList, isInScope,
- substTy, substTys, substTyWith, substTheta, substTyVar,
+ substTy, substTys, substTyWith, substTheta, substTyVar, substTyVarBndr,
isUnLiftedType, -- Source types are always lifted
isUnboxedTupleType, -- Ditto
mkTvSubst, zipTvSubst, zipTopTvSubst, mkTopTvSubst,
getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope,
extendTvSubst, extendTvSubstList, isInScope,
- substTy, substTys, substTyWith, substTheta, substTyVar,
+ substTy, substTys, substTyWith, substTheta, substTyVar, substTyVarBndr,
typeKind, repType,
pprKind, pprParendKind,
-> TcM ()
-- In patterns we insist on an exact match; hence no CoFn returned
-- See Note [Pattern coercions] in TcPat
+-- However, we can't call unify directly, because both types might be
+-- polymorphic; hence the call to tcSub, followed by a check for
+-- the identity coercion
tcSubPat sig_ty (Infer hole)
= do { sig_ty' <- zonkTcType sig_ty
import Name ( getSrcLoc )
import Var ( Id, TyVar )
import Class ( Class, FunDep, classTvsFds )
-import Unify ( unifyTys, unifyTysX )
+import Unify ( tcUnifyTys, tcUnifyTysX )
import Type ( mkTvSubst, substTy )
import TcType ( Type, ThetaType, PredType(..), tcEqType,
predTyUnique, mkClassPred, tyVarsOfTypes, tyVarsOfPred )
-- 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 unifyTys in both cases
- = case unifyTys qtvs ls1 ls2 of
+-- so we can call tcUnifyTys in both cases
+ = case tcUnifyTys qtvs ls1 ls2 of
Nothing -> []
- Just unif | maybeToBool (unifyTysX qtvs unif rs1 rs2)
+ Just unif | maybeToBool (tcUnifyTysX qtvs unif 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
import TcType ( Type, tcTyConAppTyCon, tcIsTyVarTy,
tcSplitDFunTy, tyVarsOfTypes, isExistentialTyVar
)
-import Unify ( matchTys, unifyTys )
+import Unify ( tcMatchTys, tcUnifyTys )
import FunDeps ( checkClsFD )
import TyCon ( TyCon )
import Outputable
find [] ms us = (ms, us)
find (item@(tpl_tyvars, tpl, dfun_id) : rest) ms us
- = case matchTys tpl_tyvars tpl key_tys of
+ = 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
)
-- Unification will break badly if the variables overlap
-- They shouldn't because we allocate separate uniques for them
- case unifyTys (key_vars `unionVarSet` tpl_tyvars) key_tys tpl of
+ case tcUnifyTys (key_vars `unionVarSet` tpl_tyvars) key_tys tpl of
Just _ -> find rest ms (dfun_id:us)
Nothing -> find rest ms us
old_beats_new = item `beats` new_item
(_, (tvs1, tys1, _)) `beats` (_, (tvs2, tys2, _))
- = isJust (matchTys tvs2 tys2 tys1) -- A beats B if A is more specific than B
+ = isJust (tcMatchTys tvs2 tys2 tys1) -- A beats B if A is more specific than B
-- I.e. if B can be instantiated to match A
\end{code}
extendTvSubst, extendTvSubstList, isInScope,
-- Performing substitution on types
- substTy, substTys, substTyWith, substTheta, substTyVar,
+ substTy, substTys, substTyWith, substTheta, substTyVar, substTyVarBndr,
deShadowTy,
-- Pretty-printing
\begin{code}
data TvSubst
= TvSubst InScopeSet -- The in-scope type variables
- TvSubstEnv -- The substitution itself; guaranteed idempotent
+ TvSubstEnv -- The substitution itself
-- See Note [Apply Once]
{- ----------------------------------------------------------
-- Note that the in_scope set is poked only if we hit a forall
-- so it may often never be fully computed
-subst_ty subst@(TvSubst in_scope env) ty
+subst_ty subst ty
= go ty
where
- go ty@(TyVarTy tv) = case (lookupVarEnv env tv) of
- Nothing -> ty
- Just ty' -> ty' -- See Note [Apply Once]
-
+ go (TyVarTy tv) = substTyVar subst tv
go (TyConApp tc tys) = let args = map go tys
in args `seqList` TyConApp tc args
-- The mkAppTy smart constructor is important
-- we might be replacing (a Int), represented with App
-- by [Int], represented with TyConApp
- go (ForAllTy tv ty) = case substTyVar subst tv of
+ go (ForAllTy tv ty) = case substTyVarBndr subst tv of
(subst', tv') -> ForAllTy tv' $! (subst_ty subst' ty)
-substTyVar :: TvSubst -> TyVar -> (TvSubst, TyVar)
-substTyVar subst@(TvSubst in_scope env) old_var
+substTyVar :: TvSubst -> TyVar -> Type
+substTyVar (TvSubst in_scope env) tv
+ = case (lookupVarEnv env tv) of
+ Nothing -> TyVarTy tv
+ Just ty' -> ty' -- See Note [Apply Once]
+
+substTyVarBndr :: TvSubst -> TyVar -> (TvSubst, TyVar)
+substTyVarBndr subst@(TvSubst in_scope env) old_var
| old_var == new_var -- No need to clone
-- But we *must* zap any current substitution for the variable.
-- For example:
\begin{code}
module Unify (
-- Matching and unification
- matchTys, matchTyX, tcMatchPreds, MatchEnv(..),
+ tcMatchTys, tcMatchTyX, tcMatchPreds, MatchEnv(..),
- unifyTys, unifyTysX,
+ tcUnifyTys, tcUnifyTysX,
- tcRefineTys, tcMatchTys, coreRefineTys,
+ gadtRefineTys, gadtMatchTys, coreRefineTys,
-- Re-export
MaybeErr(..)
#include "HsVersions.h"
+import Type ( pprParendType )
import Var ( Var, TyVar, tyVarKind )
import VarEnv
import VarSet
, me_env :: RnEnv2 -- Renaming envt for nested foralls
} -- In-scope set includes template tyvars
-matchTys :: TyVarSet -- Template tyvars
+tcMatchTys :: TyVarSet -- Template tyvars
-> [Type] -- Template
-> [Type] -- Target
-> Maybe TvSubstEnv -- One-shot; in principle the template
-- variables could be free in the target
-matchTys tmpls tys1 tys2
+tcMatchTys tmpls tys1 tys2
= match_tys (ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope_tyvars})
emptyTvSubstEnv
tys1 tys2
menv = ME { me_tmpls = mkVarSet tmpls, me_env = mkRnEnv2 in_scope_tyvars }
in_scope_tyvars = mkInScopeSet (tyVarsOfTheta ps1 `unionVarSet` tyVarsOfTheta ps2)
-matchTyX :: MatchEnv
+tcMatchTyX :: MatchEnv
-> TvSubstEnv -- Substitution to extend
-> Type -- Template
-> Type -- Target
-> Maybe TvSubstEnv
-matchTyX menv subst ty1 ty2 = match menv subst ty1 ty2 -- Rename for export
+tcMatchTyX menv subst ty1 ty2 = match menv subst ty1 ty2 -- Rename for export
\end{code}
Now the internals of matching
%************************************************************************
\begin{code}
-tcRefineTys, tcMatchTys
+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
-tcRefineTys ex_tvs subst tys1 tys2
+gadtRefineTys ex_tvs subst tys1 tys2
= initUM (tryToBind (mkVarSet ex_tvs)) (unify_tys subst tys1 tys2)
-tcMatchTys ex_tvs subst tys1 tys2
+gadtMatchTys ex_tvs subst tys1 tys2
= initUM (bindOnly (mkVarSet ex_tvs)) (unify_tys subst tys1 tys2)
----------------------------
coreRefineTys :: [TyVar] -- Try to unify these
-> TvSubst -- A full-blown apply-once substitition
- -> Type -- A fixed point of the incoming substitution
- -> Type
+ -> Type -- Both types should be a fixed point
+ -> Type -- of the incoming substitution
-> Maybe TvSubstEnv -- In-scope set is unaffected
-- Used by Core Lint and the simplifier. Takes a full apply-once substitution.
-- The incoming substitution's in-scope set should mention all the variables free
-- in the incoming types
coreRefineTys ex_tvs subst@(TvSubst in_scope orig_env) ty1 ty2
= maybeErrToMaybe $ initUM (tryToBind (mkVarSet ex_tvs)) $
- do { -- Apply the input substitution; nothing int ty2
- let ty1' = substTy subst ty1
- -- Run the unifier, starting with an empty env
- ; extra_env <- unify emptyTvSubstEnv ty1' ty2
+ do { -- Run the unifier, starting with an empty env
+ ; extra_env <- unify emptyTvSubstEnv ty1 ty2
-- Find the fixed point of the resulting non-idempotent
- -- substitution, and apply it to the
+ -- substitution, and apply it to the incoming substitution
; let extra_subst = TvSubst in_scope extra_env_fixpt
extra_env_fixpt = mapVarEnv (substTy extra_subst) extra_env
orig_env' = mapVarEnv (substTy extra_subst) orig_env
; return (orig_env' `plusVarEnv` extra_env_fixpt) }
-
----------------------------
-unifyTys :: TyVarSet -> [Type] -> [Type] -> Maybe TvSubstEnv
-unifyTys bind_these tys1 tys2
+tcUnifyTys :: TyVarSet -> [Type] -> [Type] -> Maybe TvSubstEnv
+tcUnifyTys bind_these tys1 tys2
= maybeErrToMaybe $ initUM (bindOnly bind_these) $
unify_tys emptyTvSubstEnv tys1 tys2
-unifyTysX :: TyVarSet -> TvSubstEnv -> [Type] -> [Type] -> Maybe TvSubstEnv
-unifyTysX bind_these subst 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
-- nor guarantee that the outgoing one is. That's fixed up by
-- the wrappers.
+-- Respects newtypes, PredTypes
+
unify subst ty1 ty2 = -- pprTrace "unify" (ppr subst <+> pprParendType ty1 <+> pprParendType ty2) $
- unify_ subst ty1 ty2
+ unify_ subst ty1 ty2
-- in unify_, any NewTcApps/Preds should be taken at face value
unify_ subst (TyVarTy tv1) ty2 = uVar False subst tv1 ty2
projects / ghc-hetmet.git / commitdiff