Fix zonk_eq_types in TcCanonical

This fixes Trac #13083. An egregious bug.

Merge to the 8.0 branch

4 files changed, 96 insertions, 6 deletions

diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index 5aeeeb8e18..7f5ea9aaa8 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 0000000000..220da0855a
--- /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 40d31bbadb..b70ab83b34 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 ae50a74f3c..60da6c09ae 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 _