[Haskell-cafe] Re: Existentially-quantified constructors: Hugs is
fine, GHC is not?
Benjamin.Rudiak-Gould at cl.cam.ac.uk
Thu May 11 08:46:43 EDT 2006
Otakar Smrz wrote:
> data ... = ... | forall b . FMap (b -> a) (Mapper s b)
> ... where FMap qf qc = stripFMap f q
> the GHC compiler as well as GHCi (6.4.2 and earlier) issue an error
> My brain just exploded.
> I can't handle pattern bindings for existentially-quantified
The problem here is a tricky interaction between irrefutable pattern
matching and existential tuples. In Core, the FMap constructor has a third
field which stores the type b, and when you match against the pattern (FMap
qf qc) you're really matching against (FMap b qf qc). (stripFMap f q) might
evaluate to _|_, in which case, according to the rules for irrefutable
matching, all of the pattern variables have to be bound to _|_. But type
variables (like b) can't be bound to _|_.
From an operational standpoint, the problem is that the (fully-evaluated)
value of b has to be available in the body of the let statement, which means
that (stripFMap f q) must be evaluated before the body, and the let
statement must diverge without reaching the body if (stripFMap f q)
diverges, since no value can be assigned to b in that case. But the
semantics of let clearly require that execution always proceed to the body
no matter what (stripFMap f q) evaluates to.
So I'm not convinced that your program is well-typed, even though it looks
fine at first. I'm not sure what happens to Haskell's semantics when you
allow type variables to be bound to _|_. The fact that Hugs allows it may be
More information about the Haskell-Cafe