Typechecking Failure When Going From Two “Forall”-quantified Variables to a Single One (But Works Fine in Reverse)

Summary

GHC will accept converting from forall (a :: Type) (b :: Type). Foo '(a, b) to forall (p :: (Type, Type)). Foo p but not the other way around.

Steps to reproduce

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}

import Data.Kind (Type)

data Foo :: (Type, Type) -> Type where
  Foo :: forall p. Foo p

test1 :: forall p. Foo p
test1 = Foo

test2 :: forall a b. Foo '( a, b)
test2 = test1

test3 :: forall a b. Foo '( a, b)
test3 = Foo

-- Error here
test4 :: forall p. Foo p
test4 = test3

Trying to compile this code will output:

Test.hs:20:9: error:
    * Couldn't match type `p' with '(a0, b0)
      Expected: Foo p
        Actual: Foo '(a0, b0)
      `p' is a rigid type variable bound by
        the type signature for:
          test4 :: forall (p :: (*, *)). Foo p
        at Test.hs:19:1-24
    * In the expression: test3
      In an equation for `test4': test4 = test3
    * Relevant bindings include test4 :: Foo p (bound at Test.hs:20:1)
   |
20 | test4 = test3
   |         ^^^^^
Failed, no modules loaded.

Explicitly annotating the kind of p like:

test4 :: forall (p :: (Type, Type)). Foo p
test4 = test3

does not help.

Expected behavior

No compile error, definition of test4 typechecks.

Environment

• GHC version used: 9.4.4