#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