Deferred equalities and forall types
In the new typechecker we occasionally find we want an equality
(forall a. F a beta) ~ (forall a. F a gamma)
where beta, gamma are unification variables that are (later) fixed from outside. As things stand we can't solve this, because our coercion form is too weak. Once Brent is done, however, I think we will. This ticket records the problem.
It shows up in package vector
:
-
Data.Vector
,Data.Vector.Unboxed
,Data.Vector.Storable
,Data.Vector.Primitive
: need to eta expand defn ofmodify
. -
Data.Vector.Generic.New
: eta expandcreate
A small example:
type function Mutable a :: * -> * -> *
data New v a = New (forall s. ST s (Mutable v s a))
create :: (forall s. ST s (Mutable v s a)) -> New v a
create = New
Trac metadata
Trac field | Value |
---|---|
Version | 6.12.3 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |