id summary reporter owner description type status priority milestone component version resolution keywords cc os architecture failure testcase blockedby blocking related differential wikipage
15869 Discrepancy between seemingly equivalent type synonym and type family RyanGlScott "Consider the following code:
{{{#!hs
{# 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:
{{{#!hs
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:
{{{#!hs
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
 ^^^^^
}}}" bug new normal Compiler (Type checker) 8.6.2 TypeFamilies, TypeInType, VisibleDependentQuantification Unknown/Multiple Unknown/Multiple GHC rejects valid program