Add test for T21306

Fixes #21306

3 files changed, 55 insertions, 0 deletions

diff --git a/testsuite/tests/typecheck/no_skolem_info/T21306.hs b/testsuite/tests/typecheck/no_skolem_info/T21306.hs
new file mode 100644
index 0000000000..db5e0d893b
--- /dev/null
+++ b/testsuite/tests/typecheck/no_skolem_info/T21306.hs
@@ -0,0 +1,25 @@
+{-# LANGUAGE GADTs               #-}
+{-# LANGUAGE RankNTypes          #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Bug where
+
+data Foo a b where
+  Foo :: Bar a b c -> Foo as c -> Foo (a,as) b
+
+data Bar a b c where
+
+data HList xs where
+  Nil :: HList ()
+  Cons :: x -> HList xs -> HList (x,xs)
+
+data EqualLists xs ys where
+  Refl :: EqualLists () ()
+  ConsRefl :: EqualLists xs ys -> EqualLists (x,xs) (x,ys)
+
+foo :: EqualLists xs ys -> HList xs -> HList ys -> Foo xs b -> Foo ys b
+foo (ConsRefl equal) (Cons _ (xs :: HList xs)) (Cons _ (ys :: HList ys)) f =
+  let k :: forall d. Foo xs d -> Foo ys d
+      k = foo equal xs ys
+  in case f of
+    Foo bar -> Foo bar $ k foo
diff --git a/testsuite/tests/typecheck/no_skolem_info/T21306.stderr b/testsuite/tests/typecheck/no_skolem_info/T21306.stderr
new file mode 100644
index 0000000000..2845cb252f
--- /dev/null
+++ b/testsuite/tests/typecheck/no_skolem_info/T21306.stderr
@@ -0,0 +1,29 @@
+
+T21306.hs:23:15: error:
+    • Couldn't match type ‘xs’ with ‘xs1’
+      Expected: EqualLists xs xs2
+        Actual: EqualLists xs1 ys
+      ‘xs’ is a rigid type variable bound by
+        a pattern with constructor:
+          Cons :: forall x xs. x -> HList xs -> HList (x, xs),
+        in an equation for ‘foo’
+        at T21306.hs:21:23-45
+      ‘xs1’ is a rigid type variable bound by
+        a pattern with constructor:
+          ConsRefl :: forall xs ys x.
+                      EqualLists xs ys -> EqualLists (x, xs) (x, ys),
+        in an equation for ‘foo’
+        at T21306.hs:21:6-19
+    • In the first argument of ‘foo’, namely ‘equal’
+      In the expression: foo equal xs ys
+      In an equation for ‘k’: k = foo equal xs ys
+    • Relevant bindings include
+        k :: Foo xs d -> Foo xs2 d (bound at T21306.hs:23:7)
+        xs :: HList xs (bound at T21306.hs:21:31)
+        equal :: EqualLists xs1 ys (bound at T21306.hs:21:15)
+
+T21306.hs:25:5: error:
+    • The constructor ‘Foo’ should have 2 arguments, but has been given 1
+    • In the pattern: Foo bar
+      In a case alternative: Foo bar -> Foo bar $ k foo
+      In the expression: case f of Foo bar -> Foo bar $ k foo
diff --git a/testsuite/tests/typecheck/no_skolem_info/all.T b/testsuite/tests/typecheck/no_skolem_info/all.T
index 5c5defc90e..7600b32ced 100644
--- a/testsuite/tests/typecheck/no_skolem_info/all.T
+++ b/testsuite/tests/typecheck/no_skolem_info/all.T
@@ -11,3 +11,4 @@ test('T20969', normal, multimod_compile_fail, ['T20969', '-v0'])
 test('T14040A', normal, compile_fail, [''])
 test('T14040', normal, compile_fail, [''])
 test('T13499', normal, compile_fail, [''])
+test('T21306', normal, compile_fail, [''])