Opened 7 months ago

Closed 6 weeks ago

#13408 closed feature request (wontfix)

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 (2)

comment:1 Changed 3 months ago by RyanGlScott

Cc: RyanGlScott added

comment:2 Changed 6 weeks ago by goldfire

Resolution: wontfix
Status: newclosed

Actually, this is all bogus. In type G = F, F is undersaturated, which is disallowed. And once we write type G z = F z, when we're inferring a higher-rank type for z, we've gone further off the map than I'm comfortable with.

Additionally, getting this right would require tracking recursiveness in type declarations more than we do already, and it's not worth the pain.

So I'm closing as wontfix. Anyone who wants this can always add a kind signature.

Note: See TracTickets for help on using tickets.