[commit: ghc] wip/rae: Fix Trac #9371. (7b3535f)

[git at git.haskell.org]

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

On branch  : wip/rae
Link       : http://ghc.haskell.org/trac/ghc/changeset/7b3535f7b9d1e2db730032691bc74ae3be237e4a/ghc

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

commit 7b3535f7b9d1e2db730032691bc74ae3be237e4a
Author: Richard Eisenberg <eir at cis.upenn.edu>
Date:   Sun Aug 3 18:40:30 2014 -0400

    Fix Trac #9371.
    
    This was very simple: lists of different lengths are
    *maybe* apart, not *surely* apart.


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

7b3535f7b9d1e2db730032691bc74ae3be237e4a
 compiler/types/Unify.lhs | 22 +++++++++++++++++++++-
 1 file changed, 21 insertions(+), 1 deletion(-)

diff --git a/compiler/types/Unify.lhs b/compiler/types/Unify.lhs
index f44e260..1eb1c2b 100644
--- a/compiler/types/Unify.lhs
+++ b/compiler/types/Unify.lhs
@@ -418,6 +418,26 @@ 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.
+
 \begin{code}
 tcUnifyTy :: Type -> Type       -- All tyvars are bindable
 	  -> Maybe TvSubst	-- A regular one-shot (idempotent) substitution
@@ -593,7 +613,7 @@ unifyList subst orig_xs orig_ys
     go subst []     []     = return subst
     go subst (x:xs) (y:ys) = do { subst' <- unify subst x y
 				; go subst' xs ys }
-    go _ _ _ = surelyApart
+    go subst _ _ = maybeApart subst  -- See Note [Lists of different lengths are MaybeApart]
 
 ---------------------------------
 uVar :: TvSubstEnv	-- An existing substitution to extend