Skip to content

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.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information