[MLton] Question about Definition of SML :)

[Anoq of the Sun]

Hello!


I have a question which is not due to MLton - but maybe you guys
know this. Especially maybe Matthew knows after implementing
the front-end? :)

Anyway - I'm not sure about the purpose of the restriction:

tynames VE \subseteq T of C

in the rulle (26) p. 24 in the Definition of SML.

I can see the purpose of the limitation:

tynames \tau \subseteq T of C

in rule (4) p. 21. It prevents that one returns
datatypes out of the scope where they are defined.

As far as I can see, the restriction:

tynames VE \subseteq T of C

in rule (14) p. 23 does the same to ensure that
one doesn't unpack an exception with a datatype
value which was raised out of scope from where
it was declared.

However, isn't the rule (26) redundant then? The
restriction should be there already because of rule (14)
(because an exception will have to go through a handle clause
to re-enter the program).
Or is there something special about the recursive
binding? And in case it's not redundant, why not?
And shouldn't it be in rule (25) as well then?

More concretely: I would very much like to see a
program which fails to type-check due to the
limitation in rule (26).


Cheers
-- 
http://www.HardcoreProcessing.com