In this episode, I begin discussing a paper titled "Type Inference with Simple Subtypes," by John C. Mitchell.  The paper presents algorithms for computing a type and set of subtype constraints for any term of the pure lambda calculus.  I mostly focus here on how subtype constraints allow typing any term (which seems surprising).