[MLton] Bug with "polymorphic" exns
Matthew Fluet
fluet@cs.cornell.edu
Mon, 24 Jan 2005 18:09:03 -0500 (EST)
> The consequent:
>
> C |- val 'a x = let exception E of 'a in () end => VE' in Env
>
> is derivable by Rule 15 as:
>
> U = tyvars('a)
> (* U = {'a} *)
> C + U |- x = let exception E of 'a in () end => VE
> (* VE = {x |-> (([],unit), v)} *)
> VE' = Clos_{C,let exception E of 'a in () end} VE
> (* VE' = {x |-> (([],unit), v)} *)
> U \cap tyvars(VE') = {}
> (* {'a} \cap {} = {} *)
>
>
> Contrast this with
>
> C |- val 'a x = let exception E of 'a in fn x => E x end => VE' in Env
>
> which is _not_ derivable by Rule 15:
>
> U = tyvars('a)
> (* U = {'a} *)
> C + U |- x = let exception E of 'a in fn x => E x end => VE
> (* VE = {x |-> (([],'a -> exn), v)} *)
> VE' = Clos_{C,let exception E of 'a in fn x => E x end} VE
> (* VE' = {x |-> (([],'a -> exn), v)} *)
> U \cap tyvars(VE') <> {} (*!!!*)
> (* {'a} \cap {'a} = {'a} *)
And, for completeness, contrast this with
C |- val 'a x = fn x => let exception E of 'a in E x end => VE' in Env
which is derivable by Rule 15:
U = tyvars('a)
(* U = {'a} *)
C + U |- x = fn x => let exception E of 'a in E x end => VE
(* VE = {x |-> (([],'a -> exn), v)} *)
VE' = Clos_{C,fn x => let exception E of 'a in E x end} VE
(* VE' = {x |-> ((['a],'a -> exn), v)} *)
U \cap tyvars(VE') = {} (*!!!*)
(* {'a} \cap {} = {} *)
Here, the Clos operation gets to bind 'a in 'a -> exn, because fn x => ...
is non-expansive.