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

 Hold the phone! This is all wrong!

 == Interaction with partial type signatures ==

 I just ended a great discussion with Iavor and with David Darais about
 this whole issue, and we came to the conclusion that (PARGEN) is a bad
 idea. The problem isn't that (PARGEN) doesn't work (I still think it
 ''does'' work) but that it paints us into a corner.

 We looked at PartialTypeSignatures, which describes an upcoming feature to
 allow wildcards in type signatures of terms, in case the programmer does
 not want to write down an entire type. With partial type signatures,
 wildcards ''can'' unify with lexically-quantified variables, contrary to
 the side condition debated in this ticket. And, the feature looks useful,
 as types get more complicated and the burden of writing out a full
 signature increases.

 There is no discussion (that I saw) of polymorphic recursion w.r.t.
 partial type signatures, so I don't know what the term-level plan is on
 that issue.

 == A change of heart ==

 Looking at all of this (now back at the type level), I see that we have
 two, mutually exclusive options:
 1) Allow polymorphic recursion in the presence of a partial kind signature
 via (PARGEN) + side condition.
 2) Allow more flexible partial kind signatures.

 I think (2) is of greater benefit to users than is (1). As a further
 bonus, (2) is '''much''' simpler than (1) -- indeed, it is what we have
 today.

 == A new proposal ==

 Thus, I propose a radically different solution to the original problem:
 come up with a syntax for a CUSK for classes. Call this proposal
 (NEWCUSK). Specifically:

 '''A class or datatype is said to have a CUSK if and only if all of its
 type variables are annotated.''' Otherwise, like (BASELINE).

 As with (BASELINE), polymorphic recursion is possible only in the presence
 of a CUSK. Under (NEWCUSK), Edward's original example will not work, but
 adding an annotation to `a` (presumably, `(a :: k2)`) would make it work.

 (NEWCUSK) means that a declaration like `data Foo a b :: *` will '''not'''
 have a CUSK. This would be a breaking change if a programmer used `:: *`
 to force other variables to have kind `*` and/or used polymorphic
 recursion.
 Note that in the case where a user puts the `::` right after the datatype
 name, there are no type variables, so every one is vacuously annotated --
 no breakage here.

 If we are opposed to making this breaking change, the (NEWCUSK) proposal
 still works while also having a top-level `::` indicate a CUSK. I just
 think that the top-level `::` syntax is a strange bump in the language
 design. (Though, to be fair, I couldn't think of something better at the
 time.)

 == Relationship to GADT pattern-matching ==

 In continuing to think about all this, I have come to realize that
 (PARGEN) is quite strange, indeed. Let's consider some more familiar
 territory:

 {{{
 data G a where
   GBool :: G Bool

 foo GBool = True
 }}}

 GHC rightly rejects the code above saying, essentially, that `foo` does
 not have a principal type. `foo :: G a -> a` and `foo :: G a -> Bool` are
 both very reasonable candidates and are not comparable. (The error
 message, of course, discusses untouchables... but it's really talking
 about principal types.)

 But, if we apply the (PARGEN) philosophy to type-checking GADT pattern-
 matches, we would decide that `foo :: G a -> Bool` ''is'' the principal
 type. This is because the (PARGEN) philosophy would say to prevent the
 inferred result type from mentioning any type variables refined in the
 pattern match. I am playing a little fast and loose here talking about the
 un-articulated "(PARGEN) philosophy", but I'm hoping readers can
 understand my concern. A perhaps tighter way of saying this is: I
 conjecture that the over-permissiveness of the type system in Fig. 10 (p.
 25) of [http://msr-waypoint.com/en-us/um/people/simonpj/papers/constraints
 /jfp-outsidein.pdf OutsideIn] (as discussed in Sec. 4.4) might be fixed by
 adding a side condition to the `Case` rule, essentially saying that any
 type variables refined in a local equality assumption cannot then appear
 in other types discovered by using constraints generated by the `case`. To
 make this meaningful, the type system would have to be re-written in a
 bidirectional manner, so we can know which types come "from" the `case`
 vs. which types go "to" the `case`. I leave the exact formulation as
 future work, but I'd be very curious to read a response to this
 conjecture.

 == Conclusion ==

 What do others think of (NEWCUSK) and the points I've brought up here? It
 seems to solve the original problem (no polymorphic recursion available in
 classes) while not upsetting too much else. And, it seems to have nicer
 theoretical properties and is easier to explain to users.

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