(I’m trying very hard to avoid this thread relitigating what’s wrong with DH. That ship has sailed.)
ScopedTypeVariables is a specific(ally ugly) GHC extension. Variables (of whatever) are naturally scoped from their point of declaration throughout the smallest enclosing syntactic construct. (I don’t get what you think “as they should be” means.) Take this Lean code:
def length (α : Type) (xs : List α) : Nat :=
match xs with
| List.nil => Nat.zero
| List.cons y ys => Nat.succ (length α ys)
-- in Haskell, the signature must be textually distinct from the function def'n.
-- (I'm avoiding DH features for now, but using v8.10 type-mangling):
{-# LANGUAGE ScopedTypeVariables, ExplicitForAll, TypeApplications #-}
length :: forall a. List a -> Nat -- this line could be anywhere in the file
last :: forall a. List a -> a -- this `a` is distinct from length's `a`
-- IOW length's `a` has discontinuous scope
length List.Nil = Nat.Zero
length (List.Cons y ys) = Nat.Succ (length @a ys) -- this is length's `a`
Lean’s def textually holds together the signature with the function body. But that’s not just a type signature: it also binds the term-level dummy variable xs. It would have been a jolly good idea to support something like this in Haskell before embarking on DH with its tyvars-everywhere bondage-and-discipline. And to more smoothly support that would probably need ResultTypeSignatures – which is a piece of work shunted into the backlog when the decks were cleared for DH.
Did you read my previous remarks? (the “stupid”) Ok, I can start another thread with all I see wrong with Lean, but to give a flavour from that length example:
def length (α : Type) (xs : List α) ...
... => Nat.succ (length α ys)
Whether or not an explicit binding point for the α in the signature would be useful (Haskell has forall), why the f*** would I want to encumber every call to length with a type application when length’s argument ys gives the type? Bondage-and-discipline, unnecessary complexity gone mad. The whole merit of Haskell is (or used to be) you can keep code short and therefore easier to read, and push off the bleedin’ obvious detail to the compiler.