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 |