I wonder if the rule comes down to simply this? To every variable, or rather name or identifier (term level, type level, meta level, state variables, any subject matter that lets you create names), you always want to do two things: * Define it, or at least introduce it (e.g., quantifier, lambda). * Use it, and it refers to something you defined/introduced. Perhaps the rule is simply: When LHS has (pattern :: typevar), this defines typevar to be [an alias of] the type of the term that matches that pattern. (BTW, this also introduces term-level vars in the pattern.) When RHS has (termexpr :: typeexpr), type variables in typeexpr are references, use sites. (BTW, term-level vars in termexpr are also references, use sites.) I guess the latter is marred by the Haskell Report (or NoScopedTypeVariables) rule, e.g., (termexpr :: [t]) is like (termexpr :: forall t. [t]). Still, a reference is involved, it just refers to something else. Here is an example of my view. Given ScopedTypeVariables, f :: forall a. a -> [a] f ((x :: b) :: c) = [x :: a, x :: b, x :: c] I introduce 1 var and define 2 aliases, and go on to use all 3 in chorus.