Remove old coercion pretty-printer

Now, all coercions are printed from IfaceType, just like types.

This also changes the rendering of TransCo to use ; instead of
a prefix operator.

8 files changed, 49 insertions, 114 deletions

diff --git a/compiler/iface/IfaceType.hs b/compiler/iface/IfaceType.hs
index 4ab40d4ac6..b1ad780782 100644
--- a/compiler/iface/IfaceType.hs
+++ b/compiler/iface/IfaceType.hs
@@ -1070,7 +1070,8 @@ ppr_co ctxt_prec (IfaceAxiomInstCo n i cos)
 ppr_co ctxt_prec (IfaceSymCo co)
   = ppr_special_co ctxt_prec (text "Sym") [co]
 ppr_co ctxt_prec (IfaceTransCo co1 co2)
-  = ppr_special_co ctxt_prec  (text "Trans") [co1,co2]
+  = maybeParen ctxt_prec TyOpPrec $
+    ppr_co TyOpPrec co1 <+> semi <+> ppr_co TyOpPrec co2
 ppr_co ctxt_prec (IfaceNthCo d co)
   = ppr_special_co ctxt_prec (text "Nth:" <> int d) [co]
 ppr_co ctxt_prec (IfaceLRCo lr co)
diff --git a/compiler/iface/ToIface.hs b/compiler/iface/ToIface.hs
index d4a2115025..f5cbe9e5c7 100644
--- a/compiler/iface/ToIface.hs
+++ b/compiler/iface/ToIface.hs
@@ -22,7 +22,7 @@ module ToIface
     , tidyToIfaceContext
     , tidyToIfaceTcArgs
       -- * Coercions
-    , toIfaceCoercion
+    , toIfaceCoercion, toIfaceCoercionX
       -- * Pattern synonyms
     , patSynToIfaceDecl
       -- * Expressions
@@ -216,7 +216,7 @@ toIfaceCoercionX :: VarSet -> Coercion -> IfaceCoercion
 toIfaceCoercionX fr co
   = go co
   where
-    go (Refl r ty)          = IfaceReflCo r (toIfaceType ty)
+    go (Refl r ty)          = IfaceReflCo r (toIfaceTypeX fr ty)
     go (CoVarCo cv)
       -- See [TcTyVars in IfaceType] in IfaceType
       | cv `elemVarSet` fr  = IfaceFreeCoVar cv
diff --git a/compiler/iface/ToIface.hs-boot b/compiler/iface/ToIface.hs-boot
index e2431b82dc..cdb472692e 100644
--- a/compiler/iface/ToIface.hs-boot
+++ b/compiler/iface/ToIface.hs-boot
@@ -13,4 +13,4 @@ toIfaceTyLit :: TyLit -> IfaceTyLit
 toIfaceForAllBndr :: TyVarBinder -> IfaceForAllBndr
 toIfaceTyCon :: TyCon -> IfaceTyCon
 toIfaceTcArgs :: TyCon -> [Type] -> IfaceTcArgs
