#13399: Location of `forall` matters with 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: | -------------------------------------+------------------------------------- Description changed by crockeea: Old description:

The following code fails to compile, but probably should:

{{{ {-# LANGUAGE RankNTypes, TypeInType #-}

import Data.Kind

data Foo :: forall k . (* -> *) -> k -> * -- Decl 1

class C (a :: forall k . k -> *)

instance C (Foo a) -- error on this line }}}

with the error

{{{ • Expected kind ‘forall k. k -> *’, but ‘Foo a’ has kind ‘k0 -> *’ • In the first argument of ‘C’, namely ‘Foo a’ In the instance declaration for ‘C (Foo a)’ }}}

Similarly, the following declarations of `Foo` also cause a similar error at the instance declaration:

Decl 2: `data Foo :: (* -> *) -> k -> *`

Decl 3: `data Foo (a :: * -> *) (b :: k)`

However, if I move the `forall` to a point ''after'' the first type parameter (which is where the instance is partially applied) thusly:

Decl 4: `data Foo :: (* -> *) -> forall k . k -> *`

then GHC happily accepts the instance of `C`.

From my (admittedly negligible) knowledge of type theory, the signatures for Decls 1 and 4 (and 2) are identical, since the `forall` can be floated to the front of Decl 4. GHC should accept any of the four versions of `Foo`, since they are all equivalent.

As a side note, I was surprised to discover that the syntax for Decl 4 is even allowed. What is the point of allowing a "global"/rank-1 forall anywhere but at the left edge of the signature (other than as a convenient workaround for this bug)?

New description: The following code fails to compile, but probably should: {{{ {-# LANGUAGE RankNTypes, TypeInType #-} import Data.Kind data Foo :: forall k . (* -> *) -> k -> * -- Decl 1 class C (a :: forall k . k -> *) instance C (Foo a) -- error on this line }}} with the error {{{ • Expected kind ‘forall k. k -> *’, but ‘Foo a’ has kind ‘k0 -> *’ • In the first argument of ‘C’, namely ‘Foo a’ In the instance declaration for ‘C (Foo a)’ }}} Similarly, the following declarations of `Foo` also cause a similar error at the instance declaration: Decl 2: `data Foo :: (* -> *) -> k -> *` Decl 3: `data Foo (a :: * -> *) (b :: k)` However, if I move the `forall` to a point ''after'' the first type parameter (which is where the instance is partially applied) thusly: Decl 4: `data Foo :: (* -> *) -> forall k . k -> *` then GHC happily accepts the instance of `C`. From my (admittedly negligible) knowledge of type theory, the signatures for Decls 1 and 4 (and 2) are identical, since the `forall` can be floated to the front of Decl 4. GHC should accept any of the four versions of `Foo`, since they are all equivalent. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13399#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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

#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 goldfire): This is all expected behavior, for a sufficiently nuanced expectation. This behavior may be undocumented however, which would be a bug. The problem all boils down to this: '''there are no type-level lambdas.''' When GHC transforms the term-level `f :: forall a. Int -> a -> a` to have type `Int -> forall a. a -> a`, it does this by generating the Core `\(n :: Int) @(a :: *) -> f a n`, which indeed works with `f` of the given type and is an expression of the desired type. Note that there is a lambda there. This is impossible at the type level. Thus: type-level `forall`s don't "float". The output from `:i` in comment:5 is an unrelated (but quite legitimate) bug. The `Foo`/`Goo` example comes from a nice rule around higher-rank types/kinds: '''GHC never infers a higher-rank type''' (or kind). So, the first (non-higher-rank) example with `Foo`/`Goo` succeeds. The second fails, because GHC won't infer a higher-rank kind for `Goo`. If you make a complete user-specified kind signature by putting a top-level kind signature on the right-hand side of the `Goo` declaration, GHC will accept, as it no longer needs to infer a higher-rank kind. At the term level, GHC makes an exception to the never-infer-higher-rank rule: when a term-level definition is by only one equation, and there is no type signature, GHC computes the (potentially higher-rank) type of the RHS and uses it as the type of the LHS. So, it's really the term level that's behaving strangely by accepting `goo2`, not the type level. Looking at this all, it seems sensible to propagate this exception to `type` declarations, which are required to obey the one-equation rule used at the term level. Admittedly, the lack of "floating" makes higher-rank kinds unwieldy. I do have a second use-case though: {{{ data (a :: k1) :~~: (b :: k2) where HRefl :: a :~~: a class HTestEquality (t :: forall k. k -> Type) where hTestEquality :: t a -> t b -> Maybe (a :~~: b) data TypeRep (a :: k) where -- or, this could be the new proper Data.Reflection.TypeRep TInt :: TypeRep Int TMaybe :: TypeRep Maybe TApp :: TypeRep a -> TypeRep b -> TypeRep (a b) instance HTestEquality TypeRep where hTestEquality TInt TInt = Just HRefl hTestEquality TMaybe TMaybe = Just HRefl hTestEquality (TApp a1 b1) (TApp a2 b2) = do HRefl <- hTestEquality a1 a2 HRefl <- hTestEquality b1 b2 return HRefl hTestEquality _ _ = Nothing }}} The need for this came up while experimenting with (prototypes of) the new `TypeRep`. See also [https://github.com/goldfirere/dependent- db/blob/master/Basics.hs#L134 this related example], necessary to power the dependently typed database example I used in my job talk. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13399#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 goldfire): I suppose you're implying that this ticket become the first bullet. Then, yes. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13399#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13399: Location of `forall` matters with higher-rank kind polymorphism -------------------------------------+------------------------------------- Reporter: crockeea | Owner: (none) Type: bug | Status: patch 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): Phab:D3860 Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * status: new => patch * differential: => Phab:D3860 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13399#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13399: Location of `forall` matters with higher-rank kind polymorphism -------------------------------------+------------------------------------- Reporter: crockeea | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.4.1 Component: Compiler | Version: 8.0.2 Resolution: fixed | 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): Phab:D3860 Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: patch => closed * resolution: => fixed * milestone: => 8.4.1 Old description:

The following code fails to compile, but probably should:

{{{ {-# LANGUAGE RankNTypes, TypeInType #-}

import Data.Kind

data Foo :: forall k . (* -> *) -> k -> * -- Decl 1

class C (a :: forall k . k -> *)

instance C (Foo a) -- error on this line }}}

with the error

{{{ • Expected kind ‘forall k. k -> *’, but ‘Foo a’ has kind ‘k0 -> *’ • In the first argument of ‘C’, namely ‘Foo a’ In the instance declaration for ‘C (Foo a)’ }}}

Similarly, the following declarations of `Foo` also cause a similar error at the instance declaration:

Decl 2: `data Foo :: (* -> *) -> k -> *`

Decl 3: `data Foo (a :: * -> *) (b :: k)`

However, if I move the `forall` to a point ''after'' the first type parameter (which is where the instance is partially applied) thusly:

Decl 4: `data Foo :: (* -> *) -> forall k . k -> *`

then GHC happily accepts the instance of `C`.

From my (admittedly negligible) knowledge of type theory, the signatures for Decls 1 and 4 (and 2) are identical, since the `forall` can be floated to the front of Decl 4. GHC should accept any of the four versions of `Foo`, since they are all equivalent.

New description: The following code fails to compile, but probably should: {{{#!hs {-# LANGUAGE RankNTypes, TypeInType #-} import Data.Kind data Foo :: forall k . (* -> *) -> k -> * -- Decl 1 class C (a :: forall k . k -> *) instance C (Foo a) -- error on this line }}} with the error {{{ • Expected kind ‘forall k. k -> *’, but ‘Foo a’ has kind ‘k0 -> *’ • In the first argument of ‘C’, namely ‘Foo a’ In the instance declaration for ‘C (Foo a)’ }}} Similarly, the following declarations of `Foo` also cause a similar error at the instance declaration: Decl 2: `data Foo :: (* -> *) -> k -> *` Decl 3: `data Foo (a :: * -> *) (b :: k)` However, if I move the `forall` to a point ''after'' the first type parameter (which is where the instance is partially applied) thusly: Decl 4: `data Foo :: (* -> *) -> forall k . k -> *` then GHC happily accepts the instance of `C`. From my (admittedly negligible) knowledge of type theory, the signatures for Decls 1 and 4 (and 2) are identical, since the `forall` can be floated to the front of Decl 4. GHC should accept any of the four versions of `Foo`, since they are all equivalent. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13399#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler