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

19 Jun 2014

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

 I don't have a particular dislike for NEWCUSK, I think. Anything that
 allows you to do polymorphic recursion with sufficient annotation is at
 least tolerable.

 However, I don't really understand what the problem with PARGEN is that
 caused the added restrictions that make it less desirable. Is the entire
 problem closed, partially annotated type families that are non-parametric,
 and therefore act like GADT definitions and lack principal types? And is
 the motivation to then have a uniform rule for both these and everything
 else that doesn't require detecting situations that would fail to have a
 principal type?

 You (goldfire) and I discussed what we're doing in Ermine, which is now
 quite a lot like the (original) PARGEN strategy. It seems to work for the
 sort of partially specified type signatures we have, and it works for
 polymorphic recursion, including polymorphic recursion with partial
 signatures. For instance:

 {{{
 let { u : a -> a -> a
     ; u x _ = x
     ; f : some b c. forall a. a -> b -> c
     ; f x y = let { z = u x y } in g x y
     ; g _ y = f () y
     } in f
 }}}

 Without the signature on `f` the inferred type is `() -> () -> c`, but
 with it the inferred type is `b -> b -> c`.

 Anyhow, I'm not particularly adamant about your choice of (original)
 PARGEN vs. NEWCUSK. But I'd like to understand what exactly the objections
 were, and whether they're tied to GADTs and type families.

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