Fix bogus test in Lintwip/T22547

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.

1 files changed, 12 insertions, 11 deletions

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 }