tcUnifyTys, BindFlag(..)
) where
-import HsSyn ( ExprCoFn(..), idCoercion, isIdCoercion )
+import HsSyn ( HsWrapper(..), idHsWrapper, isIdHsWrapper )
import Coercion ( Coercion, mkSymCoercion, mkTransCoercion, mkUnsafeCoercion,
mkLeftCoercion, mkRightCoercion, mkCoKind, coercionKindPredTy,
splitCoercionKind, decomposeCo, coercionKind )
emptyRefinement = (Reft emptyInScopeSet emptyVarEnv)
-refineType :: Refinement -> Type -> (ExprCoFn, Type)
+refineType :: Refinement -> Type -> (HsWrapper, Type)
-- Apply the refinement to the type.
-- If (refineType r ty) = (co, ty')
-- Then co :: ty:=:ty'
refineType (Reft in_scope env) ty
| not (isEmptyVarEnv env), -- Common case
any (`elemVarEnv` env) (varSetElems (tyVarsOfType ty))
- = (ExprCoFn (substTy co_subst ty), substTy tv_subst ty)
+ = (WpCo (substTy co_subst ty), substTy tv_subst ty)
| otherwise
- = (idCoercion, ty) -- The type doesn't mention any refined type variables
+ = (idHsWrapper, ty) -- 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 -> (ExprCoFn, Type)
+refineResType :: Refinement -> Type -> (HsWrapper, 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
- (ExprCoFn co, ty1) -> (ExprCoFn (mkSymCoercion co), ty1)
- (id_co, ty1) -> ASSERT( isIdCoercion id_co )
- (idCoercion, ty1)
+ (WpCo co, ty1) -> (WpCo (mkSymCoercion co), ty1)
+ (id_co, ty1) -> ASSERT( isIdHsWrapper id_co )
+ (idHsWrapper, ty1)
\end{code}
-- then use transitivity with the original coercion
where
(co_fn, ty') = refineType (Reft in_scope fixpt) ty
- co1 | ExprCoFn co'' <- co_fn = mkTransCoercion co co''
- | otherwise = ASSERT( isIdCoercion co_fn ) co
+ co1 | WpCo co'' <- co_fn = mkTransCoercion co co''
+ | otherwise = ASSERT( isIdHsWrapper co_fn ) co
-----------------------------
fixTvSubstEnv :: InScopeSet -> TvSubstEnv -> TvSubstEnv
-> UM InternalReft
-- We know that tv1 isn't refined
--- PRE-CONDITION: in the call (uUnrefined r co tv ty ty'), we know that
--- co :: tv:=:ty
+-- PRE-CONDITION: in the call (uUnrefined False r co tv1 ty2 ty2'), we know that
+-- co :: tv1:=:ty2
+-- and if the first argument is True instead, we know
+-- co :: ty2:=:tv1
uUnrefined swap subst co tv1 ty2 ty2'
| Just ty2'' <- tcView ty2'