Implement the "Binding type variables in lambda-expressions" proposal

added needs triage label

@rae If there are no objections and I'm not missing a previous ticket on this, I'd be interested in trying to implement this proposal.

I don't know of another ticket that addresses this proposal, specifically. #15530 (closed) address the closely related https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0126-type-applications-in-patterns.rst, and might be a better place to start. Coordinate with @Ericson2314, who may be working on that ticket. Also, you should know that the proposal you link to may be amended. See https://github.com/ghc-proposals/ghc-proposals/pull/238, which I will attend to shortly.

added Ttask label and removed needs triage label

Yeah we have started #15530 (closed), and I suspect the overlap on the two tickets will be heavy. We can put up a WIP PR soon though, and if you like look for ways to parallelize the work.

@Ericson2314 That sounds good to me.

@JakobBruenker !2464 (closed) is the WIP PR, btw

Wait -- is !2464 (closed) the fix for this or for #15530 (closed)? While superficially similar, I don't expect much overlap in the implementation of the two tickets. I recommend keeping !2464 (closed) just about #15530 (closed).

Yes it's just for #15530 (closed). I was getting back back to @JakobBruenker because I thought the implementation would overlap, but I defer to your judgement on that. In that case, if @JakobBruenker or anyone else wants to get started on this they can disregard my comments and get to it.

I haven't looked !2464 (closed) in detail yet but I do suspect that some of the implementation details might be reusable for this issue - at the very least it's a good idea to check, I think, so I appreciate the link, @Ericson2314. I had planned to make a separate merge request for this issue, so we're all on the same page there.

@rae there's a couple things about the proposal that aren't clear to me from the text, i.e.

The proposal doesn't contain any examples or mention for function definitions with multiple equations - should it work for those as well? I think it's technically incompatible with the specification which merely states to interpret f <args> = body as f = \ <args> -> body. #155 (comment) mentions an example with multiple equations but I believe the point wasn't responded to.

In particular, if it should work, should the case

numId :: (Eq a, Num a) => a -> a
numId @a 4 = 4
numId x = x

fail due to differing numbers of arguments in the equations?

@rae I don't know if you saw this or not, but I was wondering if you had any thoughts on the two questions I raised in the previous comment (#17594 (comment 246759))

edit: My current thinking regarding semantics (though not necessarily implementation) is to interpret

f :: forall a b c . Ordering -> () -> ty
f LT () = body0
f @d EQ () = body1
f @e @f GT () = body2

as

f :: forall a b c . Ordering -> () -> ty
f = \ @a @b x y -> case (x, y) of
  (LT, ()) -> body0
  (EQ, ()) -> body1[d := a]
  (GT, ()) -> body2[e := a, f := b]

While following the interpretation in the proposal ("As usual, we can interpret a function defintion f <args> = body as f = \ <args> -> body") would lead to

f :: forall a b c . Ordering -> () -> ty
f = \ LT () -> body0
f = \ @d EQ () -> body1
f = \ @e @f GT () -> body2

which of course doesn't make much sense with multiple equations - but then I suppose the semantics I'm suggesting here are very similar to regular multi-equation declarations, which, in retrospect, makes me think that this was obviously the intended interpretation (barring some details), but I might be wrong.

The point about multiple equations is very apt. In the end, @Gertjan423 and I have done quite a bit of thinking about all this in the past few weeks, and it's evolved my opinions about it all. Bottom line: we don't really have a stable specification of this feature right now. The proposal is sadly incomplete on this point, and we really can't proceed without typing rules. I think in the next few weeks, we will be able to produce typing rules, which will then unlock this. But I know I've promised action and failed to deliver previously. In the meantime, then, and if you have the experience to do so, you could try writing down the typing rules. The examples above are good, but we can't reason about a system just from examples. If you don't have the background to produce typing rules, then I would recommend just waiting. This is the center of my and @Gertjan423's work together, so there's reason to be hopeful for progress.

Sorry not to be more helpful here. I keep thinking this is easy -- but it's not!

