Hi, Am Dienstag, den 27.03.2018, 21:53 +0000 schrieb Simon Peyton Jones:
Interesting idea from Joachim. But it's quite complicated. Here is a much simpler version.
great! I like it: It is no less expressive than the original proposal, but forward-compatible to the full version of my proposal (which allows types, not just type variables). I believe we will want the full version eventually (Both to say `foo (Nothing @Int) = …` and once we have matchable implicit argument – right, Richard?), but we don’t have to do both steps at once. May I add one constraint to the simpler alternative proposal: It is an error to @-bind a type variables that would shadow type variable that is already in scope (whether from ScopedTypeVariables, from an instance head or from a @-binder). Why? Well, for forward compatibility. But also for consistency! To our users (or, at least to me) these two expressions are different ways of writing the same things: foo1, foo1' :: forall a. a -> Int foo1 x = length (Nothing :: Maybe a) foo1' x = length (Nothing @ a) I.e. TypeApplication is just a more convenient alternative to type signatures. The same is true, in patterns, under your simplified alternative proposal: foo2, foo2' :: a -> Maybe Int -> Int foo2 _ (Nothing :: Maybe a) = 42 foo2' _ (Nothing @ a) = 42 In both forms, a is bound by the pattern (and `a ~ Int` is added to the context). But note that a change somewhere else (and it could be arbitrarily far away if `foo2` is a local function) breaks the symmetry, at least with ScopedTypeVariables enabled: foo3, foo3' :: forall a. a -> Maybe Int -> Int foo3 _ (Nothing :: Maybe a) = 42 -- type error (a ≠ Int) foo3' _ (Nothing @ a) = 42 -- shadows a Hence I would ask to simply forbid the latter form in the simplified version of the proposal. This * helps the user not shooting in his own leg and * is compatible with the full proposal, where foo3 and foo3' would be equivalent. Cheers, Joachim -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/