Commit bb2a446a authored by Richard Eisenberg's avatar Richard Eisenberg

Preserve CoVar uniques during pretty printing

Previously, we did this for Types, but not for Coercions.
parent ef39af72
......@@ -646,6 +646,7 @@ rnIfaceCo (IfaceAppCo co1 co2)
= IfaceAppCo <$> rnIfaceCo co1 <*> rnIfaceCo co2
rnIfaceCo (IfaceForAllCo bndr co1 co2)
= IfaceForAllCo <$> rnIfaceTvBndr bndr <*> rnIfaceCo co1 <*> rnIfaceCo co2
rnIfaceCo (IfaceFreeCoVar c) = pure (IfaceFreeCoVar c)
rnIfaceCo (IfaceCoVarCo lcl) = IfaceCoVarCo <$> pure lcl
rnIfaceCo (IfaceAxiomInstCo n i cs)
= IfaceAxiomInstCo <$> rnIfaceGlobal n <*> pure i <*> mapM rnIfaceCo cs
......
......@@ -1424,6 +1424,7 @@ freeNamesIfCoercion (IfaceAppCo c1 c2)
= freeNamesIfCoercion c1 &&& freeNamesIfCoercion c2
freeNamesIfCoercion (IfaceForAllCo _ kind_co co)
= freeNamesIfCoercion kind_co &&& freeNamesIfCoercion co
freeNamesIfCoercion (IfaceFreeCoVar _) = emptyNameSet
freeNamesIfCoercion (IfaceCoVarCo _)
= emptyNameSet
freeNamesIfCoercion (IfaceAxiomInstCo ax _ cos)
......
......@@ -109,7 +109,7 @@ data IfaceOneShot -- See Note [Preserve OneShotInfo] in CoreTicy
type IfaceKind = IfaceType
data IfaceType -- A kind of universal type, used for types and kinds
= IfaceFreeTyVar TyVar -- See Note [Free tyvars in IfaceType]
= IfaceFreeTyVar TyVar -- See Note [Free tyvars in IfaceType]
| IfaceTyVar IfLclName -- Type/coercion variable only, not tycon
| IfaceLitTy IfaceTyLit
| IfaceAppTy IfaceType IfaceType
......@@ -204,6 +204,7 @@ Note that:
to deserialise one. IfaceFreeTyVar is used only in the "convert to IfaceType
and then pretty-print" pipeline.
We do the same for covars, naturally.
Note [Equality predicates in IfaceType]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......@@ -242,6 +243,7 @@ data IfaceCoercion
| IfaceTyConAppCo Role IfaceTyCon [IfaceCoercion]
| IfaceAppCo IfaceCoercion IfaceCoercion
| IfaceForAllCo IfaceTvBndr IfaceCoercion IfaceCoercion
| IfaceFreeCoVar CoVar -- See Note [Free tyvars in IfaceType]
| IfaceCoVarCo IfLclName
| IfaceAxiomInstCo IfExtName BranchIndex [IfaceCoercion]
| IfaceUnivCo IfaceUnivCoProv Role IfaceType IfaceType
......@@ -395,6 +397,7 @@ substIfaceType env ty
go_co (IfaceTyConAppCo r tc cos) = IfaceTyConAppCo r tc (go_cos cos)
go_co (IfaceAppCo c1 c2) = IfaceAppCo (go_co c1) (go_co c2)
go_co (IfaceForAllCo {}) = pprPanic "substIfaceCoercion" (ppr ty)
go_co (IfaceFreeCoVar cv) = IfaceFreeCoVar cv
go_co (IfaceCoVarCo cv) = IfaceCoVarCo cv
go_co (IfaceAxiomInstCo a i cos) = IfaceAxiomInstCo a i (go_cos cos)
go_co (IfaceUnivCo prov r t1 t2) = IfaceUnivCo (go_prov prov) r (go t1) (go t2)
......@@ -1039,6 +1042,8 @@ ppr_co ctxt_prec co@(IfaceForAllCo {})
= let (tvs, co'') = split_co co' in ((name,kind_co):tvs,co'')
split_co co' = ([], co')
-- Why these two? See Note [TcTyVars in IfaceType]
ppr_co _ (IfaceFreeCoVar covar) = ppr covar
ppr_co _ (IfaceCoVarCo covar) = ppr covar
ppr_co ctxt_prec (IfaceUnivCo IfaceUnsafeCoerceProv r ty1 ty2)
......@@ -1321,6 +1326,8 @@ instance Binary IfaceCoercion where
put_ bh a
put_ bh b
put_ bh c
put_ _ (IfaceFreeCoVar cv)
= pprPanic "Can't serialise IfaceFreeCoVar" (ppr cv)
put_ bh (IfaceCoVarCo a) = do
putByte bh 6
put_ bh a
......
......@@ -1321,6 +1321,7 @@ tcIfaceCo = go
go (IfaceForAllCo tv k c) = do { k' <- go k
; bindIfaceTyVar tv $ \ tv' ->
ForAllCo tv' k' <$> go c }
go (IfaceFreeCoVar c) = pprPanic "tcIfaceCo:IfaceFreeCoVar" (ppr c)
go (IfaceCoVarCo n) = CoVarCo <$> go_var n
go (IfaceAxiomInstCo n i cs) = AxiomInstCo <$> tcIfaceCoAxiom n <*> pure i <*> mapM go cs
go (IfaceUnivCo p r t1 t2) = UnivCo <$> tcIfaceUnivCoProv p <*> pure r
......
......@@ -217,7 +217,10 @@ toIfaceCoercionX fr co
= go co
where
go (Refl r ty) = IfaceReflCo r (toIfaceType ty)
go (CoVarCo cv) = IfaceCoVarCo (toIfaceCoVar cv)
go (CoVarCo cv)
-- See [TcTyVars in IfaceType] in IfaceType
| cv `elemVarSet` fr = IfaceFreeCoVar cv
| otherwise = IfaceCoVarCo (toIfaceCoVar cv)
go (AppCo co1 co2) = IfaceAppCo (go co1) (go co2)
go (SymCo co) = IfaceSymCo (go co)
go (TransCo co1 co2) = IfaceTransCo (go co1) (go co2)
......@@ -236,8 +239,7 @@ toIfaceCoercionX fr co
| tc `hasKey` funTyConKey
, [_,_,_,_] <- cos = pprPanic "toIfaceCoercion" (ppr co)
| otherwise = IfaceTyConAppCo r (toIfaceTyCon tc) (map go cos)
go (FunCo r co1 co2) = IfaceFunCo r (toIfaceCoercion co1)
(toIfaceCoercion co2)
go (FunCo r co1 co2) = IfaceFunCo r (go co1) (go co2)
go (ForAllCo tv k co) = IfaceForAllCo (toIfaceTvBndr tv)
(toIfaceCoercionX fr' k)
......
......@@ -13,7 +13,7 @@ convert :: Wrap Age -> Int
[GblId, Arity=1, Caf=NoCafRefs]
convert
= convert1
`cast` (<Wrap Age>_R -> Roles13.N:Wrap[0] Roles13.N:Age[0]
`cast` (<Wrap Age>_R ->_R Roles13.N:Wrap[0] (Roles13.N:Age[0])
:: (Wrap Age -> Wrap Age :: *) ~R# (Wrap Age -> Int :: *))
-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
......
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