Fix bogus test in Lint

The Lint check for branch compatiblity within an axiom, in
GHC.Core.Lint.compatible_branches was subtly different to the
check made when contructing an axiom, in
GHC.Core.FamInstEnv.compatibleBranches.

The latter is correct, so I killed the former and am now using the
latter.

On the way I did some improvements to pretty-printing and documentation.

6 files changed, 66 insertions, 79 deletions

diff --git a/compiler/GHC/Core/Coercion.hs b/compiler/GHC/Core/Coercion.hs
index 71c2d075ed..c7ade006e5 100644
--- a/compiler/GHC/Core/Coercion.hs
+++ b/compiler/GHC/Core/Coercion.hs
@@ -219,8 +219,8 @@ etaExpandCoAxBranch (CoAxBranch { cab_tvs = tvs
 pprCoAxiom :: CoAxiom br -> SDoc
 -- Used in debug-printing only
 pprCoAxiom ax@(CoAxiom { co_ax_tc = tc, co_ax_branches = branches })
-  = hang (text "axiom" <+> ppr ax <+> dcolon)
-       2 (vcat (map (pprCoAxBranchUser tc) (fromBranches branches)))
+  = hang (text "axiom" <+> ppr ax)
+       2 (braces $ vcat (map (pprCoAxBranchUser tc) (fromBranches branches)))
 
 pprCoAxBranchUser :: TyCon -> CoAxBranch -> SDoc
 -- Used when printing injectivity errors (FamInst.reportInjectivityErrors)
@@ -254,8 +254,12 @@ ppr_co_ax_branch ppr_rhs fam_tc branch
     [ pprUserForAll (mkForAllTyBinders Inferred bndrs')
          -- See Note [Printing foralls in type family instances] in GHC.Iface.Type
     , pp_lhs <+> ppr_rhs tidy_env ee_rhs
-    , text "-- Defined" <+> pp_loc ]
+    , vcat [ text "-- Defined" <+> pp_loc
+           , ppUnless (null incomps) $ whenPprDebug $
+             text "-- Incomps:" <+> vcat (map (pprCoAxBranch fam_tc) incomps) ]
+    ]
   where
+    incomps = coAxBranchIncomps branch
     loc = coAxBranchSpan branch
     pp_loc | isGoodSrcSpan loc = text "at" <+> ppr (srcSpanStart loc)
            | otherwise         = text "in" <+> ppr loc
diff --git a/compiler/GHC/Core/Coercion/Axiom.hs b/compiler/GHC/Core/Coercion/Axiom.hs
index 409acea036..5e6b456081 100644
--- a/compiler/GHC/Core/Coercion/Axiom.hs
+++ b/compiler/GHC/Core/Coercion/Axiom.hs
@@ -39,7 +39,7 @@ import GHC.Prelude
 import Language.Haskell.Syntax.Basic (Role(..))
 
 import {-# SOURCE #-} GHC.Core.TyCo.Rep ( Type )
-import {-# SOURCE #-} GHC.Core.TyCo.Ppr ( pprType )
+import {-# SOURCE #-} GHC.Core.TyCo.Ppr ( pprType, pprTyVar )
 import {-# SOURCE #-} GHC.Core.TyCon    ( TyCon )
 import GHC.Utils.Outputable
 import GHC.Data.FastString
@@ -278,7 +278,6 @@ coAxiomArity ax index
   = length tvs + length cvs
   where
     CoAxBranch { cab_tvs = tvs, cab_cvs = cvs } = coAxiomNthBranch ax index
-
 coAxiomName :: CoAxiom br -> Name
 coAxiomName = co_ax_name
 
@@ -334,7 +333,7 @@ placeHolderIncomps = panic "placeHolderIncomps"
 Note [CoAxBranch type variables]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 In the case of a CoAxBranch of an associated type-family instance,
-we use the *same* type variables (where possible) as the
+we use the *same* type variables in cab_tvs (where possible) as the
 enclosing class or instance.  Consider
 
   instance C Int [z] where
@@ -344,8 +343,11 @@ In the CoAxBranch in the instance decl (F Int [z]) we use the
 same 'z', so that it's easy to check that that type is the same
 as that in the instance header.
 
-So, unlike FamInsts, there is no expectation that the cab_tvs
-are fresh wrt each other, or any other CoAxBranch.
+However, I believe that the cab_tvs of any CoAxBranch are distinct
+from the cab_tvs of other CoAxBranches in the same CoAxiom.  This is
+important when checking for compatiblity and apartness; e.g. see
+GHC.Core.FamInstEnv.compatibleBranches.  (The story seems a bit wobbly
+here, but it seems to work.)
 
 Note [CoAxBranch roles]
 ~~~~~~~~~~~~~~~~~~~~~~~
@@ -461,6 +463,12 @@ See also:
 * Note [RoughMap and rm_empty] for how this complicates the RoughMap implementation slightly.
 -}
 
+{- *********************************************************************
+*                                                                      *
+              Instances, especially pretty-printing
+*                                                                      *
+********************************************************************* -}
+
 instance Eq (CoAxiom br) where
     a == b = getUnique a == getUnique b
     a /= b = getUnique a /= getUnique b
@@ -468,9 +476,6 @@ instance Eq (CoAxiom br) where
 instance Uniquable (CoAxiom br) where
     getUnique = co_ax_unique
 
-instance Outputable (CoAxiom br) where
-    ppr = ppr . getName
-
 instance NamedThing (CoAxiom br) where
     getName = co_ax_name
 
@@ -480,13 +485,22 @@ instance Typeable br => Data.Data (CoAxiom br) where
     gunfold _ _  = error "gunfold"
     dataTypeOf _ = mkNoRepType "CoAxiom"
 
+instance Outputable (CoAxiom br) where
+  -- You may want GHC.Core.Coercion.pprCoAxiom instead
+  ppr = ppr . getName
+
 instance Outputable CoAxBranch where
-  ppr (CoAxBranch { cab_loc = loc
-                  , cab_lhs = lhs
-                  , cab_rhs = rhs }) =
-    text "CoAxBranch" <+> parens (ppr loc) <> colon
-      <+> brackets (pprWithCommas pprType lhs)
-      <+> text "=>" <+> pprType rhs
+  -- This instance doesn't know the name of the type family
+  -- If possible, use GHC.Core.Coercion.pprCoAxBranch instead
+  ppr (CoAxBranch { cab_tvs = tvs, cab_cvs = cvs
+                  , cab_lhs = lhs_tys, cab_rhs = rhs, cab_incomps = incomps })
+    = text "CoAxBranch" <+> braces payload
+    where
+      payload = hang (text "forall" <+> pprWithCommas pprTyVar (tvs ++ cvs) <> dot)
+                   2 (vcat [ text "<tycon>" <+> sep (map pprType lhs_tys)
+                           , nest 2 (text "=" <+> ppr rhs)
+                           , ppUnless (null incomps) $
+                             text "incomps:" <+> vcat (map ppr incomps) ])
 
 {-
 ************************************************************************
diff --git a/compiler/GHC/Core/FamInstEnv.hs b/compiler/GHC/Core/FamInstEnv.hs
index 31d01d3893..121c8ffe10 100644
--- a/compiler/GHC/Core/FamInstEnv.hs
+++ b/compiler/GHC/Core/FamInstEnv.hs
@@ -24,7 +24,7 @@ module GHC.Core.FamInstEnv (
         FamInstMatch(..),
         lookupFamInstEnv, lookupFamInstEnvConflicts, lookupFamInstEnvByTyCon,
 
-        isDominatedBy, apartnessCheck,
+        isDominatedBy, apartnessCheck, compatibleBranches,
 
         -- Injectivity
         InjectivityCheckResult(..),
@@ -534,15 +534,16 @@ fails anyway.
 compatibleBranches :: CoAxBranch -> CoAxBranch -> Bool
 compatibleBranches (CoAxBranch { cab_lhs = lhs1, cab_rhs = rhs1 })
                    (CoAxBranch { cab_lhs = lhs2, cab_rhs = rhs2 })
-  = let (commonlhs1, commonlhs2) = zipAndUnzip lhs1 lhs2
-             -- See Note [Compatibility of eta-reduced axioms]
-    in case tcUnifyTysFG alwaysBindFun commonlhs1 commonlhs2 of
-      SurelyApart -> True
-      Unifiable subst
-        | Type.substTyAddInScope subst rhs1 `eqType`
-          Type.substTyAddInScope subst rhs2
-        -> True
-      _ -> False
+  = case tcUnifyTysFG alwaysBindFun commonlhs1 commonlhs2 of
+      -- Here we need the cab_tvs of the two branches to be disinct.
+      -- See Note [CoAxBranch type variables] in GHC.Core.Coercion.Axiom.
+      SurelyApart     -> True
+      MaybeApart {}   -> False
+      Unifiable subst -> Type.substTyAddInScope subst rhs1 `eqType`
+                         Type.substTyAddInScope subst rhs2
+  where
+     (commonlhs1, commonlhs2) = zipAndUnzip lhs1 lhs2
+     -- See Note [Compatibility of eta-reduced axioms]
 
 -- | Result of testing two type family equations for injectiviy.
 data InjectivityCheckResult
@@ -597,7 +598,7 @@ computeAxiomIncomps branches
   where
     go :: [CoAxBranch] -> CoAxBranch -> ([CoAxBranch], CoAxBranch)
     go prev_brs cur_br
-       = (cur_br : prev_brs, new_br)
+       = (new_br : prev_brs, new_br)
        where
          new_br = cur_br { cab_incomps = mk_incomps prev_brs cur_br }
 
diff --git a/compiler/GHC/Core/Lint.hs b/compiler/GHC/Core/Lint.hs
index f980371c26..73faebd80d 100644
--- a/compiler/GHC/Core/Lint.hs
+++ b/compiler/GHC/Core/Lint.hs
@@ -54,6 +54,7 @@ import GHC.Core.TyCo.FVs
 import GHC.Core.TyCo.Ppr
 import GHC.Core.TyCon as TyCon
 import GHC.Core.Coercion.Axiom
+import GHC.Core.FamInstEnv( compatibleBranches )
 import GHC.Core.Unify
 import GHC.Core.Coercion.Opt ( checkAxInstCo )
 import GHC.Core.Opt.Arity    ( typeArity, exprIsDeadEnd )
@@ -2640,8 +2641,10 @@ lint_family_branch fam_tc br@(CoAxBranch { cab_tvs     = tvs
        ; lintL (null cvs)
                (text "Coercion variables bound in family axiom")
        ; forM_ incomps $ \ br' ->
-           lintL (not (compatible_branches br br')) $
-           text "Incorrect incompatible branch:" <+> ppr br' }
+           lintL (not (compatibleBranches br br')) $
+           hang (text "Incorrect incompatible branches:")
+              2 (vcat [text "Branch:"       <+> ppr br,
+                       text "Bogus incomp:" <+> ppr br']) }
 
 lint_axiom_group :: NonEmpty (CoAxiom Branched) -> LintM ()
 lint_axiom_group (_  :| []) = return ()
@@ -2663,7 +2666,7 @@ lint_axiom_pair tc (ax1, ax2)
   , Just br2@(CoAxBranch { cab_tvs = tvs2
                          , cab_lhs = lhs2
                          , cab_rhs = rhs2 }) <- coAxiomSingleBranch_maybe ax2
-  = lintL (compatible_branches br1 br2) $
+  = lintL (compatibleBranches br1 br2) $
     vcat [ hsep [ text "Axioms", ppr ax1, text "and", ppr ax2
                 , text "are incompatible" ]
          , text "tvs1 =" <+> pprTyVars tvs1
@@ -2677,27 +2680,6 @@ lint_axiom_pair tc (ax1, ax2)
   = addErrL (text "Open type family axiom has more than one branch: either" <+>
              ppr ax1 <+> text "or" <+> ppr ax2)
 
-compatible_branches :: CoAxBranch -> CoAxBranch -> Bool
--- True <=> branches are compatible. See Note [Compatibility] in GHC.Core.FamInstEnv.
-compatible_branches (CoAxBranch { cab_tvs = tvs1
-                                , cab_lhs = lhs1
-                                , cab_rhs = rhs1 })
-                    (CoAxBranch { cab_tvs = tvs2
-                                , cab_lhs = lhs2
-                                , cab_rhs = rhs2 })
-  = -- we need to freshen ax2 w.r.t. ax1
-    -- do this by pretending tvs1 are in scope when processing tvs2
-    let in_scope       = mkInScopeSetList tvs1
-        subst0         = mkEmptySubst in_scope
-        (subst, _)     = substTyVarBndrs subst0 tvs2
-        lhs2'          = substTys subst lhs2
-        rhs2'          = substTy  subst rhs2
-    in
-    case tcUnifyTys alwaysBindFun lhs1 lhs2' of
-      Just unifying_subst -> substTy unifying_subst rhs1  `eqType`
-                             substTy unifying_subst rhs2'
-      Nothing             -> True
-
 {-
 ************************************************************************
 *                                                                      *
@@ -3325,33 +3307,8 @@ dumpLoc (InType ty)
 dumpLoc (InCo co)
   = (noSrcLoc, text "In the coercion" <+> quotes (ppr co))
 dumpLoc (InAxiom ax)
-  = (getSrcLoc ax_name, text "In the coercion axiom" <+> ppr ax_name <+> dcolon <+> pp_ax)
-  where
-    CoAxiom { co_ax_name     = ax_name
-            , co_ax_tc       = tc
-            , co_ax_role     = ax_role
-            , co_ax_branches = branches } = ax
-    branch_list = fromBranches branches
-
-    pp_ax
-      | [branch] <- branch_list
-      = pp_branch branch
-
-      | otherwise
-      = braces $ vcat (map pp_branch branch_list)
-
-    pp_branch (CoAxBranch { cab_tvs = tvs
-                          , cab_cvs = cvs
-                          , cab_lhs = lhs_tys
-                          , cab_rhs = rhs_ty })
-      = sep [ brackets (pprWithCommas pprTyVar (tvs ++ cvs)) <> dot
-            , ppr (mkTyConApp tc lhs_tys)
-            , text "~_" <> pp_role ax_role
-            , ppr rhs_ty ]
-
-    pp_role Nominal          = text "N"
-    pp_role Representational = text "R"
-    pp_role Phantom          = text "P"
+  = (getSrcLoc ax, hang (text "In the coercion axiom")
+                      2 (pprCoAxiom ax))
 
 pp_binders :: [Var] -> SDoc
 pp_binders bs = sep (punctuate comma (map pp_binder bs))
diff --git a/testsuite/tests/indexed-types/should_compile/T22547.hs b/testsuite/tests/indexed-types/should_compile/T22547.hs
new file mode 100644
index 0000000000..926f580adb
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T22547.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE TypeFamilies #-}
+module M where
+
+import Data.Kind (Type)
+
+data MP1 a = MP1 a
+
+type family Fixup (f :: Type) (g :: Type) :: Type where
+  Fixup f (MP1 f) = Int
+  Fixup f f = f
diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T
index 9fd26a660e..b65d9dc382 100644
--- a/testsuite/tests/indexed-types/should_compile/all.T
+++ b/testsuite/tests/indexed-types/should_compile/all.T
@@ -305,3 +305,4 @@ test('T14111', normal, compile, ['-O'])
 test('T19336', normal, compile, ['-O'])
 test('T11715b', normal, ghci_script, ['T11715b.script'])
 test('T4254', normal, compile, [''])
+test('T22547', normal, compile, [''])