Skip to content

GitLab

  • Menu
Projects Groups Snippets
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
  • GHC GHC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 4,865
    • Issues 4,865
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 461
    • Merge requests 461
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Code review
    • Insights
    • Issue
    • Repository
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #17277
Closed
Open
Created Sep 30, 2019 by sheaf@sheafMaintainer

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
Assignee
Assign to
Time tracking