| > g = \x::(Int,Bool) -> let-type (a,b) = (Int,Bool) in e | > | > But notice that the RHS of a pattern-matching let-type is | statically | > guaranteed to have the right shape. So I don't allow | > | > let-type (a,b) = c in ... | > | > (where c is a type variable). | | Really? I disagree. Making pattern type sygnatures perform | unification of the variable with the supplied signature is | useful for resolving ambiguities, and backward-compatible | (valid programs will remain valid), and doesn't allow | "unwanted generality" to cause trouble (when an expression | has a more general type than needed). I was meaning in the translation into System F of the program. Under my proposal (= yours) if one writes f (x::(a,b)) = e then f is forced to have type f :: (T1, T2) -> ... for some T1, T2. In saying that let-type can't pattern-match against a type variable c, I'm just saying that f cannot have type f :: forall c. c -> .... I think I just didn't express myself well enough. Simon