[GHC] #13408: Consider inferring a higher-rank kind for type synonyms

[GHC]

#13408: Consider inferring a higher-rank kind for type synonyms
-------------------------------------+-------------------------------------
        Reporter:  goldfire          |                Owner:  (none)
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.0.1
      Resolution:                    |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by RyanGlScott):

 * status:  closed => new
 * resolution:  wontfix =>


Comment:

 I talked with goldfire today about this issue, but in a slightly different
 context. The issue this time was that I had:

 {{{#!hs
 data A :: Type -> Type
 data B a :: A a -> Type
 }}}

 And I wanted to define a type synonym alias for `B`:

 {{{#!hs
 type C = B
 }}}

 This time, we came to the opposite conclusion of comment:2 — that is, GHC
 //should// be able to accept this. There are two main reasons why:

 * Unlike in the original example, in which the RHS of a type synonym was
 attempting to partially apply a type synonym (which is problematic), there
 is no problem with partially applying a data type constructor such as `B`.
 * The implementation might be easier than what goldfire had originally
 thought when writing comment:2. In the code that kind-checks type synonym
 declarations, we would need to check that the type synonym is the sole
 declaration in a mutually recursive group. (That is to say, no funny
 business with recursion is going on.) If this holds true, then we could
 grab the kind from the RHS (even if it's fancy, like the kind of `B ::
 forall a -> A a -> Type`) and use that to infer the kind of the whole type
 synonym.

 Having this work is especially important in the context of this particular
 example since there is currently no way to write the kind `forall a -> A a
 -> Type` in source Haskell. (If there were a way to write this, then `type
 C = (B :: forall a -> A a -> Type)` would already be a suitable
 workaround.)

 goldfire, please correct me if I got any details wrong here.

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