[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.