Hi, let me answer your questions by comparing what's implemented in Chameleon. (For details see http://www.comp.nus.edu.sg/~sulzmann/chameleon/download/haskell.html#scoped)
---- QUESTION 1 -----
In short, I'm considering adopting the Mondrian/Chameleon rule for GHC. There are two variations
1a) In the example, 'a' is only brought into scope in the right hand side if there's an explicit 'forall' written by the programmer 1b) It's brought into scope even if the forall is implicit; e.g. f :: a -> a f x = (x::a)
I'm inclined to (1a). Coments?
Currently, Chameleon goes for 1b), i.e. foralls are implicit. I agree that 1a) might help the programmer to immediately see which variables are bound by the outer scope.
----- QUESTION 2 ------
[...]
The alternatives I can see are
2a) Make an arbitrary choice of (A) or (B); GHC currently chooses (B) 2b) Decide that the scoped type variables arising from pattern bindings scope only over the right hand side, not over the body of the let 2b) Get rid of result type signatures altogether; instead, use choice (1a) or (1b), and use a separate type signature instead.
Opinions?
Chameleon goes for 2c) A Chameleon speciality is that we can write f ::: a->a f x = True f ::: a->a states that f has type a->a for some a. ::: follows the same scoping rules as :: Then, the following statement let f (x::[a],ys) = <rhs> in <body> (I assume that x::[a] states here that x has type [a] for some a) can be encoded as let f ::: ([a],b)->c f (x::[a],ys) = <rhs> in <body> The main motivation behind Chameleon's lexically scoped annotations was to allow for programs such as class Eval a b where eval::a->b f :: Eval a (b,c) => a->b f x = let g :: (b,c) g = eval x in fst g As Josef pointed out, there are also examples where it might be useful that some inner annotations refer to variable a from the outer annotation. Martin