Opened 5 months ago

Last modified 3 weeks ago

#13408 new feature request

Consider inferring a higher-rank kind for type synonyms

Reported by: goldfire Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.0.1
Keywords: TypeInType Cc: RyanGlScott
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

In terms, a definition comprising one non-recursive equation may have a higher-rank type inferred. For example:

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:

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.

Change History (1)

comment:1 Changed 3 weeks ago by RyanGlScott

Cc: RyanGlScott added
Note: See TracTickets for help on using tickets.