Discrepancy between seemingly equivalent type synonym and type family
Consider the following code:
{# LANGUAGE DataKinds #}
{# LANGUAGE ImpredicativeTypes #}
{# LANGUAGE LiberalTypeSynonyms #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
module Bug where
import Data.Kind
type KindOf1 (a :: k) = k
type family KindOf2 (a :: k) :: Type where
KindOf2 (a :: k) = k
data A (a :: Type) :: a > Type
type family Apply1 (f :: KindOf1 A) (a :: Type) (x :: a) :: Type where
Apply1 f a x = f a x
Apply1
kindchecks, which is just peachy. Note that Apply1
uses KindOf1
, which is a type synonym. Suppose I wanted to swap out KindOf1
for KindOf2
, which is (seemingly) an equivalent type family. I can define this:
type family Apply2 (f :: KindOf2 A)  (f :: forall a > a > Type)
(a :: Type)
(x :: a)
:: Type where
Apply2 f a x = f a x
However, GHC rejects this!
$ /opt/ghc/8.6.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:25:10: error:
• Expecting two more arguments to ‘f’
Expected kind ‘KindOf2 A’, but ‘f’ has kind ‘* > a > *’
• In the first argument of ‘Apply2’, namely ‘f’
In the type family declaration for ‘Apply2’

25  Apply2 f a x = f a x
 ^
I find this quite surprising, since I would have expected KindOf1
and KindOf2
to be functionally equivalent. Even providing explicit forall
s does not make it kindcheck:
type family Apply2 (f :: KindOf2 A)  (f :: forall a > a > Type)
(a :: Type)
(x :: a)
:: Type where
forall (f :: KindOf2 A) (a :: Type) (x :: a).
Apply2 f a x = f a x
Although the error message does change a bit:
$ ~/Software/ghc3/inplace/bin/ghcstage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:26:20: error:
• Expected kind ‘* > a > *’, but ‘f’ has kind ‘KindOf2 A’
• In the type ‘f a x’
In the type family declaration for ‘Apply2’

26  Apply2 f a x = f a x
 ^^^^^