Test #15076 in dependent/should_compile/T15076*

Author: Richard Eisenberg

testsuite/tests/dependent/should_compile/T15076.hs

@@ -0,0 +1,13 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE PartialTypeSignatures #-}
+module Bug where
+
+import Data.Kind
+import Data.Proxy
+
+foo :: forall (a :: Type)
+              (f :: forall (x :: a). Proxy x -> Type).
+       Proxy f -> ()
+foo (_ :: _) = ()

testsuite/tests/dependent/should_compile/T15076.stderr

@@ -0,0 +1,12 @@
+
+T15076.hs:13:11: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’ standing for ‘Proxy f’
+      Where: ‘f’, ‘a’ are rigid type variables bound by
+               the type signature for:
+                 foo :: forall a (f :: forall (x :: a). Proxy x -> *). Proxy f -> ()
+               at T15076.hs:(10,1)-(12,20)
+    • In a pattern type signature: _
+      In the pattern: _ :: _
+      In an equation for ‘foo’: foo (_ :: _) = ()
+    • Relevant bindings include
+        foo :: Proxy f -> () (bound at T15076.hs:13:1)

testsuite/tests/dependent/should_compile/T15076b.hs

@@ -0,0 +1,11 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeInType #-}
+module Bug where
+
+import Data.Kind
+import Data.Proxy
+
+foo :: forall (a :: Type)
+              (f :: forall (x :: a). Proxy x -> Type).
+       Proxy f -> ()
+foo _ = ()

testsuite/tests/dependent/should_compile/T15076c.hs

@@ -0,0 +1,16 @@
+{-# LANGUAGE PolyKinds, MultiParamTypeClasses, GADTs, ScopedTypeVariables,
+             TypeOperators #-}
+{-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
+
+module Super where
+
+import Data.Kind
+import Data.Proxy
+import GHC.Prim
+
+class (a ~ b) => C a b
+data SameKind :: k -> k -> Type where
+  SK :: SameKind a b
+
+bar :: forall (a :: Type) (b :: Type). C a b => Proxy a -> Proxy b -> ()
+bar _ _ = const () (undefined :: forall (x :: a) (y :: b). SameKind x y)

testsuite/tests/dependent/should_compile/all.T

@@ -61,3 +61,6 @@ test('T14880-2', normal, compile, [''])
 test('T15743', normal, compile, ['-ddump-types -fprint-explicit-foralls'])
 test('InferDependency', normal, compile, [''])
 test('T15743e', normal, compile, ['-ddump-types -fprint-explicit-foralls'])
+test('T15076', normal, compile, [''])
+test('T15076b', normal, compile, [''])
+test('T15076c', normal, compile, [''])