X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypes%2FUnify.lhs;h=a9586b6bf4f82628d21c0ed6e1e4b9c5e5301381;hp=c1ef798284068851384d4bf86e9e628d6b72b515;hb=56a437ee698c5a46864e7fcc530707742589ef7d;hpb=77c6ba6f015933989594d167162265b5633f74e3

diff --git a/compiler/types/Unify.lhs b/compiler/types/Unify.lhs
index c1ef798..a9586b6 100644
--- a/compiler/types/Unify.lhs
+++ b/compiler/types/Unify.lhs
@@ -16,7 +16,7 @@ module Unify (
 	Refinement, emptyRefinement, isEmptyRefinement, 
 	matchRefine, refineType, refinePred, refineResType,
 
-        -- side-effect free unification
+        -- Side-effect free unification
         tcUnifyTys, BindFlag(..)
 
    ) where
@@ -206,7 +206,7 @@ match_kind :: MatchEnv -> TvSubstEnv -> TyVar -> Type -> Maybe TvSubstEnv
 -- Match the kind of the template tyvar with the kind of Type
 -- Note [Matching kinds]
 match_kind menv subst tv ty
-  | isCoVar tv = do { let (ty1,ty2) = splitCoercionKind (tyVarKind tv)
+  | isCoVar tv = do { let (ty1,ty2) = coVarKind tv
 			  (ty3,ty4) = coercionKind ty
 		    ; subst1 <- match menv subst ty1 ty3
 		    ; match menv subst1 ty2 ty4 }
@@ -384,7 +384,7 @@ dataConCannotMatch tys con
 data Refinement = Reft InScopeSet InternalReft 
 
 type InternalReft = TyVarEnv (Coercion, Type)
--- INVARIANT:   a->(co,ty)   then   co :: (a:=:ty)
+-- INVARIANT:   a->(co,ty)   then   co :: (a~ty)
 -- Not necessarily idemopotent
 
 instance Outputable Refinement where
@@ -401,7 +401,7 @@ isEmptyRefinement (Reft _ env) = isEmptyVarEnv env
 refineType :: Refinement -> Type -> Maybe (Coercion, Type)
 -- Apply the refinement to the type.
 -- If (refineType r ty) = (co, ty')
--- Then co :: ty:=:ty'
+-- Then co :: ty~ty'
 -- Nothing => the refinement does nothing to this type
 refineType (Reft in_scope env) ty
   | not (isEmptyVarEnv env),		-- Common case
@@ -427,7 +427,7 @@ refinePred (Reft in_scope env) pred
 refineResType :: Refinement -> Type -> Maybe (Coercion, Type)
 -- Like refineType, but returns the 'sym' coercion
 -- If (refineResType r ty) = (co, ty')
--- Then co :: ty':=:ty
+-- Then co :: ty'~ty
 refineResType reft ty
   = case refineType reft ty of
       Just (co, ty1) -> Just (mkSymCoercion co, ty1)
@@ -617,8 +617,8 @@ uVar :: TvSubstEnv	-- An existing substitution to extend
      -> UM TvSubstEnv
 
 -- PRE-CONDITION: in the call (uVar swap r tv1 ty), we know that
---	if swap=False	(tv1:=:ty)
---	if swap=True	(ty:=:tv1)
+--	if swap=False	(tv1~ty)
+--	if swap=True	(ty~tv1)
 
 uVar subst tv1 ty
  = -- Check to see whether tv1 is refined by the substitution
@@ -640,7 +640,7 @@ uUnrefined subst tv1 ty2 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
+		-- and then unify a ~ Foo a
 
 uUnrefined subst tv1 ty2 (TyVarTy tv2)
   | tv1 == tv2		-- Same type variable
@@ -656,15 +656,6 @@ uUnrefined subst tv1 ty2 (TyVarTy tv2)
 	; b2 <- tvBindFlag tv2
 	; case (b1,b2) of
 	    (BindMe, _) 	 -> bind tv1 ty2
-
-	    (AvoidMe, BindMe)	 -> bind tv2 ty1
-	    (AvoidMe, _)	 -> bind 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
 	}
@@ -704,29 +695,33 @@ bindTv :: TvSubstEnv -> TyVar -> Type -> UM TvSubstEnv
 bindTv subst tv ty	-- ty is not a type variable
   = do  { b <- tvBindFlag tv
 	; case b of
-	    Skolem   -> failWith (misMatch (TyVarTy tv) ty)
-	    WildCard -> return subst
-	    _other   -> return $ extendVarEnv subst tv ty
+	    Skolem -> failWith (misMatch (TyVarTy tv) ty)
+	    BindMe -> return $ extendVarEnv subst tv ty
 	}
 \end{code}
 
 %************************************************************************
 %*									*
-		Unification monad
+		Binding decisions
 %*									*
 %************************************************************************
 
 \begin{code}
 data BindFlag 
   = BindMe	-- A regular type variable
-  | AvoidMe	-- Like BindMe but, given the choice, avoid binding it
 
   | Skolem	-- This type variable is a skolem constant
 		-- Don't bind it; it only matches itself
+\end{code}
+
 
-  | WildCard 	-- This type variable matches anything,
-		-- and does not affect the substitution
+%************************************************************************
+%*									*
+		Unification monad
+%*									*
+%************************************************************************
 
+\begin{code}
 newtype UM a = UM { unUM :: (TyVar -> BindFlag)
 		         -> MaybeErr Message a }