#14348: Poly-kinded definitions silently introduce extra type arguments captured by TypeApplications -------------------------------------+------------------------------------- Reporter: gallais | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: invalid | TypeApplications Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => closed * keywords: => TypeApplications * resolution: => invalid Comment: This is expected behavior. As noted in the [https://downloads.haskell.org/~ghc/8.2.1/docs/html/users_guide/glasgow_exts.... =#ghc-flag--XTypeApplications users' guide], GHC determines the order of arguments for type applications by doing a stable topological sort on the user-written type variables, keeping kind variables before type variables. Since `k` is user-written, this means it's available for type application, and since it's the kind of `a`, `k` comes before `a`. If you don't want `k` to be available for type application, then you can do so by not writing it explicitly: {{{#!hs {-# LANGUAGE GADTs, PolyKinds, ScopedTypeVariables, TypeApplications #-} data EQ :: k -> k -> * where Refl :: EQ a a data Wrap a = Wrap (EQ a a) wrap :: forall a. Wrap a wrap = Wrap @a Refl }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14348#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14348: Poly-kinded definitions silently introduce extra type arguments captured by TypeApplications -------------------------------------+------------------------------------- Reporter: gallais | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: invalid | TypeApplications Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): I believe what you are looking for is [https://github.com/goldfirere/ghc/pull/74 explicit specificity]. This is a GHC "proposal" that isn't fully baked yet, or even been formally proposed yet—I'm only showing this to you since you asked nicely ;) This would allow you to write: {{{#!hs data Wrap {k} (a :: k) }}} To tell GHC to treat `k` as though it were inferred (even though it's technically written in the source) and thus not available for visible type application. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14348#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler