On Mon, Aug 17, 2020 at 05:08:10PM +1200, Anthony Clayden wrote:
Hi Tom, I see nothing bizarre nor counterintuitive. Perhaps you need to retrain your intuitions ;-)
Perhaps, but I think my intuitions are fairly sound.
I have just noticed that with ScopedTypeVariables one can write the following bizarre definition
-- Inferred signature: -- add :: Num a => a -> a -> a add (x :: a) (y :: b) = x + y
What do you think is bizarre?
Erik in his sibling post gave the reason: x and y are given types that appear not to match, but for the function to type check the types do indeed need to match. (My objection is really nothing to do with the choice of "a" for the inferred signature; I only put the inferred signature there to confirm that's indeed what it is.)
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?
To be more concrete, what I would like to see is a design where `k` is allowed because the type `a` (bound within a pattern) does not need to unify with anything but `k2` is not allowed because `a` is forbidden to unify with `b`. ...
No: any tyvar might unify with any other. You can't ban tyvars from unifying. Unification would be useless if you can't unify globally. That's why all tyvars are (implicitly) universally quantified. (With the exception of existentially-quantified tyvars as you quote, which is another can of worms and we don't want to go there.) [...]
I think that's exactly where we (or I at least) want to go! It feels that what I'm asking for is very similar to the typechecking rules for existentials, although I'm not familiar enough with that part of the typechecker to say for sure. Tom