Commit 79a8b87c authored by simonpj's avatar simonpj
Browse files

[project @ 2004-12-21 12:22:22 by simonpj]

---------------------------------
     Improve handling of lexically scoped type variables
	---------------------------------

If we have

	f :: T a -> a
	f (x :: T b) = ...

then the lexically scoped variable 'b' should refer to the rigid
type variable 'a', without any intervening wobbliness.  Previously
the in-scope type variables were always mutable TyVars, which were
instantatiated to point to the type they were bound to; but since
the advent of GADTs the intervening mutable type variable is a bad
thing.

Hence
  * In the type environment, ATyVar now carries a type
  * The call to refineTyVars in tc_pat on SigPatIn
    finds the types by matching
  * Then tcExtendTyVarEnv3 extends the type envt appropriately

Rater a lot of huff and puff, but it's quite natural for ATyVar
to contain a type.

Various other small nomenclature changes along the way.
parent d673a348
......@@ -40,7 +40,7 @@ import CoreUtils ( exprIsTrivial )
import qualified Type ( substTy )
import Type ( Type, tyVarsOfType, mkTyVarTy,
TvSubstEnv, TvSubst(..), substTyVar )
TvSubstEnv, TvSubst(..), substTyVarBndr )
import VarSet
import VarEnv
import Var ( setVarUnique, isId, mustHaveLocalBinding )
......@@ -431,7 +431,7 @@ simplLetId subst@(Subst in_scope env tvs) old_id
-- 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)
......@@ -473,9 +473,9 @@ substRecBndrs subst bndrs
\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')
......@@ -510,7 +510,7 @@ subst_id keep_fragile rec_subst subst@(Subst in_scope env tvs) old_id
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
......
......@@ -26,7 +26,7 @@ import Var ( Var )
import VarSet
import VarEnv
import TcType ( TvSubstEnv )
import Unify ( matchTyX, MatchEnv(..) )
import Unify ( tcMatchTyX, MatchEnv(..) )
import BasicTypes ( Activation, CompilerPhase, isActive )
import Outputable
......@@ -324,7 +324,7 @@ We only want to replace (f T) with f', not (f Int).
\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}
......
......@@ -67,7 +67,7 @@ import TcType ( Type, TcType, TcThetaType, TcTyVarSet, TcTyVar,
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(..) )
......@@ -583,7 +583,7 @@ addInst dflags home_ie dfun
; 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
......
......@@ -17,7 +17,7 @@ module TcEnv(
-- Local environment
tcExtendKindEnv,
tcExtendTyVarEnv, tcExtendTyVarEnv2,
tcExtendTyVarEnv, tcExtendTyVarEnv2, tcExtendTyVarEnv3,
tcExtendIdEnv, tcExtendIdEnv1, tcExtendIdEnv2,
tcLookup, tcLookupLocated, tcLookupLocalIds,
tcLookupId, tcLookupTyVar,
......@@ -49,9 +49,9 @@ import HsSyn ( LRuleDecl, LHsBinds, LSig, pprLHsBinds )
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 )
......@@ -197,12 +197,12 @@ tcLookup name
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
......@@ -248,22 +248,25 @@ tcExtendKindEnv things thing_inside
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
......@@ -343,8 +346,8 @@ find_thing ignore_it tidy_env (ATcId id _ _)
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
......@@ -606,6 +609,6 @@ wrongThingErr expected thing name
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}
......@@ -34,8 +34,8 @@ import TcEnv ( tcLookup, tcLookupId, checkProcLevel,
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,
......@@ -634,7 +634,8 @@ tcApp fun args res_ty
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'])
......@@ -722,24 +723,6 @@ checkArgsCtxt fun args (Check expected_res_ty) actual_res_ty tidy_env
| 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}
......
......@@ -392,7 +392,7 @@ kcTyVar name -- Could be a tyvar or a tycon
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
......@@ -500,7 +500,7 @@ ds_var_app :: Name -> [Type] -> TcM Type
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)
......
......@@ -4,7 +4,7 @@
\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"
......@@ -20,18 +20,20 @@ import Inst ( InstOrigin(..),
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 )
......@@ -41,6 +43,7 @@ import PrelNames ( eqStringName, eqName, geName, negateName, minusName,
integralClassName )
import BasicTypes ( isBoxed )
import SrcLoc ( Located(..), SrcSpan, noLoc, unLoc, getLoc )
import Maybes ( catMaybes )
import ErrUtils ( Message )
import Outputable
import FastString
......@@ -241,8 +244,13 @@ tc_pat ctxt (SigPatIn pat sig) pat_ty thing_inside
= 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
......@@ -492,8 +500,8 @@ refineAlt :: PatCtxt -> DataCon
-> 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 {
......@@ -505,6 +513,41 @@ refineAlt ctxt con ex_tvs ctxt_tys pat_tys thing_inside
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]
......
......@@ -48,7 +48,7 @@ import HscTypes ( FixityEnv,
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 )
......@@ -386,15 +386,22 @@ topArrowCtxt = ArrCtxt { proc_level = topProcLevel, proc_banned = [] }
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}
......
......@@ -556,8 +556,8 @@ reifyThing (ATcId id _ _)
; 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) }
......
......@@ -97,7 +97,7 @@ module TcType (
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
......@@ -149,7 +149,7 @@ import Type ( -- Re-exports
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,
......
......@@ -383,6 +383,9 @@ tcSubPat :: TcSigmaType -- Pattern type signature
-> 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
......
......@@ -16,7 +16,7 @@ module FunDeps (
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 )
......@@ -302,10 +302,10 @@ checkClsFD qtvs fd clas_tvs tys1 tys2
-- 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
......
......@@ -23,7 +23,7 @@ import Type ( TvSubstEnv )
import TcType ( Type, tcTyConAppTyCon, tcIsTyVarTy,
tcSplitDFunTy, tyVarsOfTypes, isExistentialTyVar
)
import Unify ( matchTys, unifyTys )
import Unify ( tcMatchTys, tcUnifyTys )
import FunDeps ( checkClsFD )
import TyCon ( TyCon )
import Outputable
......@@ -336,7 +336,7 @@ lookup_inst_env env key_cls key_tys key_all_tvs
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
......@@ -347,7 +347,7 @@ lookup_inst_env env key_cls key_tys key_all_tvs
)
-- 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
......@@ -369,7 +369,7 @@ insert_overlapping new_item (item:items)
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}
......
......@@ -70,7 +70,7 @@ module Type (
extendTvSubst, extendTvSubstList, isInScope,
-- Performing substitution on types
substTy, substTys, substTyWith, substTheta, substTyVar,
substTy, substTys, substTyWith, substTheta, substTyVar, substTyVarBndr,
deShadowTy,
-- Pretty-printing
......@@ -994,7 +994,7 @@ instance Ord PredType where { compare = tcCmpPred }
\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]
{- ----------------------------------------------------------
......@@ -1138,13 +1138,10 @@ substPred subst (ClassP clas tys) = ClassP clas (map (subst_ty subst) tys)
-- 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
......@@ -1158,11 +1155,17 @@ subst_ty subst@(TvSubst in_scope env) ty
-- 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(..)
......@@ -13,6 +13,7 @@ module Unify (
#include "HsVersions.h"
import Type ( pprParendType )
import Var ( Var, TyVar, tyVarKind )
import VarEnv
import VarSet
......@@ -62,13 +63,13 @@ data MatchEnv
, 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
......@@ -87,13 +88,13 @@ tcMatchPreds tmpls ps1 ps2
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
......@@ -182,51 +183,48 @@ match_pred menv subst p1 p2 = Nothing
%************************************************************************
\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
......@@ -258,8 +256,10 @@ unify :: TvSubstEnv -- An existing substitution to extend
-- nor guarantee that the outgoing one is. That's fixed up by
-- the wrappers.