+ = 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)