Skip to content

Explicit forall rejected in a poly-kinded type synonym

Summary

Assume we have

newtype Ap f x = MkAp (f x)
-- Ap :: forall {k}. (k -> Type) -> k -> Type

data TypeRep (t :: k)
-- TypeRep :: forall k. k -> Type

Now, let's define a few type synonyms for Ap TypeRep:

type D1 = Ap TypeRep
type D2 = (Ap TypeRep :: j -> Type)
type D3 = (Ap TypeRep :: forall j. j -> Type)

D1 and D2 work fine, and we can check their kinds to verify:

ghci> :k D1
D1 :: forall {k}. k -> Type

ghci> :k D2
D2 :: forall j. j -> Type

D3, however, is rejected with a mysterious error:

    • Expected kind ‘forall j. j -> Type’,
        but ‘Ap TypeRep’ has kind ‘k0 -> Type’
    • In the type ‘(Ap TypeRep :: forall j. j -> Type)’
      In the type declaration for ‘D3’

Now, why is that? I would think D3 is the same thing as D2, with the forall written out explicitly.

Steps to reproduce

$ stack ghci --resolver=ghc-8.6.4
ghci> :set -XPolyKinds -XRankNTypes -XNoStarIsType -fprint-explicit-foralls -Wall
ghci> import Data.Kind (Type)
ghci> newtype Ap f x = MkAp (f x)
ghci> data TypeRep (t :: k)

ghci> type D1 = Ap TypeRep
ghci> :k D1
D1 :: forall {k}. k -> Type

ghci> type D2 = (Ap TypeRep :: j -> Type)
ghci> :k D2
D2 :: forall j. j -> Type

ghci> type D3 = (Ap TypeRep :: forall j. j -> Type)
<interactive>:24:12: error:
    • Expected kind ‘forall j. j -> Type’,
        but ‘Ap TypeRep’ has kind ‘k0 -> Type’
    • In the type ‘(Ap TypeRep :: forall j. j -> Type)’
      In the type declaration for ‘D3’

Expected behavior

ghci> type D3 = (Ap TypeRep :: forall j. j -> Type)
ghci> :k D3
D3 :: forall j. j -> Type

Environment

  • GHC version used: 8.6.4
Edited by Simon Peyton Jones
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information