[project @ 2005-11-02 17:41:00 by simonpj]

[ghc-hetmet.git] / ghc / compiler / types / Unify.lhs

diff --git a/ghc/compiler/types/Unify.lhs b/ghc/compiler/types/Unify.lhs
index bb43ce0..e6a0878 100644 (file)
--- a/ghc/compiler/types/Unify.lhs
+++ b/ghc/compiler/types/Unify.lhs
@@ -1,7 +1,7 @@
 \begin{code}
 module Unify ( 
        -- Matching and unification
-       tcMatchTys, tcMatchTyX, tcMatchPreds, MatchEnv(..), 
+       tcMatchTys, tcMatchTyX, ruleMatchTyX, tcMatchPreds, MatchEnv(..), 
 
        tcUnifyTys, 
 
@@ -22,7 +22,7 @@ import Kind           ( isSubKind )
 import Type            ( typeKind, tyVarsOfType, tyVarsOfTypes, tyVarsOfTheta, mkTyVarTys,
                          TvSubstEnv, emptyTvSubstEnv, TvSubst(..), substTy, tcEqTypeX )
 import TypeRep          ( Type(..), PredType(..), funTyCon )
-import DataCon                 ( DataCon, dataConResTy )
+import DataCon                 ( DataCon, dataConInstResTy )
 import Util            ( snocView )
 import ErrUtils                ( Message )
 import Outputable
@@ -81,6 +81,19 @@ tcMatchTys tmpls tys1 tys2
        -- 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]
@@ -92,13 +105,13 @@ tcMatchPreds tmpls ps1 ps2
     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
@@ -231,7 +244,7 @@ coreRefineTys in_scope con tvs scrut_ty
                
        ; 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
@@ -344,22 +357,30 @@ uVar swap subst tv1 ty
      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
@@ -390,16 +411,16 @@ uUnrefined subst tv1 ty2@(TyVarTy tv2)
     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,