#13399: Location of `forall` matters with higher-rank kind polymorphism -------------------------------------+------------------------------------- Reporter: crockeea | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.2 Resolution: | Keywords: TypeInType 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 crockeea): **Use case:** I'm working on a HOAS for a [http://okmij.org/ftp/tagless-final/ tagless final] DSL. That approach uses GADTs for "interpreters" of various languages (classes). The class `C` in my example comes from the language for lambda abstractions in our depth-indexed language. Namely, {{{ class LambdaD (expr :: forall k . k -> * -> *) where lamD :: (expr da a -> expr db b) -> expr '(da,db) (a -> b) appD :: expr '(da,db) (a -> b) -> expr da a -> expr db b }}} where `expr` is one of the GADT interpreters. We need to remember the depth of the input and output of the function, so we change the ''kind'' of the "depth" to a pair. **Back to this ticket:** However, I just realized you don't actually need higher-rank polymorphism to see this bug. You can do the following in GHCi: {{{
:set -XTypeInType :set -XRankNTypes :set -fprint-explicit-foralls data Bar :: forall k. (* -> *) -> k -> * :kind! Bar Bar :: forall k. (* -> *) -> k -> * -- precisely what I wrote, no surprise here :kind! (Bar Maybe :: forall k. k -> *) <interactive>:1:2: error: • Expected kind ‘forall k. k -> *’, but ‘Bar Maybe’ has kind ‘k0 -> *’ • In the type ‘(Bar Maybe :: forall k. k -> *)’ }}}
-- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13399#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler