Commit 19da321b authored by simonpj's avatar simonpj
Browse files

[project @ 2005-01-05 15:28:39 by simonpj]

------------------------
          GADTs and unification
  	------------------------

1. Adjustment to typechecking of pattern matching the call to
   gadtRefineTys in TcPat.  Now wobbly types are treated as wild
   cards in the unification process.

2. Add the WildCard possibility to the BindFlag in types/Unify.lhs

3. Some related refactoring of tcMatchTys etc.
parent df68e45e
......@@ -51,9 +51,9 @@ import TcEnv ( tcLookupId, checkWellStaged, topIdLvl, tcMetaTy )
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,
......@@ -66,7 +66,8 @@ import TcType ( Type, TcType, TcThetaType, TcTyVarSet, TcTyVar,
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 )
......@@ -80,7 +81,7 @@ import Name ( Name, mkMethodOcc, getOccName, getSrcLoc, nameModule,
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 )
......@@ -577,7 +578,7 @@ addInst dflags home_ie dfun
; 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 ()
......@@ -622,12 +623,12 @@ addDictLoc dfun thing_inside
%************************************************************************
\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
......@@ -697,6 +698,7 @@ lookupInst dict@(Dict _ pred@(ClassP clas tys) loc)
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
......@@ -710,29 +712,28 @@ instantiate_dfun tenv dfun_id pred loc
-- 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)
......
......@@ -31,7 +31,7 @@ import Inst ( tcSyntaxName, tcInstCall )
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 )
......@@ -282,16 +282,10 @@ tcMatchPats :: [LPat Name]
-- 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
......
......@@ -25,7 +25,7 @@ import TcEnv ( newLocalName, tcExtendIdEnv1, tcExtendTyVarEnv2,
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
......@@ -34,7 +34,7 @@ import TcUnify ( tcSubPat, Expected(..), zapExpectedType,
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 )
......@@ -118,15 +118,12 @@ tcCheckPats ctxt pats tys thing_inside -- A trivial wrapper
%************************************************************************
\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.
......@@ -501,17 +498,15 @@ 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 = 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]
......
......@@ -16,15 +16,15 @@ module FunDeps (
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}
......@@ -299,34 +299,40 @@ checkClsFD qtvs fd clas_tvs tys1 tys2
-- 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
--
......@@ -336,6 +342,9 @@ checkClsFD qtvs fd clas_tvs tys1 tys2
-- 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
......
......@@ -19,11 +19,11 @@ module InstEnv (
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
......@@ -41,6 +41,17 @@ import Maybe ( isJust )
%* *
%************************************************************************
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
......@@ -53,7 +64,20 @@ data ClsInstEnv
-- 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
......@@ -107,32 +131,6 @@ simpleDFunClassTyCon dfun
%* *
%************************************************************************
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
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......@@ -273,9 +271,9 @@ thing we are looking up can have an arbitrary "flexi" part.
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
......@@ -303,11 +301,11 @@ lookupInstEnv dflags (pkg_ie, home_ie) cls tys
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
......@@ -317,8 +315,19 @@ lookup_inst_env env key_cls key_tys key_all_tvs
-- 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:
......@@ -337,25 +346,8 @@ lookup_inst_env env key_cls key_tys key_all_tvs
-- 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)
......
......@@ -63,9 +63,9 @@ module Type (
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,
......@@ -1025,6 +1025,8 @@ type TvSubstEnv = TyVarEnv Type
-- 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
......@@ -1051,6 +1053,9 @@ getTvInScope (TvSubst in_scope _) = in_scope
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
......
......@@ -3,9 +3,11 @@ module Unify (
-- Matching and unification
tcMatchTys, tcMatchTyX, tcMatchPreds, MatchEnv(..),
tcUnifyTys, tcUnifyTysX,
tcUnifyTys,
gadtRefineTys, gadtMatchTys, coreRefineTys,
gadtRefineTys, BindFlag(..),
coreRefineTys,
-- Re-export
MaybeErr(..)
......@@ -18,7 +20,7 @@ import VarEnv
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 )
......@@ -65,15 +67,16 @@ data MatchEnv
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
......@@ -87,6 +90,7 @@ 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)
-- This one is called from the expression matcher, which already has a MatchEnv in hand
tcMatchTyX :: MatchEnv
-> TvSubstEnv -- Substitution to extend
-> Type -- Template
......@@ -179,23 +183,28 @@ match_pred menv subst p1 p2 = Nothing
%************************************************************************
%* *
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
......@@ -217,26 +226,20 @@ coreRefineTys in_scope ex_tvs ty1 ty2
; 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}
......@@ -321,9 +324,9 @@ uVar :: Bool -- Swapped
-> 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
......@@ -349,49 +352,38 @@ uUnrefined subst tv1 ty2@(TyVarTy tv2)
= 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