\begin{code}
module Unify (
-- Matching and unification
- tcMatchTys, tcMatchTyX, tcMatchPreds, MatchEnv(..),
+ tcMatchTys, tcMatchTyX, ruleMatchTyX, tcMatchPreds, MatchEnv(..),
tcUnifyTys,
gadtRefineTys, BindFlag(..),
- coreRefineTys,
+ coreRefineTys, TypeRefinement,
-- Re-export
MaybeErr(..)
import VarEnv
import VarSet
import Kind ( isSubKind )
-import Type ( typeKind, tyVarsOfType, tyVarsOfTypes, tyVarsOfTheta,
+import Type ( typeKind, tyVarsOfType, tyVarsOfTypes, tyVarsOfTheta, mkTyVarTys,
TvSubstEnv, emptyTvSubstEnv, TvSubst(..), substTy, tcEqTypeX )
import TypeRep ( Type(..), PredType(..), funTyCon )
+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
tvs2 = tyVarsOfTypes tys2
----------------------------
-coreRefineTys :: InScopeSet -- Superset of free vars of either type
- -> [TyVar] -- Try to unify these
- -> 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 in_scope ex_tvs ty1 ty2
- = maybeErrToMaybe $ initUM (tryToBind (mkVarSet ex_tvs)) $
+coreRefineTys :: InScopeSet -- Superset of free vars of either type
+ -> DataCon -> [TyVar] -- Case pattern (con tv1 .. tvn ...)
+ -> Type -- Type of scrutinee
+ -> Maybe TypeRefinement
+
+type TypeRefinement = (TvSubstEnv, Bool)
+ -- The Bool is True iff all the bindings in the
+ -- env are for the pattern type variables
+ -- In this case, there is no type refinement
+ -- for already-in-scope type variables
+
+-- Used by Core Lint and the simplifier.
+coreRefineTys in_scope con tvs scrut_ty
+ = maybeErrToMaybe $ initUM (tryToBind tv_set) $
do { -- Run the unifier, starting with an empty env
- ; subst_env <- unify emptyTvSubstEnv ty1 ty2
+ ; 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
subst_env_fixpt = mapVarEnv (substTy subst) subst_env
- ; return subst_env_fixpt }
+
+ ; return (subst_env_fixpt, all_bound_here subst_env) }
+ where
+ 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
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 (NoteTy _ 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