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 |