Dependent quantification prevents unification
Summary
Replacing k -> Type
with forall (a :: k) -> Type
in a kind of a type constructor should not have any effect. The latter gives a name to the variable, but is otherwise equivalent... or so I thought.
Consider these definitions:
data B1 :: k -> Type
type family F1 :: k -> Type where
F1 = B1
GHC happily accepts them, unifying the kinds of B1
and F1
. However, if I make use of dependent quantification in B
but not in F
:
data B2 :: forall (a :: k) -> Type
type family F2 :: k -> Type where
F2 = B2
... GHC gets confused:
• Expected kind ‘k1 -> Type’,
but ‘B2’ has kind ‘forall (a :: k0) -> Type’
• In the type ‘B2’
In the type family declaration for ‘F2’
|
14 | F2 = B2
| ^^
Steps to reproduce
Load this in GHCi:
{-# LANGUAGE PolyKinds, TypeFamilies, RankNTypes #-}
module T where
import Data.Kind (Type)
data B1 :: k -> Type
type family F1 :: k -> Type where
F1 = B1
data B2 :: forall (a :: k) -> Type
type family F2 :: k -> Type where
F2 = B2
Expected behavior
Both F1
and F2
should be accepted.
Environment
- GHC version used: HEAD