id summary reporter owner description type status priority milestone component version resolution keywords cc os architecture failure testcase blockedby blocking related differential wikipage
13790 GHC doesn't reduce type family in kind signature unless its arm is twisted RyanGlScott "Here's some code (inspired by Richard's musings [https://github.com/goldfirere/singletons/issues/150#issuecomment306088297 here]) which typechecks with GHC 8.2.1 or HEAD:
{{{#!hs
{# 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:
{{{#!hs
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:
{{{#!hs
...
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." bug closed normal Compiler (Type checker) 8.2.1rc2 duplicate TypeInType, TypeFamilies Unknown/Multiple Unknown/Multiple GHC rejects valid program #12088