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