Cover PredTy case in Type.tyFamInsts

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

diff --git a/compiler/types/Unify.lhs b/compiler/types/Unify.lhs
index 7c8ad9d..3e35ac6 100644 (file)
--- a/compiler/types/Unify.lhs
+++ b/compiler/types/Unify.lhs
@@ -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 }