[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 simonpj):

 I'm not quite ready to declare victory.  Some technical questions:

  * See `T1a` and `T4` under (PARGEN).  These are unexpected failures.  The
 tricky side condition means that you must declare ''all'' the polymorphism
 involving `k`, or ''none'', but nothing in between.

  * What is the rule for non-recursive bindings?  Specifically:
 {{{
 data NR f (a::k) = MkNR (f a)
 }}}
  Is this accepted (as now), or rejected by the "tricky side condition".
 If the former that gives an uncomfortable difference between recursive and
 non-recursive bindings.

  * I'd like to see a rule written down for closed type families, and a
 sketch of the accompanying algorithm.

 And finally, at a non-technical level, I'm not convinced that (PARTIAL) is
 untenable.
  * Yes, people using kind polymorphism might need to add some kind
 signatures, but that would arguably improve their code.
  * We could issue a warning for one release cycle.
  * The tricky side condition becomes simple: all kind polymorphism must be
 declared.
  * And sometimes kind polymorphism might even trip you up:
 {{{
 foo :: forall f a. f a -> f a
 foo = ...
     where
       g :: f Int -> Int
 }}}
  This will, I think, fail.  Because `foo`'s signature actually means
 {{{
 foo :: forall k. forall (f:k->*) (a:k). f a -> f a
 }}}
  so the `(f Int)` application is ill-kinded.

 Edward is an example of a high-end kind-polymorphism user.  How bad would
 (PARTIAL) be?


 Implementation.  Re `NonSkolemTv`, I'd hate to pollute `MetaInfo` for such
 a corner case.  We can simply test the side condition at the end, just as
 the rule suggests.  Generating a helpful error message is quite a
 challenge!

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