Move eta-reduced coaxiom compatibility handling quirks into FamInstEnv.

The quirk caused an issue where GHC concluded that 'D' is possibly
unifiable with 'D a' (the two types could have the same kind if D is a
data family).

Test Plan:
Ensure T9371 stays fixed.
Introduce T15704

Reviewers: goldfire, bgamari

Reviewed By: goldfire

Subscribers: RyanGlScott, rwbarton, carter

GHC Trac Issues: #15704

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

3 files changed, 42 insertions, 23 deletions

diff --git a/compiler/types/FamInstEnv.hs b/compiler/types/FamInstEnv.hs
index a5cfba1afb..d149dbf1d0 100644
--- a/compiler/types/FamInstEnv.hs
+++ b/compiler/types/FamInstEnv.hs
@@ -551,13 +551,42 @@ find a branch that matches the target, but then we make sure that the target
 is apart from every previous *incompatible* branch. We don't check the
 branches that are compatible with the matching branch, because they are either
 irrelevant (clause 1 of compatible) or benign (clause 2 of compatible).
+
+Note [Compatibility of eta-reduced axioms]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In newtype instances of data families we eta-reduce the axioms,
+See Note [Eta reduction for data family axioms] in TcInstDcls. This means that
+we sometimes need to test compatibility of two axioms that were eta-reduced to
+different degrees, e.g.:
+
+
+data family D a b c
+newtype instance D a Int c = DInt (Maybe a)
+  -- D a Int ~ Maybe
+  -- lhs = [a, Int]
+newtype instance D Bool Int Char = DIntChar Float
+  -- D Bool Int Char ~ Float
+  -- lhs = [Bool, Int, Char]
+
+These are obviously incompatible. We could detect this by saturating
+(eta-expanding) the shorter LHS with fresh tyvars until the lists are of
+equal length, but instead we can just remove the tail of the longer list, as
+those types will simply unify with the freshly introduced tyvars.
+
+By doing this, in case the LHS are unifiable, the yielded substitution won't
+mention the tyvars that appear in the tail we dropped off, and we might try
+to test equality RHSes of different kinds, but that's fine since this case
+occurs only for data families, where the RHS is a unique tycon and the equality
+fails anyway.
 -}
 
 -- See Note [Compatibility]
 compatibleBranches :: CoAxBranch -> CoAxBranch -> Bool
 compatibleBranches (CoAxBranch { cab_lhs = lhs1, cab_rhs = rhs1 })
                    (CoAxBranch { cab_lhs = lhs2, cab_rhs = rhs2 })
-  = case tcUnifyTysFG (const BindMe) lhs1 lhs2 of
+  = let (commonlhs1, commonlhs2) = zipAndUnzip lhs1 lhs2
+             -- See Note [Compatibility of eta-reduced axioms]
+    in case tcUnifyTysFG (const BindMe) commonlhs1 commonlhs2 of
       SurelyApart -> True
       Unifiable subst
         | Type.substTyAddInScope subst rhs1 `eqType`
diff --git a/compiler/types/Unify.hs b/compiler/types/Unify.hs
index 60bba1289f..951a3f9f93 100644
--- a/compiler/types/Unify.hs
+++ b/compiler/types/Unify.hs
@@ -344,26 +344,6 @@ If we discover that two types unify if and only if a skolem variable is
 substituted, we can't properly unify the types. But, that skolem variable
 may later be instantiated with a unifyable type. So, we return maybeApart
 in these cases.
-
-Note [Lists of different lengths are MaybeApart]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-It is unusual to call tcUnifyTys or tcUnifyTysFG with lists of different
-lengths. The place where we know this can happen is from compatibleBranches in
-FamInstEnv, when checking data family instances. Data family instances may be
-eta-reduced; see Note [Eta reduction for data family axioms] in TcInstDcls.
-
-We wish to say that
-
-  D :: * -> * -> *
-  axDF1 :: D Int ~ DFInst1
-  axDF2 :: D Int Bool ~ DFInst2
-
-overlap. If we conclude that lists of different lengths are SurelyApart, then
-it will look like these do *not* overlap, causing disaster. See Trac #9371.
-
-In usages of tcUnifyTys outside of family instances, we always use tcUnifyTys,
-which can't tell the difference between MaybeApart and SurelyApart, so those
-usages won't notice this design choice.
 -}
 
 -- | Simple unification of two types; all type variables are bindable
@@ -1044,7 +1024,8 @@ unify_tys env orig_xs orig_ys
       -- See Note [Kind coercions in Unify]
       = do { unify_ty env x y (mkNomReflCo $ typeKind x)
            ; go xs ys }
-    go _ _ = maybeApart  -- See Note [Lists of different lengths are MaybeApart]
+    go _ _ = surelyApart
+      -- Possibly different saturations of a polykinded tycon (See Trac #15704)
 
 ---------------------------------
 uVar :: UMEnv
diff --git a/compiler/utils/Util.hs b/compiler/utils/Util.hs
index c348f79888..c6c5362112 100644
--- a/compiler/utils/Util.hs
+++ b/compiler/utils/Util.hs
@@ -16,7 +16,7 @@ module Util (
 
         -- * General list processing
         zipEqual, zipWithEqual, zipWith3Equal, zipWith4Equal,
-        zipLazy, stretchZipWith, zipWithAndUnzip,
+        zipLazy, stretchZipWith, zipWithAndUnzip, zipAndUnzip,
 
         zipWithLazy, zipWith3Lazy,
 
@@ -441,6 +441,15 @@ zipWithAndUnzip f (a:as) (b:bs)
     (r1:rs1, r2:rs2)
 zipWithAndUnzip _ _ _ = ([],[])
 
+-- | This has the effect of making the two lists have equal length by dropping
+-- the tail of the longer one.
+zipAndUnzip :: [a] -> [b] -> ([a],[b])
+zipAndUnzip (a:as) (b:bs)
+  = let (rs1, rs2) = zipAndUnzip as bs
+    in
+    (a:rs1, b:rs2)
+zipAndUnzip _ _ = ([],[])
+
 mapAccumL2 :: (s1 -> s2 -> a -> (s1, s2, b)) -> s1 -> s2 -> [a] -> (s1, s2, [b])
 mapAccumL2 f s1 s2 xs = (s1', s2', ys)
   where ((s1', s2'), ys) = mapAccumL (\(s1, s2) x -> case f s1 s2 x of