Opened 9 years ago

Closed 8 years ago

#4310 closed bug (fixed)

Deferred equalities and forall types

Reported by: simonpj Owned by: simonpj
Priority: normal Milestone: 7.4.1
Component: Compiler Version: 6.12.3
Keywords: Cc: stefan@…, dimitris@…, coreyoconnor@…, jwlato@…, v.dijk.bas@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: typecheck/should_compile/T4310
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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

Change History (10)

comment:1 Changed 9 years ago by igloo

Milestone: 7.2.1
Owner: set to simonpj

comment:2 Changed 8 years ago by simonpj

A related post to ghc-users:

From: Stefan Holdermans [mailto:stefan@vectorfabrics.com] 
Sent: 21 June 2011 10:51
Subject: Type function under a forall type

Simon, Tom,

I hit this type-error message in GHC 7.0.3:

  Cannot deal with a type function under a forall type:
  forall e. El e u

Is there a fundamental reason why type functions under a forall type are a bad idea? Of is it just something that hasn't been implemented/thought about yet?

comment:3 Changed 8 years ago by simonpj

Dimitrios and I don't think there is a fundamental difficulty here, but it involves some work on the constraint solver that we have not yet done, especially concerning the evidence that is constructed for a proof.

So it's on the list, but currently not very high priority. Yell if it's important to you.

Simon

comment:4 Changed 8 years ago by stefan

Cc: stefan@… added

comment:5 Changed 8 years ago by dimitris

Cc: dimitris@… added

comment:6 Changed 8 years ago by CoreyOConnor

Cc: coreyoconnor@… added

comment:7 Changed 8 years ago by simonpj

See also #5595

comment:8 Changed 8 years ago by jwlato

Cc: jwlato@… added

comment:9 Changed 8 years ago by basvandijk

Cc: v.dijk.bas@… added

comment:10 Changed 8 years ago by simonpj

difficulty: Unknown
Resolution: fixed
Status: newclosed
Test Case: typecheck/should_compile/T4310

Fixed by the same patch as #5595.

Note: See TracTickets for help on using tickets.