Allow explicit impredicativity
In this email I suggested allowing a simple form of impredicativity. With a suitable extension flag (-XExplicitImpredicativeTypes perhaps), you woudl be allowed:
- To write a polytype in a visible type argument; eg.
f @(forall a. a->a) - To write a polytype as an argument of a type in a signature e.g.
f :: [forall a. a->a] -> Int
But that’s all. A unification variable still cannot be unified with a polytype. The only way you can call a polymorphic function at a polytype is to use Visible Type Application (VTA).
So using impredicative types might be tiresome. E.g.
type SID = forall a. a->a
xs :: [forall a. a->a]
xs = (:) @SID id ( (:) @SID id ([] @ SID))In short, if you call a function at a polytype, you must use VTA. Simple, easy, predictable; and doubtless annoying. But at least it's possible.
The main motivation is that we are naughtily doing this anyway in the implementation of GeneralisedNewtypeDeriving -- see Trac #14070 (closed) #14859 (closed) ff. If we are doing it under the hood, we could just made it available to programmers.
This is much less ambitious, and much easier to implement, than the proposed Guarded impredicative polymorphism (PLDI'18).
This ticket just records the idea, to see what other use-cases people might want to add. Then someone would have to write a GHC proposal.
Trac metadata
| Trac field | Value |
|---|---|
| Version | 8.2.2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture |