\begin{code}
module TcGadt (
- Refinement, emptyRefinement, gadtRefine,
- refineType, refineResType,
+ Refinement, emptyRefinement, isEmptyRefinement,
+ gadtRefine,
+ refineType, refinePred, refineResType,
dataConCanMatch,
tcUnifyTys, BindFlag(..)
) where
import HsSyn
import Coercion
+import Type
+
import TypeRep
import DataCon
import Var
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.
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 -> (HsWrapper, Type)
-- Like refineType, but returns the 'sym' coercion
-- If (refineResType r ty) = (co, ty')
do_one reft co_var = unify reft (TyVarTy co_var) ty1 ty2
where
(ty1,ty2) = splitCoercionKind (tyVarKind co_var)
-\end{code}
+\end{code}
%************************************************************************
%* *
fixpt = mapVarEnv (substTy (mkTvSubst in_scope fixpt)) env
----------------------------
-dataConCanMatch :: DataCon -> [Type] -> Bool
+dataConCanMatch :: [Type] -> DataCon -> Bool
-- Returns True iff the data con can match a scrutinee of type (T tys)
-- where T is the type constructor for the data con
--
-- Instantiate the equations and try to unify them
-dataConCanMatch con tys
+dataConCanMatch tys con
+ | null eq_spec = True -- Common
+ | all isTyVarTy tys = True -- Also common
+ | otherwise
= isJust (tcUnifyTys (\tv -> BindMe)
(map (substTyVar subst . fst) eq_spec)
(map snd eq_spec))