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.