GHC doesn't reduce type family in kind signature unless its arm is twisted
Here's some code (inspired by Richard's musings here) which typechecks with GHC 8.2.1 or HEAD:
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
data family Sing (a :: k)
data SomeSing (k :: Type) where
SomeSing :: Sing (a :: k) -> SomeSing k
type family Promote k :: Type
class (Promote (Demote k) ~ k) => SingKind (k :: Type) where
type Demote k :: Type
fromSing :: Sing (a :: k) -> Demote k
toSing :: Demote k -> SomeSing k
type family DemoteX (a :: k) :: Demote k
type instance DemoteX (a :: Type) = Demote a
type instance Promote Type = Type
instance SingKind Type where
type Demote Type = Type
fromSing = error "fromSing Type"
toSing = error "toSing Type"
-----
data N = Z | S N
data instance Sing (z :: N) where
SZ :: Sing Z
SS :: Sing n -> Sing (S n)
type instance Promote N = N
instance SingKind N where
type Demote N = N
fromSing SZ = Z
fromSing (SS n) = S (fromSing n)
toSing Z = SomeSing SZ
toSing (S n) = case toSing n of
SomeSing sn -> SomeSing (SS sn)
Things get more interesting if you try to add this type instance at the end of this file:
type instance DemoteX (n :: N) = n
Now GHC will complain:
GHCi, version 8.2.0.20170522: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:49:34: error:
• Expected kind ‘Demote N’, but ‘n’ has kind ‘N’
• In the type ‘n’
In the type instance declaration for ‘DemoteX’
|
49 | type instance DemoteX (n :: N) = n
| ^
That error message smells funny, since we do have a type family instance that says Demote N = N
! In fact, if you use Template Haskell to split up the declarations manually:
...
instance SingKind N where
type Demote N = N
fromSing SZ = Z
fromSing (SS n) = S (fromSing n)
toSing Z = SomeSing SZ
toSing (S n) = case toSing n of
SomeSing sn -> SomeSing (SS sn)
$(return [])
type instance DemoteX (n :: N) = n
Then the file typechecks without issue.
Trac metadata
Trac field | Value |
---|---|
Version | 8.2.1-rc2 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |