[Haskell-cafe] Re: Existentially-quantified constructors: Hugs is fine, GHC is not?

[Ross Paterson]

On Thu, May 11, 2006 at 01:46:43PM +0100, Ben Rudiak-Gould wrote:
> 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
> >    constructors.
> 
> 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 a bug.

Why would a type variable be present at runtime, let alone bound to _|_?

I believe the Hugs behaviour was intentional.  It's particularly
handy with single-constructor data types, e.g. representing objects.
It does complicate the formal specification of pattern matching a bit,
but I don't think it's unsound in any way.