Consider inferring a higher-rank kind for type synonyms

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 (closed), but is not tightly coupled to that ticket.

Trac metadata

Trac field	Value
Version	8.0.1
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture