#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