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 of modify.
• Data.Vector.Generic.New: eta expand create

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