Explicitly number equations when printing axiom incompatibilities

3 files changed, 32 insertions, 26 deletions

diff --git a/compiler/iface/IfaceSyn.hs b/compiler/iface/IfaceSyn.hs
index 7ed25b1927..3da0c63174 100644
--- a/compiler/iface/IfaceSyn.hs
+++ b/compiler/iface/IfaceSyn.hs
@@ -67,7 +67,7 @@ import Binary
 import BooleanFormula ( BooleanFormula, pprBooleanFormula, isTrue )
 import Var( VarBndr(..), binderVar )
 import TyCon ( Role (..), Injectivity(..), tyConBndrVisArgFlag )
-import Util( dropList, filterByList, notNull )
+import Util( dropList, filterByList, notNull, unzipWith )
 import DataCon (SrcStrictness(..), SrcUnpackedness(..))
 import Lexeme (isLexSym)
 
@@ -561,11 +561,11 @@ This is displayed as:
 Prelude> :i Data.Type.Equality.==
 type family (==) (a :: k) (b :: k) :: Bool
   where
-      (==) (f a) (g b) = (f == g) && (a == b)
-      (==) a a = 'True
-          -- incompatible indices: 0
-      (==) _1 _2 = 'False
-          -- incompatible indices: 1, 0
+    {- #0 -} (==) (f a) (g b) = (f == g) && (a == b)
+    {- #1 -} (==) a a = 'True
+          -- incompatible with: #0
+    {- #2 -} (==) _1 _2 = 'False
+          -- incompatible with: #1, #0
 The comment after an equation refers to all previous equations (0-indexed)
 that are incompatible with it.
 
@@ -576,7 +576,7 @@ that are incompatible with it.
 ************************************************************************
 -}
 
-pprAxBranch :: SDoc -> IfaceAxBranch -> SDoc
+pprAxBranch :: SDoc -> BranchIndex -> IfaceAxBranch -> SDoc
 -- The TyCon might be local (just an OccName), or this might
 -- be a branch for an imported TyCon, so it would be an ExtName
 -- So it's easier to take an SDoc here
@@ -586,25 +586,31 @@ pprAxBranch :: SDoc -> IfaceAxBranch -> SDoc
 --    in debug messages
 --    in :info F for GHCi, which goes via toConToIfaceDecl on the family tycon
 -- For user error messages we use Coercion.pprCoAxiom and friends
-pprAxBranch pp_tc (IfaceAxBranch { ifaxbTyVars = tvs
-                                 , ifaxbCoVars = _cvs
-                                 , ifaxbLHS = pat_tys
-                                 , ifaxbRHS = rhs
-                                 , ifaxbIncomps = incomps })
+pprAxBranch pp_tc idx (IfaceAxBranch { ifaxbTyVars = tvs
+                                     , ifaxbCoVars = _cvs
+                                     , ifaxbLHS = pat_tys
+                                     , ifaxbRHS = rhs
+                                     , ifaxbIncomps = incomps })
   = WARN( not (null _cvs), pp_tc $$ ppr _cvs )
     hang ppr_binders 2 (hang pp_lhs 2 (equals <+> ppr rhs))
     $+$
-    nest 6 maybe_incomps
+    nest 4 maybe_incomps
   where
     -- See Note [Printing foralls in type family instances] in IfaceType
-    ppr_binders = pprUserIfaceForAll $ map (mkIfaceForAllTvBndr Specified) tvs
+    ppr_binders = maybe_index <+>
+      pprUserIfaceForAll (map (mkIfaceForAllTvBndr Specified) tvs)
     pp_lhs = hang pp_tc 2 (pprParendIfaceAppArgs pat_tys)
 
     -- See Note [Displaying axiom incompatibilities]
+    maybe_index
+      = sdocWithDynFlags $ \dflags ->
+        ppWhen (gopt Opt_PrintAxiomIncomps dflags) $
+          text "{-" <+> (text "#" <> ppr idx) <+> text "-}"
     maybe_incomps
       = sdocWithDynFlags $ \dflags ->
         ppWhen (gopt Opt_PrintAxiomIncomps dflags && notNull incomps) $
-        text "--" <+> text "incompatible indices:" <+> interpp'SP incomps
+          text "--" <+> text "incompatible with:"
+          <+> pprWithCommas (\incomp -> text "#" <> ppr incomp) incomps
 
 instance Outputable IfaceAnnotation where
   ppr (IfaceAnnotation target value) = ppr target <+> colon <+> ppr value
@@ -887,11 +893,11 @@ pprIfaceDecl ss (IfaceFamily { ifName = tycon
       = ppShowIface ss (text "built-in")
 
     pp_branches (IfaceClosedSynFamilyTyCon (Just (ax, brs)))
-      = vcat (map (pprAxBranch
+      = vcat (unzipWith (pprAxBranch
                      (pprPrefixIfDeclBndr
                        (ss_how_much ss)
                        (occName tycon))
-                  ) brs)
+                  ) $ zip [0..] brs)
         $$ ppShowIface ss (text "axiom" <+> ppr ax)
     pp_branches _ = Outputable.empty
 
@@ -927,7 +933,7 @@ pprIfaceDecl ss (IfaceId { ifName = var, ifType = ty,
 pprIfaceDecl _ (IfaceAxiom { ifName = name, ifTyCon = tycon
                            , ifAxBranches = branches })
   = hang (text "axiom" <+> ppr name <+> dcolon)
-       2 (vcat $ map (pprAxBranch (ppr tycon)) branches)
+       2 (vcat $ unzipWith (pprAxBranch (ppr tycon)) $ zip [0..] branches)
 
 pprCType :: Maybe CType -> SDoc
 pprCType Nothing      = Outputable.empty
diff --git a/docs/users_guide/using.rst b/docs/users_guide/using.rst
index d2983c4b1a..1db30eab2e 100644
--- a/docs/users_guide/using.rst
+++ b/docs/users_guide/using.rst
@@ -843,14 +843,14 @@ messages and in GHCi:
         ghci> :i Data.Type.Equality.==
         type family (==) (a :: k) (b :: k) :: Bool
           where
-              (==) (f a) (g b) = (f == g) && (a == b)
-              (==) a a = 'True
+              {- #0 -} (==) (f a) (g b) = (f == g) && (a == b)
+              {- #1 -} (==) a a = 'True
                   -- incompatible indices: 0
-              (==) _1 _2 = 'False
+              {- #2 -} (==) _1 _2 = 'False
                   -- incompatible indices: 1, 0
 
-    The comment after each equation refers to the indices (0-indexed) of
-    preceding equations it is incompatible with.
+    The equations are numbered starting from 0, and the comment after each
+    equation refers to all preceding equations it is incompatible with.
 
 .. ghc-flag:: -fprint-equality-relations
     :shortdesc: Distinguish between equality relations when printing
diff --git a/testsuite/tests/ghci/scripts/T15546.stdout b/testsuite/tests/ghci/scripts/T15546.stdout
index dd4c41c20e..9892753fc0 100644
--- a/testsuite/tests/ghci/scripts/T15546.stdout
+++ b/testsuite/tests/ghci/scripts/T15546.stdout
@@ -3,7 +3,7 @@ type family E a b :: * where
     E a b = Bool
   	-- Defined at <interactive>:2:1
 type family E a b :: * where
-    E a a = ()
-    E a b = Bool
-        -- incompatible indices: 0
+  {- #0 -} E a a = ()
+  {- #1 -} E a b = Bool
+        -- incompatible with: #0
   	-- Defined at <interactive>:2:1