Add test for #21338

This no-skolem-info bug was fixed by the no-skolem-info patch
that will be part of GHC 9.4. This patch adds a regression test for
the issue reported in issue #21338.

Fixes #21338.

3 files changed, 74 insertions, 0 deletions

diff --git a/testsuite/tests/typecheck/should_fail/T21338.hs b/testsuite/tests/typecheck/should_fail/T21338.hs
new file mode 100644
index 0000000000..5c89ab278d
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T21338.hs
@@ -0,0 +1,40 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+
+module T21338 where
+
+import Data.Kind ( Type, Constraint )
+import Data.Proxy ( Proxy(..) )
+
+newtype K a b = K a
+
+type NP :: (Type -> Type) -> [Type] -> Type
+data NP f xs where
+
+data FieldInfo a
+
+type All :: [Type] -> Constraint
+type family All xs where {}
+
+data ConstructorInfo :: [Type] -> Type where
+  Record :: All xs => NP (K String) xs -> ConstructorInfo xs
+
+hmap :: (forall a. f a -> g a) -> h f xs -> h g xs
+hmap _ _ = undefined
+
+foo :: forall a flds. ConstructorInfo flds
+foo = undefined
+
+fieldNames :: forall (a :: Type) flds. NP (K String) flds
+fieldNames = case foo @a {- @flds -} of
+  Record np -> hmap id np
+  _ -> hmap undefined @flds
+       -- The last line caused a "No skolem info" panic on GHC 9.2 and below.
diff --git a/testsuite/tests/typecheck/should_fail/T21338.stderr b/testsuite/tests/typecheck/should_fail/T21338.stderr
new file mode 100644
index 0000000000..754763ed23
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T21338.stderr
@@ -0,0 +1,33 @@
+
+T21338.hs:38:24:
+     Couldn't match type ‘flds0’ with ‘flds’
+      Expected: NP (K String) flds
+        Actual: NP (K String) flds0
+     ‘flds0’ is untouchable
+        inside the constraints: All flds0
+        bound by a pattern with constructor:
+                   Record :: forall (xs :: [*]).
+                             All xs =>
+                             NP (K String) xs -> ConstructorInfo xs,
+                 in a case alternative
+        at T21338.hs:38:3-11
+      ‘flds’ is a rigid type variable bound by
+        the type signature for:
+          fieldNames :: forall a (flds :: [*]). NP (K String) flds
+        at T21338.hs:36:1-57
+     In the second argument of ‘hmap’, namely ‘np’
+      In the expression: hmap id np
+      In a case alternative: Record np -> hmap id np
+     Relevant bindings include
+        np :: NP (K String) flds0 (bound at T21338.hs:38:10)
+        fieldNames :: NP (K String) flds (bound at T21338.hs:37:1)
+
+T21338.hs:39:8:
+     Cannot apply expression of type ‘h0 f0 xs0 -> h0 g0 xs0’
+      to a visible type argument ‘flds’
+     In the expression: hmap undefined @flds
+      In a case alternative: _ -> hmap undefined @flds
+      In the expression:
+        case foo @a of
+          Record np -> hmap id np
+          _ -> hmap undefined @flds
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index af529398f3..c856ca7e95 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -653,3 +653,4 @@ test('T20064', normal, compile_fail, [''])
 test('T21130', normal, compile_fail, [''])
 test('T20768_fail', normal, compile_fail, [''])
 test('T21327', normal, compile_fail, [''])
+test('T21338', normal, compile_fail, [''])