@rae I'm afraid I don't have the experience to confidently produce typing rules; I might dabble with it but don't expect usable results from me on that front. So I'll mostly take your advice of waiting.

mentioned in merge request !6313 (closed)

mentioned in merge request !6956 (closed)

added ghc proposal label

mentioned in merge request !7406 (closed)

mentioned in merge request !11109 (closed)

I want to describe an alternative plan (alternative, that is to !11109 (closed)) for how to typecheck when we have \@a -> e lambdas.

Consider

f :: Int -> forall a. Bool -> a -> a
f 1 = \@p (x::Bool) (y::p) -> blah1
f 2 = \cases { @q True y -> blah2
             ; @r False y -> blah3 }
f _ = undefined

Currently matchExpectedFunTys, called on the outer Int match group for f, will skolemise that forall a to a{sk}, pushing in the type Bool -> a{sk} -> a{sk} to check each of the RHSs for f.

But that makes it a lot harder to be sure that the \@p or \cases pattern @q, matches a forall. We need an ad-hoc thing on the Check constructor of ExprType to say "we have just skolemised these type variables". That is what !11109 (closed) does, and it probably works, although

I would really want the extra Check to have type [TcTyVar] not [ExpType].
There is quite a bit of fancy footwork (e.g. in tcArgPats) that I found hard to understand

But an alternative is to do what Richard has long advocated, namely to skolemise more lazily. Just push in the type forall a. Bool -> a -> a. Now it readily meets those big lambda. It seems much more simple and direct.

I think the changes needed would be this:

Currently tcPolyExpr (which has an ExpSigmaType argument) immediately skolemises. Instead, it would deal with
- HsLam (the key one)
- HsLet (push it inwards)
- HsCase (ditto), and HsIf
- HsPar (ditto)
- ...it is possible that I have missed one
For all other constructors (including variables and applications) it would behave as now: skolemise and call tcExpr. Thus, no effect on Quick Look etc.
The HsLam case calls tcMatchesFun as now, but the latter now accepts a ExpSigmaType.
tcMatchesFun calls matchExpectedFunTys as now; but again the latter accepts an ExpSigmaType.
matchExpectedFunTys already skolemises as it goes; the change is that the [ExpPatType] it returns now includes the invisible binders. (Need to augument ExpForAllPatTy with visibility.)
tcMatches then does the right thing with that [ExpPatType].
No change to Check in ExpType.

There is a slightly awkward split of data constructors between tcExpr and tcPolyExpr, but I don't think it's a problem.

It's a preparatory refactoring that we could (and I think should) make to GHC before adding big-lambdas. That way we can check it has no effect without getting tangled up in the big-lambda stuff.

I would really like @rae's opinion about this. And @int-index and @sand-witch of course.

I had a weak attempt to solve this issue without changing Check and faced an issue with BinderStack. Look at these lines in tcPolyCheck function:

let mono_id = mkLocalId mono_name (varMult poly_id) rho_ty in
tcExtendBinderStack [TcIdBndr mono_id NotTopLevel] $
-- Why mono_id in the BinderStack?
--    See Note [Relevant bindings and the binder stack]

The Note [Relevant bindings and the binder stack] tells us, that diagnostic about relevant bindings will not work with polymorphic Id. I don't know how to solve this problem, do you?

Another problem with lazy skolemisation is that we need to not fully skolemise type in matchExpectedFunTys. Consider this example:

foo :: forall a b c. ...
foo @ta @tb = \ @tc -> ...

Here we need to stop skolemising type of foo after two forall'd variables and pass into body forall c. ... type. It is not an unsolvable issue, but that increases patch complexity.

We also will have to move matchExpectedFunTys into tcMatch because matches can have different count of expected patterns:

foo :: Bool -> forall a b. ...
foo True @ta @tb = ...
foo False @ta = \ @tb -> ...

UPD: moving matchexpectedFunTys into tcMatch will probably break inference.

