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. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe