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,869
    • Issues 4,869
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 456
    • Merge requests 456
  • 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
  • #17268
Closed
Open
Created Sep 28, 2019 by Vladislav Zavialov@int-indexDeveloper

Arcane interaction of RuntimeRep with StandaloneKindSignatures

Consider this program:

{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, ExplicitForAll, StandaloneKindSignatures #-}

import Data.Kind

data R

type TY :: R -> Type
data TY r

data A (a :: TY r) = MkA (B a)

data B a = MkB (A a)

We can discover the inferred kind of A in GHCi:

ghci> :k A
A :: forall (r :: R). TY r -> Type

And then, sure enough, we can copy this signature into the original program:

{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, ExplicitForAll, StandaloneKindSignatures #-}

import Data.Kind

data R

type TY :: R -> Type
data TY r

type A :: forall (r :: R). TY r -> Type
data A (a :: TY r) = MkA (B a)

data B a = MkB (A a)

This compiles fine. Now, let's repeat the experiment using RuntimeRep instead of a new data type R:

{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, ExplicitForAll, StandaloneKindSignatures #-}

import Data.Kind
import GHC.Exts

type R = RuntimeRep

type TY :: R -> Type
data TY r

data A (a :: TY r) = MkA (B a)

data B a = MkB (A a)

To check the kind of A in GHCi, let's not forget -fprint-explicit-runtime-reps:

ghci> :set -fprint-explicit-runtime-reps 
ghci> :k A
A :: forall (r :: R). TY r -> Type

This time, if we paste this signature into the original program, we get a kind error:

{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, ExplicitForAll, StandaloneKindSignatures #-}

import Data.Kind
import GHC.Exts

type R = RuntimeRep

type TY :: R -> Type
data TY r

type A :: forall (r :: R). TY r -> Type
data A (a :: TY r) = MkA (B a)

data B a = MkB (A a)
Test.hs:12:29: error:
    • Expected kind ‘TY 'LiftedRep’, but ‘a’ has kind ‘TY r’
    • In the first argument of ‘B’, namely ‘a’
      In the type ‘(B a)’
      In the definition of data constructor ‘MkA’
   |
12 | data A (a :: TY r) = MkA (B a)
   |   

How come?

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