GitLab

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.