I think maybe the key idea I was missing here is that the type of a variable is not always the same as the type of the scope it was defined in? If I'm understan

I think maybe the key idea I was missing here is that the type of a variable is not always the same as the type of the scope it was defined in? If I'm understanding correctly, there's an implicit rule that's missing: a : la b : lb a := b -------------------------- a : lb So for example if `b : lb`: a := b :>> doSomething() need not have a type `>= lb`. Does that sound vaguely correct? Btw thanks for clarifying