Test Trac #13784

3 files changed, 75 insertions, 0 deletions

diff --git a/testsuite/tests/indexed-types/should_fail/T13784.hs b/testsuite/tests/indexed-types/should_fail/T13784.hs
new file mode 100644
index 0000000000..0a0ae044f4
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T13784.hs
@@ -0,0 +1,30 @@
+{-# LANGUAGE DataKinds, FlexibleContexts, FlexibleInstances, GADTs #-}
+{-# LANGUAGE KindSignatures, MultiParamTypeClasses, TypeFamilies, TypeOperators #-}
+
+module T13784 where
+
+import Data.Monoid ((<>))
+
+data Product :: [*] -> * where
+    (:*) :: a -> Product as -> Product (a : as)
+    Unit :: Product '[]
+infixr 5 :*
+
+instance Show (Product '[]) where
+    show Unit = "Unit"
+
+instance (Show a, Show (Product as)) => Show (Product (a : as)) where
+    show (a :* as) = show a <> " :* " <> show as
+
+class Divideable a as where
+    type Divide a as :: [*]
+    divide :: Product as -> (a, Product (Divide a as))
+
+instance Divideable a (a : as) where
+    -- type Divide a (a : as) = as
+    -- Conflicting type family instances, seems like OVERLAPS isn't a thing for type families.
+    divide (a :* as) = (a, as)
+
+instance Divideable b as => Divideable b (a : as) where
+    type Divide b (a : as) = a : Divide b as
+    divide (a :* as) = a :* divide as
diff --git a/testsuite/tests/indexed-types/should_fail/T13784.stderr b/testsuite/tests/indexed-types/should_fail/T13784.stderr
new file mode 100644
index 0000000000..547809c63f
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T13784.stderr
@@ -0,0 +1,44 @@
+
+T13784.hs:26:28: error:
+    • Could not deduce: as1 ~ (a1 : Divide a1 as1)
+      from the context: (a : as) ~ (a1 : as1)
+        bound by a pattern with constructor:
+                   :* :: forall a (as :: [*]). a -> Product as -> Product (a : as),
+                 in an equation for ‘divide’
+        at T13784.hs:26:13-19
+      ‘as1’ is a rigid type variable bound by
+        a pattern with constructor:
+          :* :: forall a (as :: [*]). a -> Product as -> Product (a : as),
+        in an equation for ‘divide’
+        at T13784.hs:26:13-19
+      Expected type: Product (Divide a (a : as))
+        Actual type: Product as1
+    • In the expression: as
+      In the expression: (a, as)
+      In an equation for ‘divide’: divide (a :* as) = (a, as)
+    • Relevant bindings include
+        as :: Product as1 (bound at T13784.hs:26:18)
+        a :: a1 (bound at T13784.hs:26:13)
+
+T13784.hs:30:24: error:
+    • Couldn't match type ‘Product (a1 : as0)’
+                     with ‘(b, Product (Divide b (a1 : as1)))’
+      Expected type: (b, Product (Divide b (a : as)))
+        Actual type: Product (a1 : as0)
+    • In the expression: a :* divide as
+      In an equation for ‘divide’: divide (a :* as) = a :* divide as
+      In the instance declaration for ‘Divideable b (a : as)’
+    • Relevant bindings include
+        as :: Product as1 (bound at T13784.hs:30:18)
+        a :: a1 (bound at T13784.hs:30:13)
+        divide :: Product (a : as) -> (b, Product (Divide b (a : as)))
+          (bound at T13784.hs:30:5)
+
+T13784.hs:30:29: error:
+    • Couldn't match expected type ‘Product as0’
+                  with actual type ‘(a0, Product (Divide a0 as1))’
+    • In the second argument of ‘(:*)’, namely ‘divide as’
+      In the expression: a :* divide as
+      In an equation for ‘divide’: divide (a :* as) = a :* divide as
+    • Relevant bindings include
+        as :: Product as1 (bound at T13784.hs:30:18)
diff --git a/testsuite/tests/indexed-types/should_fail/all.T b/testsuite/tests/indexed-types/should_fail/all.T
index 24abd30cf0..50257e6bb8 100644
--- a/testsuite/tests/indexed-types/should_fail/all.T
+++ b/testsuite/tests/indexed-types/should_fail/all.T
@@ -134,3 +134,4 @@ test('T7102', [ expect_broken(7102) ], ghci_script, ['T7102.script'])
 test('T7102a', normal, ghci_script, ['T7102a.script'])
 test('T13271', normal, compile_fail, [''])
 test('T13674', normal, compile_fail, [''])
+test('T13784', normal, compile_fail, [''])