\begin{code}
module Unify (
-- Matching and unification
- tcMatchTys, tcMatchTyX, tcMatchPreds, MatchEnv(..),
+ tcMatchTys, tcMatchTyX, ruleMatchTyX, tcMatchPreds, MatchEnv(..),
tcUnifyTys,
import VarSet
import Kind ( isSubKind )
import Type ( typeKind, tyVarsOfType, tyVarsOfTypes, tyVarsOfTheta, mkTyVarTys,
- TvSubstEnv, emptyTvSubstEnv, TvSubst(..), substTy, tcEqTypeX )
+ TvSubstEnv, emptyTvSubstEnv, TvSubst(..), substTy, tcEqTypeX,
+ mkOpenTvSubst, tcView )
import TypeRep ( Type(..), PredType(..), funTyCon )
-import DataCon ( DataCon, dataConResTy )
+import DataCon ( DataCon, dataConInstResTy )
import Util ( snocView )
import ErrUtils ( Message )
import Outputable
-- We're assuming that all the interesting
-- tyvars in tys1 are in tmpls
+-- This is similar, but extends a substitution
+tcMatchTyX :: TyVarSet -- Template tyvars
+ -> TvSubst -- Substitution to extend
+ -> Type -- Template
+ -> Type -- Target
+ -> Maybe TvSubst
+tcMatchTyX tmpls (TvSubst in_scope subst_env) ty1 ty2
+ = case match menv subst_env ty1 ty2 of
+ Just subst_env -> Just (TvSubst in_scope subst_env)
+ Nothing -> Nothing
+ where
+ menv = ME {me_tmpls = tmpls, me_env = mkRnEnv2 in_scope}
+
tcMatchPreds
:: [TyVar] -- Bind these
-> [PredType] -> [PredType]
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
+ruleMatchTyX :: MatchEnv
-> TvSubstEnv -- Substitution to extend
-> Type -- Template
-> Type -- Target
-> Maybe TvSubstEnv
-tcMatchTyX menv subst ty1 ty2 = match menv subst ty1 ty2 -- Rename for export
+ruleMatchTyX menv subst ty1 ty2 = match menv subst ty1 ty2 -- Rename for export
\end{code}
Now the internals of matching
-- This matcher works on source types; that is,
-- it respects NewTypes and PredType
-match menv subst (NoteTy _ ty1) ty2 = match menv subst ty1 ty2
-match menv subst ty1 (NoteTy _ ty2) = match menv subst ty1 ty2
+match menv subst ty1 ty2 | Just ty1' <- tcView ty1 = match menv subst ty1' ty2
+match menv subst ty1 ty2 | Just ty2' <- tcView ty2 = match menv subst ty1 ty2'
match menv subst (TyVarTy tv1) ty2
| tv1 `elemVarSet` me_tmpls menv
tvs2 = tyVarsOfTypes tys2
----------------------------
-coreRefineTys :: InScopeSet -- Superset of free vars of either type
- -> DataCon -> [TyVar] -- Case pattern (con tv1 .. tvn ...)
+coreRefineTys :: DataCon -> [TyVar] -- Case pattern (con tv1 .. tvn ...)
-> Type -- Type of scrutinee
-> Maybe TypeRefinement
-- for already-in-scope type variables
-- Used by Core Lint and the simplifier.
-coreRefineTys in_scope con tvs scrut_ty
+coreRefineTys con tvs scrut_ty
= maybeErrToMaybe $ initUM (tryToBind tv_set) $
do { -- Run the unifier, starting with an empty env
; subst_env <- unify emptyTvSubstEnv pat_res_ty scrut_ty
-- Find the fixed point of the resulting non-idempotent substitution
- ; let subst = TvSubst in_scope subst_env_fixpt
+ ; let subst = mkOpenTvSubst subst_env_fixpt
subst_env_fixpt = mapVarEnv (substTy subst) subst_env
; return (subst_env_fixpt, all_bound_here subst_env) }
where
- pat_res_ty = dataConResTy con (mkTyVarTys tvs)
+ pat_res_ty = dataConInstResTy con (mkTyVarTys tvs)
-- 'tvs' are the tyvars bound by the pattern
tv_set = mkVarSet tvs
all_bound_here env = all bound_here (varEnvKeys env)
bound_here uniq = elemVarSetByKey uniq tv_set
-
-----------------------------
-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)
+-- This version is used by the type checker
+gadtRefineTys :: TvSubst
+ -> DataCon -> [TyVar]
+ -> [Type] -> [Type]
+ -> MaybeErr Message (TvSubst, Bool)
+-- The bool is True <=> the only *new* bindings are for pat_tvs
+
+gadtRefineTys (TvSubst in_scope env1) con pat_tvs pat_tys ctxt_tys
+ = initUM (tryToBind tv_set) $
+ do { -- Run the unifier, starting with an empty env
+ ; env2 <- unify_tys env1 pat_tys ctxt_tys
+
+ -- Find the fixed point of the resulting non-idempotent substitution
+ ; let subst2 = TvSubst in_scope subst_env_fixpt
+ subst_env_fixpt = mapVarEnv (substTy subst2) env2
+
+ ; return (subst2, all_bound_here env2) }
+ where
+ -- 'tvs' are the tyvars bound by the pattern
+ tv_set = mkVarSet pat_tvs
+ all_bound_here env = all bound_here (varEnvKeys env)
+ bound_here uniq = elemVarEnvByKey uniq env1 || elemVarSetByKey uniq tv_set
+ -- The bool is True <=> the only *new* bindings are for pat_tvs
----------------------------
tryToBind :: TyVarSet -> TyVar -> BindFlag
unify_ subst (TyVarTy tv1) ty2 = uVar False subst tv1 ty2
unify_ subst ty1 (TyVarTy tv2) = uVar True subst tv2 ty1
-unify_ subst (NoteTy _ ty1) ty2 = unify subst ty1 ty2
-unify_ subst ty1 (NoteTy _ ty2) = unify subst ty1 ty2
+unify_ subst ty1 ty2 | Just ty1' <- tcView ty1 = unify subst ty1' ty2
+unify_ subst ty1 ty2 | Just ty2' <- tcView ty2 = unify subst ty1 ty2'
unify_ subst (PredTy p1) (PredTy p2) = unify_pred subst p1 p2
Just ty' | swap -> unify subst ty ty'
| otherwise -> unify subst ty' ty
-- No, continue
- Nothing -> uUnrefined subst tv1 ty
+ Nothing -> uUnrefined subst tv1 ty ty
uUnrefined :: TvSubstEnv -- An existing substitution to extend
-> TyVar -- Type variable to be unified
-> Type -- with this type
+ -> Type -- (de-noted version)
-> UM TvSubstEnv
-- We know that tv1 isn't refined
-uUnrefined subst tv1 ty2@(TyVarTy tv2)
- | tv1 == tv2 -- Same, do nothing
+
+uUnrefined subst tv1 ty2 ty2'
+ | Just ty2'' <- tcView ty2'
+ = uUnrefined subst tv1 ty2 ty2'' -- Unwrap synonyms
+ -- This is essential, in case we have
+ -- type Foo a = a
+ -- and then unify a :=: Foo a
+
+uUnrefined subst tv1 ty2 (TyVarTy tv2)
+ | tv1 == tv2 -- Same type variable
= return subst
-- Check to see whether tv2 is refined
| Just ty' <- lookupVarEnv subst tv2
- = uUnrefined subst tv1 ty'
+ = uUnrefined subst tv1 ty' ty'
-- So both are unrefined; next, see if the kinds force the direction
| k1 == k2 -- Can update either; so check the bind-flags
k2 = tyVarKind tv2
bind tv ty = return (extendVarEnv subst tv ty)
-uUnrefined subst tv1 ty2 -- ty2 is not a type variable
- | tv1 `elemVarSet` substTvSet subst (tyVarsOfType ty2)
+uUnrefined subst tv1 ty2 ty2' -- ty2 is not a type variable
+ | tv1 `elemVarSet` substTvSet subst (tyVarsOfType ty2')
= failWith (occursCheck tv1 ty2) -- Occurs check
| not (k2 `isSubKind` k1)
= failWith (kindMisMatch tv1 ty2) -- Kind check
| otherwise
- = bindTv subst tv1 ty2
+ = bindTv subst tv1 ty2 -- Bind tyvar to the synonym if poss
where
k1 = tyVarKind tv1
- k2 = typeKind ty2
+ k2 = typeKind ty2'
substTvSet :: TvSubstEnv -> TyVarSet -> TyVarSet
-- Apply the non-idempotent substitution to a set of type variables,
projects / ghc-hetmet.git / blobdiff