[commit: ghc] master: Move eta-reduced coaxiom compatibility handling quirks into FamInstEnv. (f877d9c)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/f877d9cc99dd1ba0c038e70527031e9ba0934cd3/ghc

>---------------------------------------------------------------

commit f877d9cc99dd1ba0c038e70527031e9ba0934cd3
Author: mniip <mniip at mniip.com>
Date:   Thu Nov 1 18:33:10 2018 -0400

    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


>---------------------------------------------------------------

f877d9cc99dd1ba0c038e70527031e9ba0934cd3
 compiler/types/FamInstEnv.hs                       | 31 +++++++++++++++++++++-
 compiler/types/Unify.hs                            | 23 ++--------------
 compiler/utils/Util.hs                             | 11 +++++++-
 .../tests/indexed-types/should_compile/T15704.hs   | 12 +++++++++
 testsuite/tests/indexed-types/should_compile/all.T |  1 +
 5 files changed, 55 insertions(+), 23 deletions(-)

diff --git a/compiler/types/FamInstEnv.hs b/compiler/types/FamInstEnv.hs
index a5cfba1..d149dbf 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 60bba12..951a3f9 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 c348f79..c6c5362 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 0000000..fbd317f
--- /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 687e71d..5725c96 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'])