Commit 51ab3ed1 authored by's avatar
Browse files

Implement a smart constructor mkUnsafeCoercion, and use it

This just ensures that an unsafe coercion is as localised as possible.
For example, instead of
    UnsafeCo (Int -> t1) (Int -> t2)
    Int -> UnsafeCo t1 t2
parent 88e7faf1
......@@ -379,9 +379,18 @@ mkInstsCoercion co tys = foldl mkInstCoercion co tys
-- | Manufacture a coercion from this air. Needless to say, this is not usually safe,
-- but it is used when we know we are dealing with bottom, which is one case in which
-- it is safe. This is also used implement the @unsafeCoerce#@ primitive.
-- Optimise by pushing down through type constructors
mkUnsafeCoercion :: Type -> Type -> Coercion
mkUnsafeCoercion ty1 ty2 = mkCoercion unsafeCoercionTyCon [ty1, ty2]
mkUnsafeCoercion (TyConApp tc1 tys1) (TyConApp tc2 tys2)
| tc1 == tc2
= TyConApp tc1 (zipWith mkUnsafeCoercion tys1 tys2)
mkUnsafeCoercion (FunTy a1 r1) (FunTy a2 r2)
= FunTy (mkUnsafeCoercion a1 a2) (mkUnsafeCoercion r1 r2)
mkUnsafeCoercion ty1 ty2
| ty1 `coreEqType` ty2 = ty1
| otherwise = mkCoercion unsafeCoercionTyCon [ty1, ty2]
-- See note [Newtype coercions] in TyCon
......@@ -112,8 +112,8 @@ opt_co_tc_app env sym tc desc cos
| otherwise -> opt_trans opt_co1 opt_co2
| sym -> TyConApp tc [opt_co2,opt_co1]
| otherwise -> TyConApp tc [opt_co1,opt_co2]
| sym -> mkUnsafeCoercion ty2' ty1'
| otherwise -> mkUnsafeCoercion ty1' ty2'
CoSym -> opt_co env (not sym) co1
CoLeft -> opt_lr fst
......@@ -125,21 +125,22 @@ opt_co_tc_app env sym tc desc cos
CoInst -- See if the first arg is already a forall
-- ...then we can just extend the current substitution
| Just (tv, co1_body) <- splitForAllTy_maybe co1
-> opt_co (extendTvSubst env tv ty') sym co1_body
-> opt_co (extendTvSubst env tv ty2') sym co1_body
-- See if is *now* a forall
| Just (tv, opt_co1_body) <- splitForAllTy_maybe opt_co1
-> substTyWith [tv] [ty'] opt_co1_body -- An inefficient one-variable substitution
-> substTyWith [tv] [ty2'] opt_co1_body -- An inefficient one-variable substitution
| otherwise
-> TyConApp tc [opt_co1, ty']
ty' = substTy env co2
-> TyConApp tc [opt_co1, ty2']
(co1 : cos1) = cos
(co2 : _) = cos1
ty1' = substTy env co1
ty2' = substTy env co2
-- These opt_cos have the sym pushed into them
opt_co1 = opt_co env sym co1
opt_co2 = opt_co env sym co2
......@@ -362,6 +363,8 @@ etaCoPred_maybe co
= Nothing
etaApp_maybe :: Coercion -> Maybe (Coercion, Coercion)
-- Split a coercion g :: t1a t1b ~ t2a t2b
-- into (left g, right g) if possible
etaApp_maybe co
| Just (co1, co2) <- splitAppTy_maybe co
= Just (co1, co2)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment