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
kind-checks, 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 kind-check:
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/ghc-stage2 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
| ^^^^^