[GHC] #15869: Discrepancy between seemingly equivalent type synonym and type family
GHC
ghc-devs at haskell.org
Wed Nov 7 16:04:08 UTC 2018
#15869: Discrepancy between seemingly equivalent type synonym and type family
-------------------------------------+-------------------------------------
Reporter: RyanGlScott | Owner: (none)
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 8.6.2
(Type checker) |
Keywords: TypeFamilies | Operating System: Unknown/Multiple
Architecture: | Type of failure: GHC rejects
Unknown/Multiple | valid program
Test Case: | Blocked By:
Blocking: | Related Tickets:
Differential Rev(s): | Wiki Page:
-------------------------------------+-------------------------------------
Consider the following code:
{{{#!hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# 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:
{{{#!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 kind-check:
{{{#!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/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
| ^^^^^
}}}
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15869>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
More information about the ghc-tickets
mailing list