Inconsistent behaviour of StandaloneKindSignatures with type families which are not given standalone kind signatures
Turning on StandaloneKindSignatures
stops the following program from typechecking:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
data AB = A | B
data SAB (ab :: AB) where
SA :: SAB 'A
SB :: SAB 'B
--type SingAB :: forall (ab :: AB) -> SAB ab
type family SingAB (ab :: AB) :: SAB ab where
SingAB A = 'SA
SingAB B = 'SB
saks.hs:15:12: error:
* Expected kind `SAB ab', but 'SA has kind `SAB 'A'
* In the type 'SA
In the type family declaration for `SingAB'
|
15 | SingAB A = 'SA
|
Uncommenting the standalone kind signature allows the program to typecheck.
When removing the equations for the type family SingAB
, with or without the standalone kind signature, one has:
> :set -fprint-explicit-foralls -fprint-explicit-kinds
> :kind! SingAB
SingAB :: forall (ab :: AB) -> SAB ab
= SingAB
So I'm not sure why the equations fail to typecheck without the standalone kind signature.
Similar behaviour also happens for the invisible equivalent:
--type SingAB2 :: forall (ab :: AB). SAB ab
type family SingAB2 :: SAB ab where
SingAB2 = ( 'SA :: SAB 'A )
SingAB2 = ( 'SB :: SAB 'B )
saks.hs:21:15: error:
* Expected kind `SAB ab', but 'SA :: SAB 'A has kind `SAB 'A'
* In the type `('SA :: SAB 'A)'
In the type family declaration for `SingAB2'
|
21 | SingAB2 = ( 'SA :: SAB 'A )
| ^^^
Ditto for passing the type explicitly:
--type SingAB3 :: forall (ab :: AB). Proxy ab -> SAB ab
type family SingAB3 ( px :: Proxy ab ) :: SAB ab where
SingAB3 ( _ :: Proxy 'A ) = 'SA
SingAB3 ( _ :: Proxy 'B ) = 'SB
With StandaloneKindSignatures
enabled, this causes the following error:
saks.hs:28:13: error:
* Expected kind `Proxy @{AB} ab',
but `_ :: Proxy 'A' has kind `Proxy @{AB} 'A'
* In the first argument of `SingAB3', namely `(_ :: Proxy 'A)'
In the type family declaration for `SingAB3'
|
28 | SingAB3 ( _ :: Proxy 'A ) = 'SA
| ^^^^^^^
Either turning off StandaloneKindSignatures
, or uncommenting the standalone kind signature, allows the program to typecheck.