| Couldn't this work? | | f (MkT (x :: a) g) Yes you can do this today, but it's a bit clumsy and indirect. And it gets harder when there are more complicated constraints data T where MkT :: forall a b c. (F a ~ G b, F b ~ c) => a -> T c I don't know of a practical application, but in the dual case of applications (rather than pattern matching) we have found that specifying type arguments indirectly is sometimes very clumsy. So I like the idea of having a bale-out route to the *direct* thing. By "direct" I mean: the source program desugars to a program with type abstractions, applications and type variables bound in pattern matches. | But in general the idea of having a whole new syntax for passing types | around makes me a bit nervous; GHC Haskell is already getting quite | syntactically cluttered. Yes, but see above. There really is a principled reason for wanting this: it's not just a random feature, it's the ground truth. Type inference "fills in" the missing type arguments most of the time, but just as type signatures are usually redundant but sometimes useful, so are type arguments. It's not a new mechanism: it's just surface syntax for an existing mechanism. Simon