Poly-kinded definitions silently introduce extra type arguments captured by TypeApplications

The first type argument of a poly-kinded definition is not the one explicitly quantified over in the definition but rather the implicitly inserted kind.

This leads to the puzzling error message "Expected a type, but ‘a’ has kind ‘k’" when ghc actually expected a kind.

{-# LANGUAGE GADTs, PolyKinds, ScopedTypeVariables, TypeApplications #-}

data EQ :: k -> k -> * where
  Refl :: EQ a a

data Wrap (a :: k) = Wrap (EQ a a)

wrap :: forall (a :: k). Wrap a
wrap = Wrap @a Refl -- fails
-- wrap = Wrap @k @a Refl -- works

Trac metadata

Trac field	Value
Version	8.0.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture