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

10 Mar 2017

      #13408: Consider inferring a higher-rank kind for type synonyms
-------------------------------------+-------------------------------------
           Reporter:  goldfire       |             Owner:  (none)
               Type:  feature        |            Status:  new
  request                            |
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.1
           Keywords:  TypeInType     |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 In terms, a definition comprising one non-recursive equation may have a
 higher-rank type inferred. For example:

 {{{#!hs
 f :: (forall a. a -> a -> a) -> Int
 f z = z 0 1

 g = f
 }}}

 `g` gets an inferred type equal to `f`'s. However, this fails at the type
 level:

 {{{#!hs
 type F (z :: forall a. a -> a -> a) = z 0 1

 type G = F
 }}}

 If anything is strange here, it's that the term-level definition is
 accepted. GHC should not be in the business of inferring higher-rank
 types. But there is an exception for definitions comprising one non-
 recursive equation.

 This ticket proposes expanding this behavior to the type level, allowing
 `G` to be accepted.

 This is spun off from #13399, but is not tightly coupled to that ticket.

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13408
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler