[commit: ghc] master: Fix zonk_eq_types in TcCanonical (7d2e5da)

[git at git.haskell.org]

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

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

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

commit 7d2e5da61714025142f0085d5ae150a61e637a5e
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Mon Jan 9 14:58:02 2017 +0000

    Fix zonk_eq_types in TcCanonical
    
    This fixes Trac #13083. An egregious bug.
    
    Merge to the 8.0 branch


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

7d2e5da61714025142f0085d5ae150a61e637a5e
 compiler/typecheck/TcCanonical.hs                  | 19 +++--
 testsuite/tests/typecheck/should_compile/T13083.hs | 80 ++++++++++++++++++++++
 testsuite/tests/typecheck/should_compile/all.T     |  1 +
 testsuite/tests/typecheck/should_fail/T3950.stderr |  2 +-
 4 files changed, 96 insertions(+), 6 deletions(-)

diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index 5aeeeb8..7f5ea9a 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -700,8 +700,15 @@ zonk_eq_types = go
     go ty1 ty2
       | Just (tc1, tys1) <- tcRepSplitTyConApp_maybe ty1
       , Just (tc2, tys2) <- tcRepSplitTyConApp_maybe ty2
-      , tc1 == tc2
-      = tycon tc1 tys1 tys2
+      = if tc1 == tc2 && tys1 `equalLength` tys2
+          -- Crucial to check for equal-length args, because
+          -- we cannot assume that the two args to 'go' have
+          -- the same kind.  E.g go (Proxy *      (Maybe Int))
+          --                        (Proxy (*->*) Maybe)
+          -- We'll call (go (Maybe Int) Maybe)
+          -- See Trac #13083
+        then tycon tc1 tys1 tys2
+        else bale_out ty1 ty2
 
     go ty1 ty2
       | Just (ty1a, ty1b) <- tcRepSplitAppTy_maybe ty1
@@ -714,12 +721,14 @@ zonk_eq_types = go
       | lit1 == lit2
       = return (Right ty1)
 
-    go ty1 ty2 = return $ Left (Pair ty1 ty2)
-      -- we don't handle more complex forms here
+    go ty1 ty2 = bale_out ty1 ty2
+      -- We don't handle more complex forms here
+
+    bale_out ty1 ty2 = return $ Left (Pair ty1 ty2)
 
     tyvar :: SwapFlag -> TcTyVar -> TcType
           -> TcS (Either (Pair TcType) TcType)
-      -- try to do as little as possible, as anything we do here is redundant
+      -- Try to do as little as possible, as anything we do here is redundant
       -- with flattening. In particular, no need to zonk kinds. That's why
       -- we don't use the already-defined zonking functions
     tyvar swapped tv ty
diff --git a/testsuite/tests/typecheck/should_compile/T13083.hs b/testsuite/tests/typecheck/should_compile/T13083.hs
new file mode 100644
index 0000000..220da08
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T13083.hs
@@ -0,0 +1,80 @@
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+{-# OPTIONS_GHC -Wall #-}
+
+-- | Bug(?) in Coercible constraint solving
+
+module T13083 where
+
+import GHC.Generics (Par1(..),(:*:)(..))
+import GHC.Exts (coerce)
+
+-- Representation as free vector space
+type family V (a :: *) :: * -> *
+
+type instance V R = Par1
+type instance V (a,b) = V a :*: V b
+
+type instance V (Par1 a) = V a
+
+data R = R
+
+-- Linear map in row-major order
+newtype L a b = L (V b (V a R))
+
+-- Use coerce to drop newtype wrapper
+bar :: L a b -> V b (V a R)
+bar = coerce
+
+{-
+[W] L a b ~R V b (V a R)
+-->
+    V b (V a R)  ~R  V b (V a R)
+-}
+
+{--------------------------------------------------------------------
+    Bug demo
+--------------------------------------------------------------------}
+
+-- A rejected type specialization of bar with a ~ (R,R), b ~ (Par1 R,R)
+foo :: L (R,R) (Par1 R,R) -> V (Par1 R,R) (V (R,R) R)
+-- foo :: L (a1,R) (Par1 b1,b2) -> V (Par1 b1,b2) (V (a1,R) R)
+foo = coerce
+
+{-
+[W] L (a1,R) (Par1 b1, b2)   ~R   V (Par1 b1,b2) (V (a1,R) R)
+-->
+    V (Par1 b1, b2) (V (a1,R) R)  ~R    same
+
+    -> (V (Par1 b1) :*: V b2) ((V a1 :*: V R) R)
+    -> (:*:) (V b1) (V b2) (:*: (V a1) Par1 R)
+
+-->
+    L (a1,R) (Par1 b1, b2)   ~R   (:*:) (V b1) (V b2) (:*: (V a1) Par1 R)
+-}
+
+--     • Couldn't match representation of type ‘V Par1’
+--                                with that of ‘Par1’
+--         arising from a use of ‘coerce’
+
+-- Note that Par1 has the wrong kind (* -> *) for V Par1
+
+-- Same error:
+--
+-- foo :: (a ~ (R,R), b ~ (Par1 R,R)) => L a b -> V b (V a R)
+
+-- The following similar signatures work:
+
+-- foo :: L (R,R) (R,Par1 R) -> V (R,Par1 R) (V (R,R) R)
+-- foo :: L (Par1 R,R) (R,R) -> V (R,R) (V (Par1 R,R) R)
+
+-- Same error:
+
+-- -- Linear map in column-major order
+-- newtype L a b = L (V a (V b s))
+
+-- foo :: L (R,R) (Par1 R,R) -> V (R,R) (V (Par1 R,R) R)
+-- foo = coerce
+
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 40d31bb..b70ab83 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -564,3 +564,4 @@ test('T12925', normal, compile, [''])
 test('T12919', expect_broken(12919), compile, [''])
 test('T12936', normal, compile, [''])
 test('T13050', normal, compile, ['-fdefer-type-errors'])
+test('T13083', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/T3950.stderr b/testsuite/tests/typecheck/should_fail/T3950.stderr
index ae50a74..60da6c0 100644
--- a/testsuite/tests/typecheck/should_fail/T3950.stderr
+++ b/testsuite/tests/typecheck/should_fail/T3950.stderr
@@ -5,7 +5,7 @@ T3950.hs:15:8: error:
         w :: (* -> * -> *) -> *
         Sealed :: (* -> *) -> *
       Expected type: Maybe (w (Id p))
-        Actual type: Maybe (Sealed (Id p x0))
+        Actual type: Maybe (Sealed (Id p0 x0))
     • In the expression: Just rp'
       In an equation for ‘rp’:
           rp _