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