-toIfaceCoercion :: Coercion -> IfaceCoercion
+toIfaceCoercionX :: VarSet -> Coercion -> IfaceCoercion
diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs
index 3f5036c4dd..b0b13b85ec 100644
--- a/compiler/types/Coercion.hs
+++ b/compiler/types/Coercion.hs
@@ -95,7 +95,7 @@ module Coercion (
         seqCo,
 
         -- * Pretty-printing
-        pprCo, pprParendCo, pprCoBndr,
+        pprCo, pprParendCo,
         pprCoAxiom, pprCoAxBranch, pprCoAxBranchHdr,
 
         -- * Tidying
@@ -152,117 +152,32 @@ setCoVarUnique = setVarUnique
 setCoVarName :: CoVar -> Name -> CoVar
 setCoVarName   = setVarName
 
-
 {-
 %************************************************************************
 %*                                                                      *
-                   Pretty-printing coercions
+                   Pretty-printing CoAxioms
 %*                                                                      *
 %************************************************************************
 
-@pprCo@ is the standard @Coercion@ printer; the overloaded @ppr@
-function is defined to use this.  @pprParendCo@ is the same, except it
-puts parens around the type, except for the atomic cases.
-@pprParendCo@ works just by setting the initial context precedence
-very high.
--}
-
--- Outputable instances are in TyCoRep, to avoid orphans
-
-pprCo, pprParendCo :: Coercion -> SDoc
-pprCo       co = ppr_co TopPrec   co
-pprParendCo co = ppr_co TyConPrec co
-
-ppr_co :: TyPrec -> Coercion -> SDoc
-ppr_co _ (Refl r ty) = angleBrackets (ppr ty) <> ppr_role r
-
-ppr_co _ (TyConAppCo r tc cos) = pprTcAppCo TyConPrec ppr_co tc cos <> ppr_role r
-ppr_co p (AppCo co arg)        = maybeParen p TyConPrec $
-                                 pprCo co <+> ppr_co TyConPrec arg
-ppr_co p co@(ForAllCo {})      = ppr_forall_co p co
-ppr_co p co@(FunCo {})         = ppr_fun_co p co
-ppr_co _ (CoVarCo cv)          = parenSymOcc (getOccName cv) (ppr cv)
-ppr_co p (AxiomInstCo con index args)
-  = pprPrefixApp p (ppr (getName con) <> brackets (ppr index))
-                   (map (ppr_co TyConPrec) args)
-
-ppr_co p co@(TransCo {}) = maybeParen p FunPrec $
-                           case trans_co_list co [] of
-                             [] -> panic "ppr_co"
-                             (co:cos) -> sep ( ppr_co FunPrec co
-                                             : [ char ';' <+> ppr_co FunPrec co | co <- cos])
-ppr_co p (InstCo co arg) = maybeParen p TyConPrec $
-                           pprParendCo co <> text "@" <> ppr_co TopPrec arg
-
-ppr_co p (UnivCo UnsafeCoerceProv r ty1 ty2)
-  = pprPrefixApp p (text "UnsafeCo" <+> ppr r)
-                   [pprParendType ty1, pprParendType ty2]
-ppr_co _ (UnivCo p r t1 t2)
-  = char 'U'
-    <> parens (ppr_prov <> comma <+> ppr t1 <> comma <+> ppr t2)
-    <> ppr_role r
-  where
-    ppr_prov = case p of
-      HoleProv h          -> text "hole:"   <> ppr h
-      PhantomProv kind_co -> text "phant:"  <> ppr kind_co
-      ProofIrrelProv co   -> text "irrel:"  <> ppr co
-      PluginProv s        -> text "plugin:" <> text s
-      UnsafeCoerceProv    -> text "unsafe"
-
-ppr_co p (SymCo co)          = pprPrefixApp p (text "Sym") [pprParendCo co]
-ppr_co p (NthCo n co)        = pprPrefixApp p (text "Nth:" <> int n) [pprParendCo co]
-ppr_co p (LRCo sel co)       = pprPrefixApp p (ppr sel) [pprParendCo co]
-ppr_co p (CoherenceCo c1 c2) = maybeParen p TyConPrec $
-                               (ppr_co FunPrec c1) <+> (text "|>") <+>
-                               (ppr_co FunPrec c2)
-ppr_co p (KindCo co)         = pprPrefixApp p (text "kind") [pprParendCo co]
-ppr_co p (SubCo co)         = pprPrefixApp p (text "Sub") [pprParendCo co]
-ppr_co p (AxiomRuleCo co cs) = maybeParen p TopPrec $ ppr_axiom_rule_co co cs
-
-ppr_axiom_rule_co :: CoAxiomRule -> [Coercion] -> SDoc
-ppr_axiom_rule_co co ps = ppr (coaxrName co) <+> parens (interpp'SP ps)
-
-ppr_role :: Role -> SDoc
-ppr_role r = underscore <> pp_role
-  where pp_role = case r of
-                    Nominal          -> char 'N'
-                    Representational -> char 'R'
-                    Phantom          -> char 'P'
-
-trans_co_list :: Coercion -> [Coercion] -> [Coercion]
-trans_co_list (TransCo co1 co2) cos = trans_co_list co1 (trans_co_list co2 cos)
-trans_co_list co                cos = co : cos
-
-ppr_fun_co :: TyPrec -> Coercion -> SDoc
-ppr_fun_co p co = pprArrowChain p (split co)
-  where
-    split :: Coercion -> [SDoc]
-    split (FunCo _ arg res)
-      = ppr_co FunPrec arg : split res
-    split co = [ppr_co TopPrec co]
+Defined here to avoid module loops. CoAxiom is loaded very early on.
 
-ppr_forall_co :: TyPrec -> Coercion -> SDoc
-ppr_forall_co p (ForAllCo tv h co)
-  = maybeParen p FunPrec $
-    sep [pprCoBndr (tyVarName tv) h, ppr_co TopPrec co]
-ppr_forall_co _ _ = panic "ppr_forall_co"
-
-pprCoBndr :: Name -> Coercion -> SDoc
-pprCoBndr name eta =
-  forAllLit <+> parens (ppr name <+> dcolon <+> ppr eta) <> dot
+-}
 
 pprCoAxiom :: CoAxiom br -> SDoc
 pprCoAxiom ax@(CoAxiom { co_ax_branches = branches })
   = hang (text "axiom" <+> ppr ax <+> dcolon)
-       2 (vcat (map (ppr_co_ax_branch (const ppr) ax) $ fromBranches branches))
+       2 (vcat (map (ppr_co_ax_branch (const pprType) ax) $ fromBranches branches))
 
 pprCoAxBranch :: CoAxiom br -> CoAxBranch -> SDoc
 pprCoAxBranch = ppr_co_ax_branch pprRhs
   where
-    pprRhs fam_tc (TyConApp tycon _)
-      | isDataFamilyTyCon fam_tc
+    pprRhs fam_tc rhs
+      | Just (tycon, _) <- splitTyConApp_maybe rhs
+      , isDataFamilyTyCon fam_tc
       = pprDataCons tycon
-    pprRhs _ rhs = ppr rhs
+
+      | otherwise
+      = ppr rhs
 
 pprCoAxBranchHdr :: CoAxiom br -> BranchIndex -> SDoc
 pprCoAxBranchHdr ax index = pprCoAxBranch ax (coAxiomNthBranch ax index)
diff --git a/compiler/types/Coercion.hs-boot b/compiler/types/Coercion.hs-boot
index dd10d6e5ca..d9aa234193 100644
--- a/compiler/types/Coercion.hs-boot
+++ b/compiler/types/Coercion.hs-boot
@@ -8,7 +8,6 @@ import {-# SOURCE #-} TyCon
 import BasicTypes ( LeftOrRight )
 import CoAxiom
 import Var
-import Outputable
 import Pair
 import Util
 
@@ -47,5 +46,3 @@ seqCo :: Coercion -> ()
 
 coercionKind :: Coercion -> Pair Type
 coercionType :: Coercion -> Type
-
-pprCo :: Coercion -> SDoc
diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
index 9b82ab80f9..ca3a4ad32b 100644
--- a/compiler/types/TyCoRep.hs
+++ b/compiler/types/TyCoRep.hs
@@ -62,10 +62,12 @@ module TyCoRep (
         pprTyVar, pprTyVars,
         pprThetaArrowTy, pprClassPred,
         pprKind, pprParendKind, pprTyLit,
-        TyPrec(..), maybeParen, pprTcAppCo,
+        TyPrec(..), maybeParen,
         pprPrefixApp, pprArrowChain,
         pprDataCons, ppSuggestExplicitKinds,
 
+        pprCo, pprParendCo,
+
         -- * Free variables
         tyCoVarsOfType, tyCoVarsOfTypeDSet, tyCoVarsOfTypes, tyCoVarsOfTypesDSet,
         tyCoFVsBndr, tyCoFVsOfType, tyCoVarsOfTypeList,
@@ -139,13 +141,14 @@ import {-# SOURCE #-} DataCon( dataConFullSig
 import {-# SOURCE #-} Type( isPredTy, isCoercionTy, mkAppTy, mkCastTy
                           , tyCoVarsOfTypeWellScoped
                           , tyCoVarsOfTypesWellScoped
+                          , toposortTyVars
                           , coreView, typeKind )
    -- Transitively pulls in a LOT of stuff, better to break the loop
 
 import {-# SOURCE #-} Coercion
 import {-# SOURCE #-} ConLike ( ConLike(..), conLikeName )
 import {-# SOURCE #-} ToIface( toIfaceTypeX, toIfaceTyLit, toIfaceForAllBndr
-                             , toIfaceTyCon, toIfaceTcArgs, toIfaceCoercion )
+                             , toIfaceTyCon, toIfaceTcArgs, toIfaceCoercionX )
 
 -- friends:
 import IfaceType
@@ -2473,6 +2476,29 @@ tidyToIfaceType ty = toIfaceTypeX (mkVarSet free_tcvs) (tidyType env ty)
     free_tcvs = tyCoVarsOfTypeWellScoped ty
 
 ------------
+pprCo, pprParendCo :: Coercion -> SDoc
+pprCo       co = getPprStyle $ \ sty -> pprIfaceCoercion (tidyToIfaceCoSty co sty)
+pprParendCo co = getPprStyle $ \ sty -> pprParendIfaceCoercion (tidyToIfaceCoSty co sty)
+
+tidyToIfaceCoSty :: Coercion -> PprStyle -> IfaceCoercion
+tidyToIfaceCoSty co sty
+  | userStyle sty = tidyToIfaceCo co
+  | otherwise     = toIfaceCoercionX (tyCoVarsOfCo co) co
+     -- in latter case, don't tidy, as we'll be printing uniques.
+
+tidyToIfaceCo :: Coercion -> IfaceCoercion
+-- It's vital to tidy before converting to an IfaceType
+-- or nested binders will become indistinguishable!
+--
+-- Also for the free type variables, tell toIfaceCoercionX to
+-- leave them as IfaceFreeCoVar.  This is super-important
+-- for debug printing.
+tidyToIfaceCo co = toIfaceCoercionX (mkVarSet free_tcvs) (tidyCo env co)
+  where
+    env       = tidyFreeTyCoVars emptyTidyEnv free_tcvs
+    free_tcvs = toposortTyVars $ tyCoVarsOfCoList co
+
+------------
 pprClassPred :: Class -> [Type] -> SDoc
 pprClassPred clas tys = pprTypeApp (classTyCon clas) tys
 
@@ -2596,11 +2622,6 @@ pprTypeApp tc tys
                             (toIfaceTcArgs tc tys)
     -- TODO: toIfaceTcArgs seems rather wasteful here
 
-pprTcAppCo :: TyPrec -> (TyPrec -> Coercion -> SDoc)
-           -> TyCon -> [Coercion] -> SDoc
-pprTcAppCo p _pp tc cos
-  = pprIfaceCoTcApp p (toIfaceTyCon tc) (map toIfaceCoercion cos)
-
 ------------------
 
 pprPrefixApp :: TyPrec -> SDoc -> [SDoc] -> SDoc
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index cea12abcde..c53fcc8e22 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -1828,7 +1828,7 @@ predTypeEqRel ty
 --
 -- This is a deterministic sorting operation
 -- (that is, doesn't depend on Uniques).
-toposortTyVars :: [TyVar] -> [TyVar]
+toposortTyVars :: [TyCoVar] -> [TyCoVar]
 toposortTyVars tvs = reverse $
                      [ node_payload node | node <- topologicalSortG $
                                           graphFromEdgedVerticesOrd nodes ]
diff --git a/compiler/types/Type.hs-boot b/compiler/types/Type.hs-boot
index 2fc251acb7..41486ddc37 100644
--- a/compiler/types/Type.hs-boot
+++ b/compiler/types/Type.hs-boot
@@ -2,7 +2,7 @@
 
 module Type where
 import TyCon
-import Var ( TyVar )
+import Var ( TyCoVar )
 import {-# SOURCE #-} TyCoRep( Type, Coercion, Kind )
 import Util
 
@@ -21,6 +21,7 @@ partitionInvisibles :: TyCon -> (a -> Type) -> [a] -> ([a], [a])
 coreView :: Type -> Maybe Type
 tcView :: Type -> Maybe Type
 
-tyCoVarsOfTypesWellScoped :: [Type] -> [TyVar]
-tyCoVarsOfTypeWellScoped :: Type -> [TyVar]
+tyCoVarsOfTypesWellScoped :: [Type] -> [TyCoVar]
+tyCoVarsOfTypeWellScoped :: Type -> [TyCoVar]
+toposortTyVars :: [TyCoVar] -> [TyCoVar]
 splitTyConApp_maybe :: HasDebugCallStack => Type -> Maybe (TyCon, [Type])