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