Skip to content

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 foralls 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
   |                    ^^^^^
Edited by Ryan Scott
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information