5 files changed, 55 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
diff --git a/testsuite/tests/indexed-types/should_compile/T15704.hs b/testsuite/tests/indexed-types/should_compile/T15704.hs
new file mode 100644
index 0000000000..fbd317f5e7
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T15704.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE TypeFamilies, PolyKinds #-}
+
+module T15704 where
+
+import Data.Kind
+
+data family D :: k
+
+type family F (a :: k) :: Type
+
+type instance F D = Int
+type instance F (D a) = Char
diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T
index 687e71d673..5725c96507 100644
--- a/testsuite/tests/indexed-types/should_compile/all.T
+++ b/testsuite/tests/indexed-types/should_compile/all.T
@@ -294,4 +294,5 @@ test('T15322a', normal, compile_fail, [''])
 test('T15142', normal, compile, [''])
 test('T15352', normal, compile, [''])
 test('T15664', normal, compile, [''])
+test('T15704', normal, compile, [''])
 test('T15711', normal, compile, ['-ddump-types'])