Here we need to stop skolemising type of foo after two forall'd variables and pass into body forall c. ... type. It is not an unsolvable issue, but that increases patch complexity.

That part is very easy: first match on 0 args remaining in matchExpectedFunTys and only then skolemise a forall. No new complexity, just equations in a different order!

We also will have to move matchExpectedFunTys into tcMatch because matches can have different count of expected patterns:

I had in mind that matchExpectedFunTys would continue to take the number of value args as its "arity", and stop when that reaches zero.

So then indeed in tcMatch

tcMatch :: (AnnoBody body) => TcMatchCtxt body
        -> [ExpPatType]          -- Expected pattern types
        -> ExpSigmaType            -- Expected result-type of the Match.
        -> LMatch GhcRn (LocatedA (body GhcRn))
        -> TcM (LMatch GhcTc (LocatedA (body GhcTc)))

there might be fewer [ExpPatType] than there are m_pats in the LMatch. But all the trailing pats will be type binders (like your great example above). It's easy to deal with them: they behave just like big-lambdas.

The Note [Relevant bindings and the binder stack] tells us, that diagnostic about relevant bindings will not work with polymorphic Id. I don't know how to solve this problem, do you?

You are right -- there are in fact two things that are special about the outer level in tcPolyCheck:

tcPolyCheck prag_fn
            (CompleteSig { sig_bndr  = poly_id
                         , sig_ctxt  = ctxt
                         , sig_loc   = sig_loc })
            (L bind_loc (FunBind { fun_id = L nm_loc name
                                 , fun_matches = matches }))
  = do { traceTc "tcPolyCheck" (ppr poly_id $$ ppr sig_loc)

       ; mono_name <- newNameAt (nameOccName name) (locA nm_loc)
       ; (wrap_gen, (wrap_res, matches'))
             <- setSrcSpan sig_loc $ -- Sets the binding location for the skolems
                tcSkolemiseScoped ctxt (idType poly_id) $ \rho_ty ->
                -- Unwraps multiple layers; e.g
                --    f :: forall a. Eq a => forall b. Ord b => blah
                -- NB: tcSkolemiseScoped makes fresh type variables
                -- See Note [Instantiate sig with fresh variables]

                let mono_id = mkLocalId mono_name (varMult poly_id) rho_ty in
                tcExtendBinderStack [TcIdBndr mono_id NotTopLevel] $
                -- Why mono_id in the BinderStack?
                --    See Note [Relevant bindings and the binder stack]

                setSrcSpanA bind_loc $
                tcMatchesFun (L nm_loc (idName mono_id)) matches
                             (mkCheckExpType rho_ty)

That tcSkolemiseScoped does the ExtendedForAllScope thing, to bring the forall's variables into scope in the body
And, as you point out, we need that mono_id in the relevant-binders stack.

When I was thinking about this I thought that the simplest solution may be to leave this code unchanged; but to to pass the skolemised variables in to tcMatchesFun. But that doesn't work very well in this case:

foo :: forall a b. b -> a -> a
foo @p = case v of
          True  -> \@q -> ...a...b...p...q...
          False -> \@r -> ...a...b...p...r...

The lazy-skolemisation approach would delay skolemising at least b; but b is suposed to be in scope across the entire RHS of foo.

(Actually could I mention b in the scrutinee of the case, even before the \@q??)

Urgh. That is horrible. I think we should pause and reflect on this, and consult @rae.

What about type inference for @-binders? I had in mind that I will create something like arity schema (f a b c @d e f @g @h ... will produce [Explicit 3, Implicit 1, Explicit 2, Implicit 2, ...]) and then perform inference like defer in tcMatchesFun now. But this will not work if we don't pass the rest of [ExpPatType] into rhs.

The proposal only allow @ binders when checking, I believe. Not inference.

GHC Proposal #448

In synthesis mode, when examining \ @a -> expr, we simply put a in scope as a fresh skolem variable (that is, not equal to any other type) and then check expr. <...> When we infer that expr has type ty, the expression \ @a -> expr has type forall a. ty.

Crumbs. Well that is another thing to think about, which I have not begun to do yet.

Related issue about inference for @k-binders: #23502

Hmm yes. That Note [No inference for invisible binders in type decls] says:

Note that in *terms* we do not allow
  f @a (x::a) = rhs
unless `f` has a type signature.  So we do the same for types:

which is what I thought.

I am baffled by how we might do type inference for a recursive definition

f x @a y = ...f....

More questions for @rae

Let's leave off the inference problem for later. It's an extra idea that got tacked on at the end, and is inessential. If we run into trouble with inference, just give up (for now).

The scoped type variable problem is real -- but happily it's already solved. From https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0448-type-variable-scoping.rst#52proposed-change-specification, point 6 (the link has better formatting than the below):

-XTypeAbstractions and -XExtendedForAllScope have a fraught relationship, as both are trying to accomplish the same goal via different means. Here are the rules keeping this sibling rivalry at bay:

-XExtendedForAllScope does not apply in expression type signatures. Instead, if users want a type variable brought into scope, they are encouraged to use -XTypeAbstractions. (It would not be hard to introduce a helpful error message instructing users to do this.)

If -XExtendedForAllScope is enabled, in an equation for a function definition for a function f (and similar for pattern synonym pattern bindings and pattern synonym expression bindings): a. If f is written with no arguments or its first argument is not a type argument (that is, the next token after f is not a prefix @), then -XExtendedForAllScope is in effect and brings type variables into scope. b. Otherwise, if f's first argument is a type argument, then -XExtendedForAllScope has no effect. No additional type variables are brought into scope.

In terms of implementation, this means that we do a simple syntactic check (is the first argument to the left of the = a type argument?) and use that to decide whether to eagerly skolemize or not in tcPolyCheck.

I'll now think about the inference problem.

Inference:

For non-recursive definitions (including any appearance of a literal big-lambda \ @a ->), I think the proposal has it right. Just bring the variable into scope. No problems (I think).

For recursive definitions, we risk accepting polymorphic recursion. But we don't want to quite eliminate the possibility of writing a big-lambda, because big-lambdas usefully bring type variables into scope. So how about this: We allow recursive definitions to bind a type variable, but we do not allow instantiation of this type variable (within the same recursive group). For example:

f @a x y = .... f (x - 3) (y + 1) ....

is fine. f is monomorphic in the right-hand side. Ditto

f2 x @a y = ..... f2 (x - 3) (y + 1) ....

Still fine. f is still monomorphic in the right-hand side. (The impedance matcher will have to be taught how to eta-expand. But this eta-expansion is, I believe, semantics-preserving because of the function parameters taken in the LHS.)

Not fine:

f3 @a x y = .... f3 @(Maybe a) (Just x) (y + 1) ....

This tries to instantiate a monomorphic f3. This is polymorphic recursion. No no. Maybe we could allow f3 @a in the RHS (where the a must be identical to whatever was brought into scope in the LHS), but that seems hard and is unnecessary. The rule is simple: Functions are monomorphic within their own mutually recursive group -- just as they always have been. (Would be nice to give an informative error message in this case, but actually that shouldn't be too hard I think.)

If we agree with this plan, we should update the proposal. But actually I propose finishing the implementation first before addressing the proposal, in case other problems arise requiring amendment to the proposal. And this whole treatment of inference can be done in a separate patch: checking is the important thing here, inference is just a nice-to-have.

There is a problem with inferring this example:

foo True @ta @tb = ...
foo False @ta = \ @tb -> ...

We need to have the same skolem variable for both tb, so they can be unified, but they don't.

I agree that we should not support inference for @a binders yet; checking only. One thing at a time.

The scoped type variable problem is real -- but happily it's already solved.

I'm not sure it's solved. The proposal says:

If -XExtendedForAllScope is enabled, in an equation for a function definition for a function f:

If f is written with no arguments or its first argument is not a type argument (that is, the next token after f is not a prefix @), then -XExtendedForAllScope is in effect and brings type variables into scope

Otherwise, if f's first argument is a type argument, then -XExtendedForAllScope has no effect. No additional type variables are brought into scope.

Now consider this:

v :: forall x. x -> Bool

foo2 :: forall a. Int -> a -> a
foo2 = case v (undefined :: a) of
          True  -> \@q -> ...a......q...
          False -> \@r -> ...a....r...

This falls under the first bullet, suggesting that a scoped over the whole RHS, a fact I have exploited (in a silly way) to mention a before I even get to the \@q.

This is all ridiculously corner-case stuff. I don't want to pollute the implementation with complexity to deal with it.

@rae do you like the lazy-skolemisation approach. (I'm assuming you do, since you have advocated for it in the past.) What do you think we should do in this case?

One simple possibility is simply to write (bidirectional) typing rules that say that when ExtendedForAllScope is in effect (see the above bullets) we do eager skolemisation as today -- and therefore reject foo2. I like that. Simple, direct.

@rae you were going to set up the typing rules repo, weren't you? Any progress there?

That leaves us with the "relevant bindings" question. If we don't do eager skolemisation that is significantly harder. But I'm not sure how useful it is when the binding has a type signature anyway. It'd be worth trying simply not extending the relevent-binder stack in tcPolyCheck.

@sand-witch Richard and I dicussed this today. Conclusions:

We should not support inference for** @a binders yet; checking only.
We like the lazy skolemisation story, described here: #17594 (comment 522656)
For foo2 in the comment just above (#17594 (comment 522795)), we agree that we'll do eager skolemisation, and end up rejecting the program
Let's not worry about the relevant-binder-stack business. It'll only affect programs that have @ binders, and probably not in a way that we will notice.
In short, in tcPolyCheck,
- Check the Matche for "no arguments or its first argument is not a type argument"
- If so, behave as now (eager skolemisation, binder stack etc)
- If not (i.e. a leading @a binder) do lazy skolemisation, don't extend binder stack.

Would you like to try this? Or have a call to discuss the design? Or do you want me to sketch the design in a separate branch?

I want to make refactorings that would be needed for all the implementations, like separation of \case and \cases in the AST and rebase !11109 (closed) on top of that refactorings. After that, I can try to implement lazy skolemisation.

OK. But I don't want to do code review on an implemetation with Check [Type] Type (as in the current MR). The point about lazy skolemisation is to get rid of that. So perhaps I'll await a draft lazy-skol before reviewing. Is that OK?

PS: what are these refactorings? Do we have a ticket explaining the problem?

Is that OK?

Yep, not a problem

what are these refactorings?

I can remember only separation between \case and \cases in AST, so perhaps I need to do only one refactoring. There is no ticket explaining the problem, I can create it now.

Here is it: #23916 (closed)

Am I right that, since we reject foo2 above, this example also would be rejected?

idl :: forall a. a -> a
idl = \ @t x -> x :: t

Yes. This example would be rejected. By the time we see \ @t ->, we would be checking against a monomorphic a -> a (for an in-scope, skolem a).

This is annoying, in that moving the @t over the = causes a change in behavior. This is why -XExtendedForAllScope is bad! :)

I directly implemented the plan described in this message #17594 (comment 522656), and faced with this code example:

f :: (forall a. Maybe a) -> forall a. a
f x = case x of Just y -> y

With eager skolemisation this code would be elaborated into

f = \x @a -> case x @a of Just y -> y

but according to this point

HsCase (push it inwards)

This code now elaborates into

f = \x -> case x @_??? of Just y -> \@a -> y

And fails to type-check

Couldn't match expected type ‘a’ with actual type ‘a0’
  because type variable ‘a’ would escape its scope
This (rigid, skolem) type variable is bound by
  a type expected by the context:
    forall a. a

I had hope that this issue was resolved in the stability paper, but as I can see, mixed polymorphic λ-calculus has no case expressions.

I can provide my implementation, but there are a couple of internal GHC panics which source I don't understand now, so I want to investigate it.

Lazy skolemisation implementation: !11198 (closed)

I directly implemented the plan described in this message #17594 (comment 522656), and faced with this code example:

@sand-witch that is an excellent example. If we had an explicit big-lambda in the case-branch we obviously could not typecheck it

f2 x = case x of Just y -> \@a -> y::a

The only wa to write it would be with the big-lambda further out

f3 x = \@a -> case x of Just y -> y::a

Now all is good. So that suggests that we should skolemise before the case. But the whole point of lazy skolemisation is to delay skolemisation so we can write

g :: Bool -> forall a. a -> [a]
g x = case x of
       True  -> \@p -> \(x::p) -> []
       False -> \@q -> \(y::q) -> [y,y]

I can't see how to reconcile these two; that is, how to make both f and g typecheck. Except perhaps by doing you original plan:

Skolemise eagerly
But keep track of the skolemised variables in case you meet a \@p binder

So in g we would skolemise outside the case, but record (in the Check type) that a is "just-skolemised". Then when we meet the @p we can bind p to the just-skolemised a; and similary q. The elaborated term would look like

g x = \@a -> case x of
                   True - > \(x::a) -> []
                   False -> (\y::a) -> [y,y]

I don't really like this:

It is quite complicated to explain the "just-skolemised" business
The big lambda ends up in quite a different place than it is actually written

But otherwise I think we must reject either f or g. I'm not sure which is best. Let's see what @rae thinks.

One good thing: by implementing this we have discovered a subtlety that was entirely hidden before.

Just to flesh out a real-world example, on your branch !11198 (closed), the module System.Console.Terminfo.Color fails to compile saying

libraries/terminfo/System/Console/Terminfo/Color.hs:94:22: error: [GHC-46956]
    • Couldn't match type ‘c0’ with ‘s’
      Expected: Capability (Color -> s)
        Actual: Capability (Color -> c0)
        because type variable ‘s’ would escape its scope

The reason is similar to the above. We have

setForegroundColor :: TermStr s => Capability (Color -> s)
setForegroundColor = setaf `mplus` setf
    where
        setaf = fmap (. colorIntA) $ tiGetOutput1 "setaf"
        setf = fmap (. colorInt) $ tiGetOutput1 "setf"

With lazy-skol, we don't skolemise s (or the TErmStr s => context) before dealing with the where clauses. The MR means that setaf is not generalised, so it has a type with a free unification variable bound outside the not-yet-skolemised forall-s. Disaster.

One possiblity is to skolemise more eagerly than in your branch, including at let, where, and case. But that would make a distinction between these two:

h1 :: Int -> forall a. a -> a
h1 x = \@p -> blah

h2 :: Int -> forall a. a -> a
h2 x = \@p -> blah
  where
    w = ...

For h1 we could skolemise lazily but for h2 we have to do it eageerly as Color shows. (Unless we are willing to accept some real breaking changes, which I think we probably are not.)

So our alternatives seem to be:

Plan A: skolemise lazily as in your branch. Accept that it is a breaking change. (Worse, there is no very easy/obvious workaround.)
Plan B: skolemise lazily in certain very limited cases, such as f = \@a -> blah.
Plan C (your previous plan): skolemise eagerly but track the "newly skolemised" variables so they can brought into scope with \@p -> blah.

None of these plans seems entirely satisfactory.

The goal is to use @a-binders as a replacement for ScopedTypeVariables, so I find breaking changes barely acceptable. This rules out plan A.

Plan C works, but I too find it rather confusing and distasteful that the @-binders in Core end up in a different place than the ones written in the source code.

This leaves us with Plan B. That's lazy skolemization, but various things like case and let make it eager, i.e. force it. Well, who is to say that they shouldn't force it? As long as we have sufficient expressive power to replace all current use cases for ScopedTypeVariables, I don't think it's a big deal to disallow let x = ... in \ @a -> and ask the users to write \ @a -> let x = ... in ... instead.

Yes that is a defensible position, but it does mean that h1 and h2 above behave differently, even if h2's binding was entirely innocuous like w=True. Any guards would similarly force skolemisation (they are like case). So lazy skolemisation applies only in the very narrow case of immediately-nested lambdas (Plan B1).

One could narrow it even more (Plan B2): it applies only on left-hand sides, and not for free-floating lambdas. Thus

t1 :: Int -> forall a. blah
t1 x = \@p -> blah                -- Rejected

t2 :: Int -> forall a. blah
t2 x @p = blah                    -- Accepted

That is simple and predictable. It doesn't have an odd special case for "no guards and no where clause".

What about t = foo \@a @b -> ... and t = foo \@a -> \@b -> ...?

B2 would allow us to get rid of ScopedTypeVariables, but I still find B1 preferable because it enables higher-order usage

f :: (forall a. F a) -> blah
g = f (\ @a -> ...)

The proposal has such examples in its motivation, so I think we shouldn't give up on it

What about t = foo \@a @b -> ... and t = foo \@a -> \@b -> ...?

I can't parse these! Can you cadd parens or something? Is this supposed to be an application of foo? What is foo's type?

foo :: (forall a b. SomeClass a b => r) -> r

t :: Int
t = foo \@a @b -> {- use a and b here to produce Int with help of `SomeClass a b` instance -}

B2 would allow us to get rid of ScopedTypeVariables, but I still find B1 preferable because it enables higher-order usage

Good point! We could add that to B1. So B1 had better not mean "LHSs only". It had better mean "lazy skol for LHSs and and big lambdas; but eager skol as soon as we cross to the RHS of of a definition lhs = rhs." I'm just arguing that making h1 and h2 behave differently is ... uncomfortable.

@sand-witch I still can't parse your example. Perhaps you mean this?

t = foo (\@a @b -> {- use a and b here to produce Int with help of `SomeClass a b` instance -})

Note the parens!

If so, then your point is the same as Vlad's, and I agree we want to accept those big lambdas.

Note the parens!

Ah, sorry, I'm living in the world where -XBlockArguments is enabled everywhere. Yes, I mean foo (\@a @b -> ...) and foo (\@a -> \@b -> ...). That's the same point as Vlad's.

I'm just arguing that making h1 and h2 behave differently is ... uncomfortable.

Maybe so, but making f p1 p2 p3 = ... not equivalent to f = \ p1 p2 p3 -> ... is equally uncomfortable. Besides, consider \cases. One of the ideas behind it is that the users wouldn't need to repeat the function name in each equation. So instead of

longFunctionName A B C = ...
longFunctionName D E F = ...

one could write

longFunctionName = \cases
  A B C -> ...
  D E F -> ...

Can we reconcile this with @-patterns? I think it'd be great if we could support this:

longFunctionName = \cases
  A B @a C -> ...
  D E @a F -> ...

But that means we shouldn't skolemize eagerly at the top level of the RHS

Can we reconcile this with @-patterns? I think it'd be great if we could support this:

All good points, with examples that we should include in our rationale, once we have converged.

Good discussion!

Just to check my understanding: I think this example

longFunctionName = \cases
  A B @a C -> ...
  D E @a F -> ...

isn't really in play, right? That is, we're not looking to do deep skolemization, such that our choice of lazy vs eager affects the @a there. It should matter only for an @a that comes before any term-level arguments.

I'm also unconvinced about the comment "I still find B1 preferable because it enables higher-order usage", in that I don't think B2 eliminates that example. My understanding is this:

B1. Lazy skolemization, but skolemization is forced by let, where, case, and if.
B2. Lazy skolemization, but skolemization is forced by =.

Note that B1 and B2 are incomparable: neither subsumes the other. We could do both, having skolemization forced by both case-like constructs and =. Let's call that B1/2.

B1 is uncomfortable in that putting a guard or a where on a definition changes typing.

B2 is uncomfortable in that moving a binding from the LHS to the RHS of an = changes typing. But actually note that we've done this before, to avoid unseemly interactions with -XScopedTypeVariables. So this, on its own, is not terribly upsetting to me.

What is bothersome is the interaction with \cases. In a slightly different world, I would just use \cases pervasively, and so it would be annoying if it eagerly skolemizes and thus cannot be used to bind an outer type variable. Interestingly, the interaction with \cases is bad in both B1 and B2.

Perhaps OCaml can be instructive here. It has a feature that is roughly similar to \cases, called function. (It's actually closer to \case then \cases, but it's used like we would like to use \cases.) Interestingly, there is special custom treatment of function when it appears immediately to the right of a =. So we could perhaps do the same? That is:

B3. Lazy skolemization, but skolemization is forced by =, unless the next token is a lambda (including \case or \cases).

B3 would be fouled by a where clause, but maybe that would be rare enough that no one would notice?

I'm afraid I don't have any wonderful ideas here.

B1. Lazy skolemization, but skolemization is forced by let, where, case, and if.

Yes: but it might be better to put it the other way around:

Plan B1: Lazy skolemisation, but skolemisation is forced by anything except:

Lambda
\case
\cases

And "anything" includes guards and where clauses.

So now

B2 is strictly more restrictive than B1: it skolemises before the RHS even if there are no guards or where clauses.
B1 is pretty much what Richard calls B3.

We seem to be converging.

Simon and I had a nice discussion. For a little while, we were verging toward Plan C, which is a little annoying to implement, more annoying to specify using fancy typing rules, but is most forgiving to users. But we eventually settled more on Plan B2. To reformulate:

Plan B2. Skolemise eagerly, except on any of the lambda constructs. This includes skolemising the type in a type signature before processing the RHS of an = in a FunBind.

Advantages of Plan B2:

It still allows capture of type variables in higher-rank constructs: f (\ @a @b x y -> ...) works just fine. (f (if blah then (\ @a ...) else (\ @b ...)) would not, though.)
It is unaffected by the addition of where in a FunBind.
It is easy to formalize and explain.
It allows the types of where-bound variables to mention forall-bound type variables.
It means that the presence of -XExtendedForAllScope does not affect whether a definition is accepted. (With any of the other plans, f :: forall a. ...; f = \ @b -> ... is accepted without -XExtendedForAllScope but rejected with the extension on, even if neither a nor b is ever used.)

Disadvantage of Plan B2:

It does not allow the binding of outer type variables in a \cases. That is, the following does not work:

f :: forall a. ...
f = \cases
  @a ... -> ...
  @b ... -> ...

Instead, you have to lift initial type variables to appear to the left of the =. Note that this limitation is specific to FunBinds; \cases will be able to bind type variables in first position in a higher-rank context.

The disadvantage is non-negligible, but Simon and I felt it was the least problematic of the different options. Another point in favor: if we dislike this too much in practice, it seems possible to switch to Plan C later, which should accept strictly more programs.

Have we missed anything? How does this plan sound to others?

I'm not sure how I should distinct GRHS (that's the place where guards and where clauses located, right?) of FunBind and lambda.

It does not allow the binding of outer type variables in a \cases

This will become a much more annoying with foreach. quantificator.

I'm not sure how I should distinct GRHS (that's the place where guards and where clauses located, right?) of FunBind and lambda.

With B2 you don't need to think about that -- all GRHSs trigger skolemisation.

I implementation terms, I think that means that tcMatch is given an ExpRhoType not an ExpSigmaType.

This will become a much more annoying with foreach. quantificator.

I think foreach arguments are always required and visible; so none of this implicit stuff applies. More like value arguments.

#378 allows invisible foreach. The argument can sometimes be inferred; e.g. if you have

length :: foreach (n :: Nat) . Vec n Char -> Nat`
length @n _ = n

n can be inferred in a call like length myVec.

I updated !11198 (closed) according to plan B2

mentioned in merge request !11198 (closed)

Implement the "Binding type variables in lambda-expressions" proposal

Child items ...

Activity