Add a -fprint-axiom-incomps option (#15546)wip/D5097

Supply branch incomps when building an IfaceClosedSynFamilyTyCon

`pprTyThing` now has access to incomps. This also causes them to be
written out to .hi files, but that doesn't pose an issue other than a
more faithful bijection between `tyThingToIfaceDecl` and `tcIfaceDecl`.

The machinery for displaying axiom incomps was already present but not
in use. Since this is now a thing that pops up in ghci's :info the
format was modified to look like a haskell comment.

Documentation and a test for the new feature included.

Test Plan: T15546

Reviewers: simonpj, bgamari, goldfire

Reviewed By: simonpj

Subscribers: rwbarton, carter

GHC Trac Issues: #15546

Differential Revision: https://phabricator.haskell.org/D5097

8 files changed, 103 insertions, 25 deletions

diff --git a/compiler/iface/IfaceSyn.hs b/compiler/iface/IfaceSyn.hs
index 05f64dff5a..dac3270482 100644
--- a/compiler/iface/IfaceSyn.hs
+++ b/compiler/iface/IfaceSyn.hs
@@ -47,6 +47,7 @@ import IfaceType
 import BinFingerprint
 import CoreSyn( IsOrphan, isOrphan )
 import PprCore()            -- Printing DFunArgs
+import DynFlags( gopt, GeneralFlag (Opt_PrintAxiomIncomps) )
 import Demand
 import Class
 import FieldLabel
@@ -66,7 +67,7 @@ import Binary
 import BooleanFormula ( BooleanFormula, pprBooleanFormula, isTrue )
 import Var( VarBndr(..), binderVar )
 import TyCon ( Role (..), Injectivity(..), tyConBndrVisArgFlag )
-import Util( dropList, filterByList )
+import Util( dropList, filterByList, notNull )
 import DataCon (SrcStrictness(..), SrcUnpackedness(..))
 import Lexeme (isLexSym)
 
@@ -545,6 +546,28 @@ to cross the separate compilation boundary.
 In general we retain all info that is left by CoreTidy.tidyLetBndr, since
 that is what is seen by importing module with --make
 
+Note [Displaying axiom incompatibilities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+With -fprint-axiom-incomps we display which closed type family equations
+are incompatible with which. This information is sometimes necessary
+because GHC doesn't try equations in order: any equation can be used when
+all preceding equations that are incompatible with it do not apply.
+
+For example, the last "a && a = a" equation in Data.Type.Bool.&& is
+actually compatible with all previous equations, and can reduce at any
+time.
+
+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
+The comment after an equation refers to all previous equations (0-indexed)
+that are incompatible with it.
 
 ************************************************************************
 *                                                                      *
@@ -571,13 +594,17 @@ pprAxBranch pp_tc (IfaceAxBranch { ifaxbTyVars = tvs
   = WARN( not (null _cvs), pp_tc $$ ppr _cvs )
     hang ppr_binders 2 (hang pp_lhs 2 (equals <+> ppr rhs))
     $+$
-    nest 2 maybe_incomps
+    nest 6 maybe_incomps
   where
     -- See Note [Printing foralls in type family instances] in IfaceType
     ppr_binders = pprUserIfaceForAll $ map (mkIfaceForAllTvBndr Specified) tvs
     pp_lhs = hang pp_tc 2 (pprParendIfaceAppArgs pat_tys)
-    maybe_incomps = ppUnless (null incomps) $ parens $
-                    text "incompatible indices:" <+> ppr incomps
+
+    -- See Note [Displaying axiom incompatibilities]
+    maybe_incomps
+      = sdocWithDynFlags $ \dflags ->
+        ppWhen (gopt Opt_PrintAxiomIncomps dflags && notNull incomps) $
+        text "--" <+> text "incompatible indices:" <+> interpp'SP incomps
 
 instance Outputable IfaceAnnotation where
   ppr (IfaceAnnotation target value) = ppr target <+> colon <+> ppr value
diff --git a/compiler/iface/MkIface.hs b/compiler/iface/MkIface.hs
index 1ea608e787..cd1ee33ed2 100644
--- a/compiler/iface/MkIface.hs
+++ b/compiler/iface/MkIface.hs
@@ -1722,33 +1722,30 @@ coAxiomToIfaceDecl ax@(CoAxiom { co_ax_tc = tycon, co_ax_branches = branches
  where
    branch_list = fromBranches branches
 
--- 2nd parameter is the list of branch LHSs, for conversion from incompatible branches
--- to incompatible indices
+-- 2nd parameter is the list of branch LHSs, in case of a closed type family,
+-- for conversion from incompatible branches to incompatible indices.
+-- For an open type family the list should be empty.
 -- See Note [Storing compatibility] in CoAxiom
 coAxBranchToIfaceBranch :: TyCon -> [[Type]] -> CoAxBranch -> IfaceAxBranch
 coAxBranchToIfaceBranch tc lhs_s
-                        branch@(CoAxBranch { cab_incomps = incomps })
-  = (coAxBranchToIfaceBranch' tc branch) { ifaxbIncomps = iface_incomps }
+                        (CoAxBranch { cab_tvs = tvs, cab_cvs = cvs
+                                    , cab_eta_tvs = eta_tvs
+                                    , cab_lhs = lhs, cab_roles = roles
+                                    , cab_rhs = rhs, cab_incomps = incomps })
+
+  = IfaceAxBranch { ifaxbTyVars  = toIfaceTvBndrs tidy_tvs
+                  , ifaxbCoVars  = map toIfaceIdBndr cvs
+                  , ifaxbEtaTyVars = toIfaceTvBndrs eta_tvs
+                  , ifaxbLHS     = toIfaceTcArgs tc lhs
+                  , ifaxbRoles   = roles
+                  , ifaxbRHS     = toIfaceType rhs
+                  , ifaxbIncomps = iface_incomps }
   where
     iface_incomps = map (expectJust "iface_incomps"
-                        . (flip findIndex lhs_s
-                          . eqTypes)
+                        . flip findIndex lhs_s
+                        . eqTypes
                         . coAxBranchLHS) incomps
 
--- use this one for standalone branches without incompatibles
-coAxBranchToIfaceBranch' :: TyCon -> CoAxBranch -> IfaceAxBranch
-coAxBranchToIfaceBranch' tc (CoAxBranch { cab_tvs = tvs, cab_cvs = cvs
-                                        , cab_eta_tvs = eta_tvs
-                                        , cab_lhs = lhs
-                                        , cab_roles = roles, cab_rhs = rhs })
-  = IfaceAxBranch { ifaxbTyVars    = toIfaceTvBndrs tvs
-                  , ifaxbCoVars    = map toIfaceIdBndr cvs
-                  , ifaxbEtaTyVars = toIfaceTvBndrs eta_tvs
-                  , ifaxbLHS       = toIfaceTcArgs tc lhs
-                  , ifaxbRoles     = roles
-                  , ifaxbRHS       = toIfaceType rhs
-                  , ifaxbIncomps   = [] }
-
 -----------------
 tyConToIfaceDecl :: TidyEnv -> TyCon -> (TidyEnv, IfaceDecl)
 -- We *do* tidy TyCons, because they are not (and cannot
@@ -1829,7 +1826,8 @@ tyConToIfaceDecl env tycon
     to_if_fam_flav (ClosedSynFamilyTyCon (Just ax))
       = IfaceClosedSynFamilyTyCon (Just (axn, ibr))
       where defs = fromBranches $ coAxiomBranches ax
-            ibr  = map (coAxBranchToIfaceBranch' tycon) defs
+            lhss = map coAxBranchLHS defs
+            ibr  = map (coAxBranchToIfaceBranch tycon lhss) defs
             axn  = coAxiomName ax
 
     ifaceConDecls (NewTyCon { data_con = con })    = IfNewTyCon  (ifaceConDecl con)
diff --git a/compiler/main/DynFlags.hs b/compiler/main/DynFlags.hs
index b3cfa4860e..dc5f22f85f 100644
--- a/compiler/main/DynFlags.hs
+++ b/compiler/main/DynFlags.hs
@@ -446,6 +446,7 @@ data GeneralFlag
    | Opt_PrintExplicitCoercions
    | Opt_PrintExplicitRuntimeReps
    | Opt_PrintEqualityRelations
+   | Opt_PrintAxiomIncomps
    | Opt_PrintUnicodeSyntax
    | Opt_PrintExpandedSynonyms
    | Opt_PrintPotentialInstances
@@ -4168,6 +4169,7 @@ fFlagsDeps = [
   flagSpec "print-explicit-coercions"         Opt_PrintExplicitCoercions,
   flagSpec "print-explicit-runtime-reps"      Opt_PrintExplicitRuntimeReps,
   flagSpec "print-equality-relations"         Opt_PrintEqualityRelations,
+  flagSpec "print-axiom-incomps"              Opt_PrintAxiomIncomps,
   flagSpec "print-unicode-syntax"             Opt_PrintUnicodeSyntax,
   flagSpec "print-expanded-synonyms"          Opt_PrintExpandedSynonyms,
   flagSpec "print-potential-instances"        Opt_PrintPotentialInstances,
diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst
index 67be116ae4..55562f863c 100644
--- a/docs/users_guide/glasgow_exts.rst
+++ b/docs/users_guide/glasgow_exts.rst
@@ -7921,6 +7921,9 @@ other hand, the two equations are compatible. Thus, GHC can ignore the
 first equation when looking at the second. So, ``G a`` will simplify to
 ``a``.
 
+Incompatibilities between closed type family equations can be displayed
+in :ghci-cmd:`:info` when :ghc-flag:`-fprint-axiom-incomps` is enabled.
+
 However see :ref:`ghci-decls` for the overlap rules in GHCi.
 
 .. _type-family-decidability:
diff --git a/docs/users_guide/using.rst b/docs/users_guide/using.rst
index d11dedfb9a..b9dc114ae0 100644
--- a/docs/users_guide/using.rst
+++ b/docs/users_guide/using.rst
@@ -842,6 +842,37 @@ messages and in GHCi:
     kinds, GHC uses type-level coercions. Users will rarely need to
     see these, as they are meant to be internal.
 
+.. ghc-flag:: -fprint-axiom-incomps
+    :shortdesc: Display equation incompatibilities in closed type families
+    :type: dynamic
+    :reverse: -fno-print-axiom-incomps
+    :category: verbosity
+
+    Using :ghc-flag:`-fprint-axiom-incomps` tells GHC to display
+    incompatibilities between closed type families' equations, whenever they
+    are printed by :ghci-cmd:`:info` or :ghc-flag:`--show-iface ⟨file⟩`.
+
+    .. code-block:: none
+
+        ghci> :i Data.Type.Equality.==
+        type family (==) (a :: k) (b :: k) :: Bool
+          where
+              (==) (f a) (g b) = (f == g) && (a == b)
+              (==) a a = 'True
+              (==) _1 _2 = 'False
+        ghci> :set -fprint-axiom-incomps
+        ghci> :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
+
+    The comment after each equation refers to the indices (0-indexed) of
+    preceding equations it is incompatible with.
+
 .. ghc-flag:: -fprint-equality-relations
     :shortdesc: Distinguish between equality relations when printing
     :type: dynamic
diff --git a/testsuite/tests/ghci/scripts/T15546.script b/testsuite/tests/ghci/scripts/T15546.script
new file mode 100644
index 0000000000..76bcda783e
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T15546.script
@@ -0,0 +1,5 @@
+:set -XTypeFamilies
+type family E a b where E a a = (); E a b = Bool
+:info E
+:set -fprint-axiom-incomps
+:info E
diff --git a/testsuite/tests/ghci/scripts/T15546.stdout b/testsuite/tests/ghci/scripts/T15546.stdout
new file mode 100644
index 0000000000..a5e8292ac3
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T15546.stdout
@@ -0,0 +1,11 @@
+type family E a b :: *
+  where
+      E a a = ()
+      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
+  	-- Defined at <interactive>:2:1
diff --git a/testsuite/tests/ghci/scripts/all.T b/testsuite/tests/ghci/scripts/all.T
index 946c6ef954..576357cb70 100755
--- a/testsuite/tests/ghci/scripts/all.T
+++ b/testsuite/tests/ghci/scripts/all.T
@@ -292,3 +292,4 @@ test('T16030', normal, ghci_script, ['T16030.script'])
 test('T11606', normal, ghci_script, ['T11606.script'])
 test('T16089', normal, ghci_script, ['T16089.script'])
 test('T14828', expect_broken(14828), ghci_script, ['T14828.script'])
+test('T15546', normal, ghci_script, ['T15546.script'])