Remove dead code dealing with type refinement

diff --git a/compiler/types/Unify.lhs b/compiler/types/Unify.lhs
index a9586b6..de5ac49 100644 (file)
--- a/compiler/types/Unify.lhs
+++ b/compiler/types/Unify.lhs
@@ -12,10 +12,6 @@ module Unify (
        
        dataConCannotMatch,
 
-        -- GADT type refinement
-       Refinement, emptyRefinement, isEmptyRefinement, 
-       matchRefine, refineType, refinePred, refineResType,
-
         -- Side-effect free unification
         tcUnifyTys, BindFlag(..)
 
@@ -374,130 +370,6 @@ dataConCannotMatch tys con
 \end{code}
 
 
-%************************************************************************
-%*                                                                     *
-               What a refinement is
-%*                                                                     *
-%************************************************************************
-
-\begin{code}
-data Refinement = Reft InScopeSet InternalReft 
-
-type InternalReft = TyVarEnv (Coercion, Type)
--- INVARIANT:   a->(co,ty)   then   co :: (a~ty)
--- Not necessarily idemopotent
-
-instance Outputable Refinement where
-  ppr (Reft _in_scope env)
-    = ptext (sLit "Refinement") <+>
-        braces (ppr env)
-
-emptyRefinement :: Refinement
-emptyRefinement = (Reft emptyInScopeSet emptyVarEnv)
-
-isEmptyRefinement :: Refinement -> Bool
-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'
--- Nothing => the refinement does nothing to this type
-refineType (Reft in_scope env) ty
-  | not (isEmptyVarEnv env),           -- Common case
-    any (`elemVarEnv` env) (varSetElems (tyVarsOfType ty))
-  = Just (substTy co_subst ty, substTy tv_subst ty)
-  | otherwise
-  = Nothing    -- The type doesn't mention any refined type variables
-  where
-    tv_subst = mkTvSubst in_scope (mapVarEnv snd env)
-    co_subst = mkTvSubst in_scope (mapVarEnv fst env)
- 
-refinePred :: Refinement -> PredType -> Maybe (Coercion, PredType)
-refinePred (Reft in_scope env) pred
-  | not (isEmptyVarEnv env),           -- Common case
-    any (`elemVarEnv` env) (varSetElems (tyVarsOfPred pred))
-  = Just (mkPredTy (substPred co_subst pred), substPred tv_subst pred)
-  | otherwise
-  = Nothing    -- The type doesn't mention any refined type variables
-  where
-    tv_subst = mkTvSubst in_scope (mapVarEnv snd env)
-    co_subst = mkTvSubst in_scope (mapVarEnv fst env)
- 
-refineResType :: Refinement -> Type -> Maybe (Coercion, Type)
--- Like refineType, but returns the 'sym' coercion
--- If (refineResType r ty) = (co, ty')
--- Then co :: ty'~ty
-refineResType reft ty
-  = case refineType reft ty of
-      Just (co, ty1) -> Just (mkSymCoercion co, ty1)
-      Nothing       -> Nothing
-\end{code}
-
-
-%************************************************************************
-%*                                                                     *
-               Simple generation of a type refinement
-%*                                                                     *
-%************************************************************************
-
-\begin{code}
-matchRefine :: [TyVar] -> [Coercion] -> Refinement
-\end{code}
-
-Given a list of coercions, where for each coercion c::(ty1~ty2), the type ty2
-is a specialisation of ty1, produce a type refinement that maps the variables
-of ty1 to the corresponding sub-terms of ty2 using appropriate coercions; eg,
-
-  matchRefine (co :: [(a, b)] ~ [(c, Maybe d)])
-    = { right (left (right co)) :: a ~ c
-      , right (right co)        :: b ~ Maybe d
-      }
-
-Precondition: The rhs types must indeed be a specialisation of the lhs types;
-  i.e., some free variables of the lhs are replaced with either distinct free 
-  variables or proper type terms to obtain the rhs.  (We don't perform full
-  unification or type matching here!)
-
-NB: matchRefine does *not* expand the type synonyms.
-
-\begin{code}
-matchRefine in_scope_tvs cos 
-  = Reft in_scope (foldr plusVarEnv emptyVarEnv (map refineOne cos))
-  where
-    in_scope = mkInScopeSet (mkVarSet in_scope_tvs)
-       -- NB: in_scope_tvs include both coercion variables
-       --     *and* the tyvars in their kinds
-
-    refineOne co = refine co ty1 ty2
-      where
-        (ty1, ty2) = coercionKind co
-
-    refine co (TyVarTy tv) ty                     = unitVarEnv tv (co, ty)
-    refine co (TyConApp _ tys) (TyConApp _ tys')  = refineArgs co tys tys'
-    refine _  (PredTy _) (PredTy _)               = 
-      error "Unify.matchRefine: PredTy"
-    refine co (FunTy arg res) (FunTy arg' res')   =
-      refine (mkRightCoercion (mkLeftCoercion co)) arg arg' 
-      `plusVarEnv` 
-      refine (mkRightCoercion co) res res'
-    refine co (AppTy fun arg) (AppTy fun' arg')   = 
-      refine (mkLeftCoercion co) fun fun' 
-      `plusVarEnv`
-      refine (mkRightCoercion co) arg arg'
-    refine co (ForAllTy tv ty) (ForAllTy _tv ty') =
-      refine (mkForAllCoercion tv co) ty ty' `delVarEnv` tv
-    refine _ _ _ = error "RcGadt.matchRefine: mismatch"
-
-    refineArgs :: Coercion -> [Type] -> [Type] -> InternalReft
-    refineArgs co tys tys' = 
-      fst $ foldr refineArg (emptyVarEnv, id) (zip tys tys')
-      where
-        refineArg (ty, ty') (reft, coWrapper) 
-          = (refine (mkRightCoercion (coWrapper co)) ty ty' `plusVarEnv` reft, 
-             mkLeftCoercion . coWrapper)
-\end{code}
-
 
 %************************************************************************
 %*                                                                     *