[GHC] #13399: Location of `forall` matters with higher-rank kind polymorphism

[GHC]

#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