X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypes%2FUnify.lhs;h=3e35ac6421fcce8dca6c0d2f6bb96e2033efc83c;hb=3a61d75c70f61a2b919e94e85ffe1166e7151b5b;hp=69478bedc6f9b5b381f6b741e3f64e49f72e4065;hpb=35fc429931738f31c60e8a4bb85ef86dd7ce169e;p=ghc-hetmet.git

diff --git a/compiler/types/Unify.lhs b/compiler/types/Unify.lhs
index 69478be..3e35ac6 100644
--- a/compiler/types/Unify.lhs
+++ b/compiler/types/Unify.lhs
@@ -389,7 +389,7 @@ type InternalReft = TyVarEnv (Coercion, Type)
 
 instance Outputable Refinement where
   ppr (Reft _in_scope env)
-    = ptext SLIT("Refinement") <+>
+    = ptext (sLit "Refinement") <+>
         braces (ppr env)
 
 emptyRefinement :: Refinement
@@ -442,7 +442,7 @@ refineResType reft ty
 %************************************************************************
 
 \begin{code}
-matchRefine :: [CoVar] -> Refinement
+matchRefine :: [TyVar] -> [Coercion] -> Refinement
 \end{code}
 
 Given a list of coercions, where for each coercion c::(ty1~ty2), the type ty2
@@ -462,19 +462,16 @@ Precondition: The rhs types must indeed be a specialisation of the lhs types;
 NB: matchRefine does *not* expand the type synonyms.
 
 \begin{code}
-matchRefine co_vars 
-  = Reft in_scope (foldr plusVarEnv emptyVarEnv (map refineOne co_vars))
+matchRefine in_scope_tvs cos 
+  = Reft in_scope (foldr plusVarEnv emptyVarEnv (map refineOne cos))
   where
-    in_scope = foldr extend emptyInScopeSet co_vars
+    in_scope = mkInScopeSet (mkVarSet in_scope_tvs)
+	-- NB: in_scope_tvs include both coercion variables
+	--     *and* the tyvars in their kinds
 
-	-- For each co_var, add it *and* the tyvars it mentions, to in_scope
-    extend co_var in_scope
-      = extendInScopeSetSet in_scope $
-	  extendVarSet (tyVarsOfType (tyVarKind co_var)) co_var
-
-    refineOne co_var = refine (TyVarTy co_var) ty1 ty2
+    refineOne co = refine co ty1 ty2
       where
-        (ty1, ty2) = splitCoercionKind (tyVarKind co_var)
+        (ty1, ty2) = coercionKind co
 
     refine co (TyVarTy tv) ty                     = unitVarEnv tv (co, ty)
     refine co (TyConApp _ tys) (TyConApp _ tys')  = refineArgs co tys tys'
@@ -659,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
 	}
@@ -707,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 }
 
@@ -767,23 +759,23 @@ maybeErrToMaybe (Failed _)    = Nothing
 \begin{code}
 misMatch :: Type -> Type -> SDoc
 misMatch t1 t2
-  = ptext SLIT("Can't match types") <+> quotes (ppr t1) <+> 
-    ptext SLIT("and") <+> quotes (ppr t2)
+  = ptext (sLit "Can't match types") <+> quotes (ppr t1) <+> 
+    ptext (sLit "and") <+> quotes (ppr t2)
 
 lengthMisMatch :: [Type] -> [Type] -> SDoc
 lengthMisMatch tys1 tys2
-  = sep [ptext SLIT("Can't match unequal length lists"), 
+  = sep [ptext (sLit "Can't match unequal length lists"), 
 	 nest 2 (ppr tys1), nest 2 (ppr tys2) ]
 
 kindMisMatch :: TyVar -> Type -> SDoc
 kindMisMatch tv1 t2
-  = vcat [ptext SLIT("Can't match kinds") <+> quotes (ppr (tyVarKind tv1)) <+> 
-	    ptext SLIT("and") <+> quotes (ppr (typeKind t2)),
-	  ptext SLIT("when matching") <+> quotes (ppr tv1) <+> 
-		ptext SLIT("with") <+> quotes (ppr t2)]
+  = vcat [ptext (sLit "Can't match kinds") <+> quotes (ppr (tyVarKind tv1)) <+> 
+	    ptext (sLit "and") <+> quotes (ppr (typeKind t2)),
+	  ptext (sLit "when matching") <+> quotes (ppr tv1) <+> 
+		ptext (sLit "with") <+> quotes (ppr t2)]
 
 occursCheck :: TyVar -> Type -> SDoc
 occursCheck tv ty
-  = hang (ptext SLIT("Can't construct the infinite type"))
+  = hang (ptext (sLit "Can't construct the infinite type"))
        2 (ppr tv <+> equals <+> ppr ty)
 \end{code}