On Wed, Apr 13, 2011 at 9:44 AM, Matthew Fluet matthew.fluet@gmail.com wrote:

On Wed, Apr 13, 2011 at 2:49 AM, Andreas Rossberg rossberg@mpi-sws.org wrote:

...

On Apr 13, 2011, at 01:49, Michael Norrish wrote:

...

Poly 5.3 rejects

?datatype foo = bar of string

?fun f x = let ? val bar as y = 3 ?in ? bar + x ?end

MLton 20091212~svn accepts it.

Who's right?

Mlton, although this is arguably a design bug of the language.

I was going to conclude that Poly/ML is right.

I don't see why rule (43) applies to the "bar as y" pattern; it is not the case that "bar \notin Dom(C)" (because "bar" is in scope) and it is not the case that "is of C(vid) = v" (because "bar" has constructor status). ?MLton omits those two antecedents in its implementation of "as"-pattern elaboration. ?(Similarly, HaMLet omits them.)

On the other hand, "val rec bar as y = fn() => 3" would allow changing the identifier status of "bar" (rule (26) and comment).

Though, as Andreas' Defects document points out, the Defn's static and dynamic semantics are inconsistent with regards to val rec bindings changing identifier status. MLton resolves the inconsistency by *not* allowing a val rec to redefine constructors (so it would reject the "val rec" version of the program). Poly/ML resolves the inconsistency by changing the dynamic semantics to change the identifier status of val rec bound variables (and not throwing the Bind exception at the point of the val rec).