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

 * I agree that (PARGEN) is a breaking change. But, I'll quote Simon's
 comment from the wiki page, which I fully agree with:

 > So moving from (BASELINE) to (PARGEN) would be a breaking change, but
 only in rather obscure circumstances. I am intensely relaxed about that
 particular backward-compatibility problem!

 * Non-recursive bindings should behave the same as recursive ones. This
 means that `NR` would be rejected due to the side condition.

 == Closed type families ==

 (PARGEN) (including the side condition) should work out just fine. Here
 would be the declarative typing rule:

 {{{
 k2 = forall fkv(k1). k1[k'1 .. k'n/_]
 fkv(k1) \not\in k'j
 forall i: G, F:k2 |- (F ps_i = t_i) ok
 k3 = gen(G, k2)
 ---------------------------------------------------
 G |- type family F :: k1 where { F ps_i = t_i } : k3
 }}}

 This is very similar to the declarative typing rule for `letrec` given on
 the [GhcKinds/KindInference wiki page]. Here, I am ignoring issues with
 arity/saturation and using a syntax where the kind signature of a type
 family is given as `k1` with blanks, instead of the tyvarbndr syntax used
 in source code.

 This is in fact an improvement over the current state of affairs, which is
 essentially this rule ''without'' the side condition. Because of the
 omitted side condition, we don't have principal types! For example,

 {{{
 type family X (a :: k) where
   X True = False
 }}}

 `X` could be `X :: k -> k` or `X :: k -> Bool`. Neither is more general
 than the other. GHC chooses `X :: k -> Bool`, but it's not principled.
 This is what I get for implementing kind inference for closed type
 families without writing out declarative rules! In any case, the solution
 to this problem (closed type families) seems to be the same as the
 solution for datatypes and classes, quite happily: add the side condition.

 == Using (PARTIAL) ==

 I'm still quite strongly against (PARTIAL). Let's ignore the backward
 compatibility problem, for now. With (PARTIAL), we have a very different
 story about kind polymorphism than we do about type polymorphism. GHC
 tries to be as polymorphic as possible with types: writing `foo x = x`
 gives `foo :: forall a. a -> a`, ''not'' `foo : () -> ()`. It seems very
 odd to me to not do the same in kinds. Yet, (PARTIAL) would say that `data
 Foo x = MkFoo (Foo x)` would get `Foo :: * -> *` instead of `Foo :: forall
 k. k -> k`. Especially as we're inching toward dependent types, this seems
 like a step backward.

 And, though I defer to Edward's experience, I tend to think the backward
 compatibility problem would be annoying for what may seem like a dubious
 benefit (polymorphic recursion in the presence of partial kind
 signatures).

 == Conclusion ==

 I ''am'' worried that (PARGEN) has a strange surface area, and I think
 that any error messages that the side condition produces should include a
 URL for further reading. (I actually think that links to further reading
 would helpful in several error messages!) But, if this surface area is
 deemed too bumpy, I personally would prefer to go back to (BASELINE) than
 to go to (PARTIAL).

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