remove empty dir
[ghc-hetmet.git] / ghc / compiler / types / Unify.lhs
index e6a0878..f60c7be 100644 (file)
@@ -20,7 +20,8 @@ import VarEnv
 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, dataConInstResTy )
 import Util            ( snocView )
@@ -127,8 +128,8 @@ match :: MatchEnv   -- For the most part this is pushed downwards
 -- 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
@@ -221,8 +222,7 @@ tcUnifyTys bind_fn tys1 tys2
     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
 
@@ -233,13 +233,13 @@ type TypeRefinement = (TvSubstEnv, Bool)
        -- 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) }
@@ -250,18 +250,30 @@ coreRefineTys in_scope con tvs scrut_ty
     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
@@ -294,8 +306,8 @@ unify subst ty1 ty2 = -- pprTrace "unify" (ppr subst <+> pprParendType ty1 <+> p
 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
 
@@ -368,8 +380,9 @@ uUnrefined :: TvSubstEnv          -- An existing substitution to extend
 
 -- We know that tv1 isn't refined
 
-uUnrefined subst tv1 ty2 (NoteTy _ ty2')
-  = uUnrefined subst tv1 ty2 ty2'      -- Unwrap synonyms
+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