[GHC] #9200: Milner-Mycroft failure at the kind level

[GHC]

#9200: Milner-Mycroft failure at the kind level
----------------------------------------------+----------------------------
        Reporter:  ekmett                     |            Owner:
            Type:  bug                        |           Status:  new
        Priority:  normal                     |        Milestone:
       Component:  Compiler (Type checker)    |          Version:  7.8.2
      Resolution:                             |         Keywords:
Operating System:  Unknown/Multiple           |     Architecture:
 Type of failure:  GHC rejects valid program  |  Unknown/Multiple
       Test Case:                             |       Difficulty:  Unknown
        Blocking:                             |       Blocked By:
                                              |  Related Tickets:
----------------------------------------------+----------------------------

Comment (by dolio):

 This example:

 {{{
 foo :: forall f a. f a -> f a
 foo = ...
     where
       g :: f Int -> Int
 }}}

 just seems like bad policy to me. The top signature is a partial
 signature, the missing pieces (the kinds) should be solved, and it is not
 sufficient to only look at the signature of `foo` to do that solving. I
 can construct similar examples in Ermine, although it is a bit convoluted
 due to our currently meager tooling:

 {{{
 :type
 let { f : forall f a. f a -> f a
     ; f x = x
     } in f

 forall {k} (f : k -> *) (a : k). f a -> f a
 }}}

 {{{
 :type
 let { f : forall f a. f a -> f a
     ; f x = x where
         { z = g x
         ; g : some f a b. f a -> f b -> b
         ; g _ _ = ""
         }
     } in f

 forall (f : * -> *) (a : *). f a -> f a
 }}}

 Effectively, this signature is the same as (for us)

 {{{
 some k1 k2. forall (f : k1) (a : k2). f a -> f a
 }}}

 although we don't currently handle some-bound kinds; unspecified kinds act
 similarly, though.

 The problem with this example seems to be deciding on things too early,
 not generalizing. For instance, doesn't PARTIAL error if you apply the
 same kind of policy to:

 {{{
 foo :: forall f a. f a -> f a
 foo = ...
     where
       g :: f Maybe -> f Maybe
 }}}

 `f` will be defaulted to `* -> *`, but that is wrong for application to
 `Maybe`.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9200#comment:20>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler