Fix Trac #9371.
authorRichard Eisenberg <eir@cis.upenn.edu>
Sun, 3 Aug 2014 22:40:30 +0000 (18:40 -0400)
committerAustin Seipp <austin@well-typed.com>
Mon, 15 Dec 2014 15:01:02 +0000 (09:01 -0600)
This was very simple: lists of different lengths are
*maybe* apart, not *surely* apart.

(cherry picked from commit f29bdfbcedda6cb33ab05d884c151f2b31f4e4e0)

compiler/types/Unify.lhs

index f2b45e8..2acbb24 100644 (file)
@@ -415,6 +415,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
@@ -590,7 +610,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