| With reference to the documentation [about lexically scoped type variables] that just appeared in darcs: For the benefit of others, the draft 6.6 documentation is here http://www.haskell.org/ghc/dist/current/docs/users_guide/type-extensions .html#scoped-type-variables | Result type signatures are now equivalent to attaching the signature | to the rhs, i.e. redundant. Yes, that's true. I don't think I had fully absorbed that. They didn't *use* to be redundant, because they used to bind type variables, but now that they don't they are entirely redundant. It is perhaps sometimes a bit more convenient to write the (small) type before the (big) expression, but that's true of type signatures in general. If we cared about that we should provide a prefix form of expression type signature I think I will therefore remove them from the documentation, and (in due course) from the code. | How about finishing the decoupling of type variable binding from pattern | type signatures by introducing an (optional) pattern form | | forall v1 ... vk. C p1 ... pn | | mimicking the datatype declaration for an existential (with vi scoping | over pj, guards, where decls and the rhs), so the example would become | | data T = forall a. MkT [a] | | k :: T -> T | k (forall a. MkT [t]) = MkT t3 | where | t3::[a] = [t,t,t] Stepanie and I have discussed this idea -- but in a different syntax. We were thinking of writing a pattern like k (MkT {a} [t]) = ... where the {a} binds the polymorphic parameters. But that's new syntax and I quite like your idea of re-using forall. The other awkward question is: when there are several existential type variables, which order do they come in? You may say "the foralls in the data type decl must match the foralls in the pattern". Thus data T = forall a b. MkT ... k (forall a b. MkT ...) = ... But with GADTs, you don't necessarily write a forall. Suppose T was declared thus: data T where MkT :: b -> a -> T Now, which order should the foralls in the pattern come in? Simon