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