<html><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;">Kim,<div><br></div><div>What you are observing is that just because module m is correct, and can be proved so by a fairly simple type system, does <i>not</i> mean that every possible module m' that inherits from m and overrides arbitrary parts of m is also correct and type-safe. <br></div><div><br></div><div>If you want to do static checks for this, it's always seemed to me that m needs two quite different types. The first is the user's type, or the interface type, which provides information about the external interface of m — which is what existing Grace types do.</div><div><br></div><div>The second is the heir's type, which provides information about the internal structure of m. In your example, it provides the information that a.new -> Alpha and Alpha <: type {x -> Number} (which is in the confidential interface type), but also that b.new uses a internally, with that type. </div><div><br></div><div>Figuring out what's in an heirs type seems like a good thesis project.</div><div><br></div><div><span class="Apple-tab-span" style="white-space:pre"> </span>Andrew</div><div><br></div></body></html>