[TYPES] how to typing for logic equality operator

[wagnerdm at seas.upenn.edu]

Well, this rule looks a bit strange:

Quoting ??? <is99zcp at hotmail.com>:

> e1 : T1  e2 : T2  T1 <: T2 || T2 <: T1
> --------------------------------
> e1 == e2 : Bool

I would expect something along these lines instead:

e1 : T1  e2 : T2  T1 <: T  T2 <: T
----------------------------------
e1 == e2 : Bool

Does this rule have better substitution properties? If not, can you  
briefly describe examples of a well-typed term (using either rule) and  
a substitution that breaks the typed-ness? (I'm not even sure I  
understand why the rule you proposed doesn't work.)

~d