On Sun, Aug 16, 2020 at 01:17:11PM +0100, Tom Ellis wrote:
-- Inferred signature: -- add :: Num a => a -> a -> a add (x :: a) (y :: b) = x + y [...]
But this leads to a rather puzzling user experience. Was it really not possible to design this extension in a way that would allow bringing new type variables into scope locally but not allow them to unify with other type variables from outer scopes?
Back to Tom's original question, the answer is "no" because in fact no unification of `a` and `b` is taking place. The type variables `a` and `b` in the above lexical Pattern Type Signatures are not "generalised": http://downloads.haskell.org/ghc/8.10.1/docs/html/users_guide/glasgow_exts.h... Unlike expression and declaration type signatures, pattern type signatures are not implicitly generalised. So what the example definition of `add` says (beyond giving a formula for add x y) is that also the lexical type variables `a` and `b` satisfy: a ~ TypeOf(x) b ~ TypeOf(y) but since we've already inferred: TypeOf(x) ~ TypeOf(y), bringing `a` and `b` into scope does not change that in any way. -- Viktor.