id,summary,reporter,owner,description,type,status,priority,milestone,component,version,resolution,keywords,cc,os,architecture,failure,difficulty,testcase,blockedby,blocking,related
4310,Deferred equalities and forall types,simonpj,simonpj,"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
}}}",bug,closed,normal,7.4.1,Compiler,6.12.3,fixed,,stefan@… dimitris@… coreyoconnor@… jwlato@… v.dijk.bas@…,Unknown/Multiple,Unknown/Multiple,None/Unknown,Unknown,typecheck/should_compile/T4310,,,