Commit 1d4e94d1 authored by Iavor S. Diatchki's avatar Iavor S. Diatchki
Browse files

Add a provenance field to universal coercions.

Universal coercions allow casting between arbitrary types, so it is a
good idea to keep track where they came from, which now we can do by
using the provenance field in `UnivCo`.

This is also handy for type-checker plugins that provide functionality
beyond what's expressible by GHC's standard coercions:  such plugins
can generate universal coercions, but they should still tag them,
so that if something goes wrong we can link the casts to the plugin.
parent 98686223
......@@ -1124,7 +1124,7 @@ lintCoercion (CoVarCo cv)
2 (ppr cv)) }
; return (k, s, t, r) }
lintCoercion (UnivCo r ty1 ty2)
lintCoercion (UnivCo _prov r ty1 ty2)
= do { k1 <- lintType ty1
; _k2 <- lintType ty2
-- ; unless (k1 `eqKind` k2) $
......
......@@ -528,7 +528,9 @@ lkC env co m
go (AxiomInstCo ax ind cs) = km_axiom >.> lkNamed ax >=> lookupTM ind >=> lkList (lkC env) cs
go (AppCo c1 c2) = km_app >.> lkC env c1 >=> lkC env c2
go (TransCo c1 c2) = km_trans >.> lkC env c1 >=> lkC env c2
go (UnivCo r t1 t2) = km_univ >.> lookupTM r >=> lkT env t1 >=> lkT env t2
-- the provenance is not used in the map
go (UnivCo _ r t1 t2) = km_univ >.> lookupTM r >=> lkT env t1 >=> lkT env t2
go (InstCo c t) = km_inst >.> lkC env c >=> lkT env t
go (ForAllCo v c) = km_forall >.> lkC (extendCME env v) c >=> lkBndr env v
go (CoVarCo v) = km_var >.> lkVar env v
......@@ -550,7 +552,8 @@ xtC env (TyConAppCo r tc cs) f m = m { km_tc_app = km_tc_app m |> xtR r |>> x
xtC env (AxiomInstCo ax ind cs) f m = m { km_axiom = km_axiom m |> xtNamed ax |>> xtInt ind |>> xtList (xtC env) cs f }
xtC env (AppCo c1 c2) f m = m { km_app = km_app m |> xtC env c1 |>> xtC env c2 f }
xtC env (TransCo c1 c2) f m = m { km_trans = km_trans m |> xtC env c1 |>> xtC env c2 f }
xtC env (UnivCo r t1 t2) f m = m { km_univ = km_univ m |> xtR r |>> xtT env t1 |>> xtT env t2 f }
-- the provenance is not used in the map
xtC env (UnivCo _ r t1 t2) f m = m { km_univ = km_univ m |> xtR r |>> xtT env t1 |>> xtT env t2 f }
xtC env (InstCo c t) f m = m { km_inst = km_inst m |> xtC env c |>> xtT env t f }
xtC env (ForAllCo v c) f m = m { km_forall = km_forall m |> xtC (extendCME env v) c
|>> xtBndr env v f }
......
......@@ -957,7 +957,7 @@ ds_tc_coercion subst tc_co
(subst', tv') = Coercion.substTyVarBndr subst tv
go (TcAxiomInstCo ax ind cos)
= AxiomInstCo ax ind (map go cos)
go (TcPhantomCo ty1 ty2) = UnivCo Phantom ty1 ty2
go (TcPhantomCo ty1 ty2) = UnivCo (fsLit "ds_tc_coercion") Phantom ty1 ty2
go (TcSymCo co) = mkSymCo (go co)
go (TcTransCo co1 co2) = mkTransCo (go co1) (go co2)
go (TcNthCo n co) = mkNthCo n (go co)
......
......@@ -1152,7 +1152,7 @@ freeNamesIfCoercion (IfaceCoVarCo _)
= emptyNameSet
freeNamesIfCoercion (IfaceAxiomInstCo ax _ cos)
= unitNameSet ax &&& fnList freeNamesIfCoercion cos
freeNamesIfCoercion (IfaceUnivCo _ t1 t2)
freeNamesIfCoercion (IfaceUnivCo _ _ t1 t2)
= freeNamesIfType t1 &&& freeNamesIfType t2
freeNamesIfCoercion (IfaceSymCo c)
= freeNamesIfCoercion c
......
......@@ -141,7 +141,7 @@ data IfaceCoercion
| IfaceForAllCo IfaceTvBndr IfaceCoercion
| IfaceCoVarCo IfLclName
| IfaceAxiomInstCo IfExtName BranchIndex [IfaceCoercion]
| IfaceUnivCo Role IfaceType IfaceType
| IfaceUnivCo FastString Role IfaceType IfaceType
| IfaceSymCo IfaceCoercion
| IfaceTransCo IfaceCoercion IfaceCoercion
| IfaceNthCo Int IfaceCoercion
......@@ -593,9 +593,9 @@ ppr_co ctxt_prec co@(IfaceForAllCo _ _)
ppr_co _ (IfaceCoVarCo covar) = ppr covar
ppr_co ctxt_prec (IfaceUnivCo r ty1 ty2)
ppr_co ctxt_prec (IfaceUnivCo s r ty1 ty2)
= maybeParen ctxt_prec TyConPrec $
ptext (sLit "UnivCo") <+> ppr r <+>
ptext (sLit "UnivCo") <+> ftext s <+> ppr r <+>
pprParendIfaceType ty1 <+> pprParendIfaceType ty2
ppr_co ctxt_prec (IfaceInstCo co ty)
......@@ -788,11 +788,12 @@ instance Binary IfaceCoercion where
put_ bh a
put_ bh b
put_ bh c
put_ bh (IfaceUnivCo a b c) = do
put_ bh (IfaceUnivCo a b c d) = do
putByte bh 8
put_ bh a
put_ bh b
put_ bh c
put_ bh d
put_ bh (IfaceSymCo a) = do
putByte bh 9
put_ bh a
......@@ -850,7 +851,8 @@ instance Binary IfaceCoercion where
8 -> do a <- get bh
b <- get bh
c <- get bh
return $ IfaceUnivCo a b c
d <- get bh
return $ IfaceUnivCo a b c d
9 -> do a <- get bh
return $ IfaceSymCo a
10-> do a <- get bh
......@@ -954,7 +956,7 @@ toIfaceCoercion (CoVarCo cv) = IfaceCoVarCo (toIfaceCoVar cv)
toIfaceCoercion (AxiomInstCo con ind cos)
= IfaceAxiomInstCo (coAxiomName con) ind
(map toIfaceCoercion cos)
toIfaceCoercion (UnivCo r ty1 ty2) = IfaceUnivCo r (toIfaceType ty1)
toIfaceCoercion (UnivCo s r ty1 ty2)= IfaceUnivCo s r (toIfaceType ty1)
(toIfaceType ty2)
toIfaceCoercion (SymCo co) = IfaceSymCo (toIfaceCoercion co)
toIfaceCoercion (TransCo co1 co2) = IfaceTransCo (toIfaceCoercion co1)
......
......@@ -880,7 +880,7 @@ tcIfaceCo (IfaceCoVarCo n) = mkCoVarCo <$> tcIfaceCoVar n
tcIfaceCo (IfaceAxiomInstCo n i cs) = AxiomInstCo <$> tcIfaceCoAxiom n
<*> pure i
<*> mapM tcIfaceCo cs
tcIfaceCo (IfaceUnivCo r t1 t2) = UnivCo r <$> tcIfaceType t1
tcIfaceCo (IfaceUnivCo s r t1 t2) = UnivCo s r <$> tcIfaceType t1
<*> tcIfaceType t2
tcIfaceCo (IfaceSymCo c) = SymCo <$> tcIfaceCo c
tcIfaceCo (IfaceTransCo c1 c2) = TransCo <$> tcIfaceCo c1
......
......@@ -1427,8 +1427,8 @@ zonkCoToCo env co
go (TyConAppCo r tc args) = mkTyConAppCo r tc <$> mapM go args
go (AppCo co arg) = mkAppCo <$> go co <*> go arg
go (AxiomInstCo ax ind args) = AxiomInstCo ax ind <$> mapM go args
go (UnivCo r ty1 ty2) = mkUnivCo r <$> zonkTcTypeToType env ty1
<*> zonkTcTypeToType env ty2
go (UnivCo s r ty1 ty2) = mkUnivCo s r <$> zonkTcTypeToType env ty1
<*> zonkTcTypeToType env ty2
go (SymCo co) = mkSymCo <$> go co
go (TransCo co1 co2) = mkTransCo <$> go co1 <*> go co2
go (NthCo n co) = mkNthCo n <$> go co
......
......@@ -1496,7 +1496,7 @@ orphNamesOfCo (AppCo co1 co2) = orphNamesOfCo co1 `unionNameSet` orphNames
orphNamesOfCo (ForAllCo _ co) = orphNamesOfCo co
orphNamesOfCo (CoVarCo _) = emptyNameSet
orphNamesOfCo (AxiomInstCo con _ cos) = orphNamesOfCoCon con `unionNameSet` orphNamesOfCos cos
orphNamesOfCo (UnivCo _ ty1 ty2) = orphNamesOfType ty1 `unionNameSet` orphNamesOfType ty2
orphNamesOfCo (UnivCo _ _ ty1 ty2) = orphNamesOfType ty1 `unionNameSet` orphNamesOfType ty2
orphNamesOfCo (SymCo co) = orphNamesOfCo co
orphNamesOfCo (TransCo co1 co2) = orphNamesOfCo co1 `unionNameSet` orphNamesOfCo co2
orphNamesOfCo (NthCo _ co) = orphNamesOfCo co
......
......@@ -177,7 +177,8 @@ data Coercion
-- See [Coercion axioms applied to coercions]
-- see Note [UnivCo]
| UnivCo Role Type Type -- :: "e" -> _ -> _ -> e
| UnivCo FastString Role Type Type -- :: "e" -> _ -> _ -> e
-- the FastString is just a note for provenance
| SymCo Coercion -- :: e -> e
| TransCo Coercion Coercion -- :: e -> e -> e
......@@ -524,7 +525,7 @@ tyCoVarsOfCo (AppCo co1 co2) = tyCoVarsOfCo co1 `unionVarSet` tyCoVarsOfCo
tyCoVarsOfCo (ForAllCo tv co) = tyCoVarsOfCo co `delVarSet` tv
tyCoVarsOfCo (CoVarCo v) = unitVarSet v
tyCoVarsOfCo (AxiomInstCo _ _ cos) = tyCoVarsOfCos cos
tyCoVarsOfCo (UnivCo _ ty1 ty2) = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2
tyCoVarsOfCo (UnivCo _ _ ty1 ty2) = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2
tyCoVarsOfCo (SymCo co) = tyCoVarsOfCo co
tyCoVarsOfCo (TransCo co1 co2) = tyCoVarsOfCo co1 `unionVarSet` tyCoVarsOfCo co2
tyCoVarsOfCo (NthCo _ co) = tyCoVarsOfCo co
......@@ -544,7 +545,7 @@ coVarsOfCo (AppCo co1 co2) = coVarsOfCo co1 `unionVarSet` coVarsOfCo co2
coVarsOfCo (ForAllCo _ co) = coVarsOfCo co
coVarsOfCo (CoVarCo v) = unitVarSet v
coVarsOfCo (AxiomInstCo _ _ cos) = coVarsOfCos cos
coVarsOfCo (UnivCo _ _ _) = emptyVarSet
coVarsOfCo (UnivCo _ _ _ _) = emptyVarSet
coVarsOfCo (SymCo co) = coVarsOfCo co
coVarsOfCo (TransCo co1 co2) = coVarsOfCo co1 `unionVarSet` coVarsOfCo co2
coVarsOfCo (NthCo _ co) = coVarsOfCo co
......@@ -563,7 +564,7 @@ coercionSize (AppCo co1 co2) = coercionSize co1 + coercionSize co2
coercionSize (ForAllCo _ co) = 1 + coercionSize co
coercionSize (CoVarCo _) = 1
coercionSize (AxiomInstCo _ _ cos) = 1 + sum (map coercionSize cos)
coercionSize (UnivCo _ ty1 ty2) = typeSize ty1 + typeSize ty2
coercionSize (UnivCo _ _ ty1 ty2) = typeSize ty1 + typeSize ty2
coercionSize (SymCo co) = 1 + coercionSize co
coercionSize (TransCo co1 co2) = 1 + coercionSize co1 + coercionSize co2
coercionSize (NthCo _ co) = 1 + coercionSize co
......@@ -597,7 +598,7 @@ tidyCo env@(_, subst) co
Just cv' -> CoVarCo cv'
go (AxiomInstCo con ind cos) = let args = tidyCos env cos
in args `seqList` AxiomInstCo con ind args
go (UnivCo r ty1 ty2) = (UnivCo r $! tidyType env ty1) $! tidyType env ty2
go (UnivCo s r ty1 ty2) = (UnivCo s r $! tidyType env ty1) $! tidyType env ty2
go (SymCo co) = SymCo $! go co
go (TransCo co1 co2) = (TransCo $! go co1) $! go co2
go (NthCo d co) = NthCo d $! go co
......@@ -658,7 +659,7 @@ ppr_co p co@(TransCo {}) = maybeParen p FunPrec $
ppr_co p (InstCo co ty) = maybeParen p TyConPrec $
pprParendCo co <> ptext (sLit "@") <> pprType ty
ppr_co p (UnivCo r ty1 ty2) = pprPrefixApp p (ptext (sLit "UnivCo") <+> ppr r)
ppr_co p (UnivCo s r ty1 ty2) = pprPrefixApp p (ptext (sLit "UnivCo") <+> ftext s <+> ppr r)
[pprParendType ty1, pprParendType ty2]
ppr_co p (SymCo co) = pprPrefixApp p (ptext (sLit "Sym")) [pprParendCo co]
ppr_co p (NthCo n co) = pprPrefixApp p (ptext (sLit "Nth:") <> int n) [pprParendCo co]
......@@ -1008,7 +1009,7 @@ mkSymCo :: Coercion -> Coercion
-- Do a few simple optimizations, but don't bother pushing occurrences
-- of symmetry to the leaves; the optimizer will take care of that.
mkSymCo co@(Refl {}) = co
mkSymCo (UnivCo r ty1 ty2) = UnivCo r ty2 ty1
mkSymCo (UnivCo s r ty1 ty2) = UnivCo s r ty2 ty1
mkSymCo (SymCo co) = co
mkSymCo co = SymCo co
......@@ -1056,12 +1057,12 @@ mkInstCo co ty = InstCo co ty
-- @unsafeCoerce#@ primitive. Optimise by pushing
-- down through type constructors.
mkUnsafeCo :: Type -> Type -> Coercion
mkUnsafeCo = mkUnivCo Representational
mkUnsafeCo = mkUnivCo (fsLit "mkUnsafeCo") Representational
mkUnivCo :: Role -> Type -> Type -> Coercion
mkUnivCo role ty1 ty2
mkUnivCo :: FastString -> Role -> Type -> Type -> Coercion
mkUnivCo prov role ty1 ty2
| ty1 `eqType` ty2 = Refl role ty1
| otherwise = UnivCo role ty1 ty2
| otherwise = UnivCo prov role ty1 ty2
mkAxiomRuleCo :: CoAxiomRule -> [Type] -> [Coercion] -> Coercion
mkAxiomRuleCo = AxiomRuleCo
......@@ -1071,7 +1072,7 @@ mkSubCo :: Coercion -> Coercion
mkSubCo (Refl Nominal ty) = Refl Representational ty
mkSubCo (TyConAppCo Nominal tc cos)
= TyConAppCo Representational tc (applyRoles tc cos)
mkSubCo (UnivCo Nominal ty1 ty2) = UnivCo Representational ty1 ty2
mkSubCo (UnivCo s Nominal ty1 ty2) = UnivCo s Representational ty1 ty2
mkSubCo co = ASSERT2( coercionRole co == Nominal, ppr co <+> ppr (coercionRole co) )
SubCo co
......@@ -1106,7 +1107,7 @@ setNominalRole_maybe (Refl _ ty) = Just $ Refl Nominal ty
setNominalRole_maybe (TyConAppCo Representational tc coes)
= do { cos' <- mapM setNominalRole_maybe coes
; return $ TyConAppCo Nominal tc cos' }
setNominalRole_maybe (UnivCo Representational ty1 ty2) = Just $ UnivCo Nominal ty1 ty2
setNominalRole_maybe (UnivCo s Representational ty1 ty2) = Just $ UnivCo s Nominal ty1 ty2
-- We do *not* promote UnivCo Phantom, as that's unsafe.
-- UnivCo Nominal is no more unsafe than UnivCo Representational
setNominalRole_maybe (TransCo co1 co2)
......@@ -1125,7 +1126,7 @@ setNominalRole_maybe _ = Nothing
mkPhantomCo :: Coercion -> Coercion
mkPhantomCo co
| Just ty <- isReflCo_maybe co = Refl Phantom ty
| Pair ty1 ty2 <- coercionKind co = UnivCo Phantom ty1 ty2
| Pair ty1 ty2 <- coercionKind co = UnivCo (fsLit "mkPhantomCo") Phantom ty1 ty2
-- don't optimise here... wait for OptCoercion
-- All input coercions are assumed to be Nominal,
......@@ -1355,7 +1356,8 @@ coreEqCoercion2 env (AxiomInstCo con1 ind1 cos1) (AxiomInstCo con2 ind2 cos2)
&& ind1 == ind2
&& all2 (coreEqCoercion2 env) cos1 cos2
coreEqCoercion2 env (UnivCo r1 ty11 ty12) (UnivCo r2 ty21 ty22)
-- the provenance string is just a note, so don't use in comparisons
coreEqCoercion2 env (UnivCo _ r1 ty11 ty12) (UnivCo _ r2 ty21 ty22)
= r1 == r2 && eqTypeX env ty11 ty21 && eqTypeX env ty12 ty22
coreEqCoercion2 env (SymCo co1) (SymCo co2)
......@@ -1517,7 +1519,7 @@ subst_co subst co
ForAllCo tv' $! subst_co subst' co
go (CoVarCo cv) = substCoVar subst cv
go (AxiomInstCo con ind cos) = AxiomInstCo con ind $! map go cos
go (UnivCo r ty1 ty2) = (UnivCo r $! go_ty ty1) $! go_ty ty2
go (UnivCo s r ty1 ty2) = (UnivCo s r $! go_ty ty1) $! go_ty ty2
go (SymCo co) = mkSymCo (go co)
go (TransCo co1 co2) = mkTransCo (go co1) (go co2)
go (NthCo d co) = mkNthCo d (go co)
......@@ -1646,7 +1648,8 @@ ty_co_subst subst role ty
go role ty@(LitTy {}) = ASSERT( role == Nominal )
mkReflCo role ty
lift_phantom ty = mkUnivCo Phantom (liftCoSubstLeft subst ty)
lift_phantom ty = mkUnivCo (fsLit "lift_phantom")
Phantom (liftCoSubstLeft subst ty)
(liftCoSubstRight subst ty)
{-
......@@ -1817,7 +1820,7 @@ seqCo (AppCo co1 co2) = seqCo co1 `seq` seqCo co2
seqCo (ForAllCo tv co) = tv `seq` seqCo co
seqCo (CoVarCo cv) = cv `seq` ()
seqCo (AxiomInstCo con ind cos) = con `seq` ind `seq` seqCos cos
seqCo (UnivCo r ty1 ty2) = r `seq` seqType ty1 `seq` seqType ty2
seqCo (UnivCo s r ty1 ty2) = s `seq` r `seq` seqType ty1 `seq` seqType ty2
seqCo (SymCo co) = seqCo co
seqCo (TransCo co1 co2) = seqCo co1 `seq` seqCo co2
seqCo (NthCo _ co) = seqCo co
......@@ -1877,7 +1880,7 @@ coercionKind co = go co
-- exactly saturate the axiom branch
Pair (substTyWith tvs tys1 (mkTyConApp (coAxiomTyCon ax) lhs))
(substTyWith tvs tys2 rhs)
go (UnivCo _ ty1 ty2) = Pair ty1 ty2
go (UnivCo _ _ ty1 ty2) = Pair ty1 ty2
go (SymCo co) = swap $ go co
go (TransCo co1 co2) = Pair (pFst $ go co1) (pSnd $ go co2)
go (NthCo d co) = tyConAppArgN d <$> go co
......@@ -1915,7 +1918,7 @@ coercionKindRole = go
(mkForAllTy tv <$> tys, r)
go (CoVarCo cv) = (toPair $ coVarKind cv, coVarRole cv)
go co@(AxiomInstCo ax _ _) = (coercionKind co, coAxiomRole ax)
go (UnivCo r ty1 ty2) = (Pair ty1 ty2, r)
go (UnivCo _ r ty1 ty2) = (Pair ty1 ty2, r)
go (SymCo co) = first swap $ go co
go (TransCo co1 co2)
= let (tys1, r) = go co1 in
......
......@@ -199,9 +199,9 @@ opt_co4 env sym rep r (AxiomInstCo con ind cos)
cos)
-- Note that the_co does *not* have sym pushed into it
opt_co4 env sym rep r (UnivCo _r oty1 oty2)
opt_co4 env sym rep r (UnivCo s _r oty1 oty2)
= ASSERT( r == _r )
opt_univ env (chooseRole rep r) a b
opt_univ env s (chooseRole rep r) a b
where
(a,b) = if sym then (oty2,oty1) else (oty1,oty2)
......@@ -266,24 +266,24 @@ opt_co4 env sym rep r (AxiomRuleCo co ts cs)
opt_phantom :: CvSubst -> SymFlag -> Coercion -> NormalCo
opt_phantom env sym co
= if sym
then opt_univ env Phantom ty2 ty1
else opt_univ env Phantom ty1 ty2
then opt_univ env (fsLit "opt_phantom") Phantom ty2 ty1
else opt_univ env (fsLit "opt_phantom") Phantom ty1 ty2
where
Pair ty1 ty2 = coercionKind co
opt_univ :: CvSubst -> Role -> Type -> Type -> Coercion
opt_univ env role oty1 oty2
opt_univ :: CvSubst -> FastString -> Role -> Type -> Type -> Coercion
opt_univ env prov role oty1 oty2
| Just (tc1, tys1) <- splitTyConApp_maybe oty1
, Just (tc2, tys2) <- splitTyConApp_maybe oty2
, tc1 == tc2
= mkTyConAppCo role tc1 (zipWith3 (opt_univ env) (tyConRolesX role tc1) tys1 tys2)
= mkTyConAppCo role tc1 (zipWith3 (opt_univ env prov) (tyConRolesX role tc1) tys1 tys2)
| Just (l1, r1) <- splitAppTy_maybe oty1
, Just (l2, r2) <- splitAppTy_maybe oty2
, typeKind l1 `eqType` typeKind l2 -- kind(r1) == kind(r2) by consequence
= let role' = if role == Phantom then Phantom else Nominal in
-- role' is to comform to mkAppCo's precondition
mkAppCo (opt_univ env role l1 l2) (opt_univ env role' r1 r2)
mkAppCo (opt_univ env prov role l1 l2) (opt_univ env prov role' r1 r2)
| Just (tv1, ty1) <- splitForAllTy_maybe oty1
, Just (tv2, ty2) <- splitForAllTy_maybe oty2
......@@ -291,10 +291,10 @@ opt_univ env role oty1 oty2
= case substTyVarBndr2 env tv1 tv2 of { (env1, env2, tv') ->
let ty1' = substTy env1 ty1
ty2' = substTy env2 ty2 in
mkForAllCo tv' (opt_univ (zapCvSubstEnv2 env1 env2) role ty1' ty2') }
mkForAllCo tv' (opt_univ (zapCvSubstEnv2 env1 env2) prov role ty1' ty2') }
| otherwise
= mkUnivCo role (substTy env oty1) (substTy env oty2)
= mkUnivCo prov role (substTy env oty1) (substTy env oty2)
-------------
-- NthCo must be handled separately, because it's the one case where we can't
......
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