forall quantifier and mandatory declarations for type variables in new analysis

[cameel]

Depends on #14655. Merged.
Fixes #14570.

This PR introduces the new forall quantifier, which can be used to declare type variables used by a function.

Currently it's usable only on free functions. We may want to consider using it for types and instantiations as well, but those already allow declaring variables and I did not touch their syntax. We may also want to allow it inside blocks to get let-polymorphism, but that's also out of scope of this PR.

Having the quantifier, we can start requiring declarations for all type variables. Thanks to this it is now possible to refer to existing type variables and also use type variables in function return types.

[ekpyron]

Since this is experimental-only, we can also wait and see if and when this will cause problems.
In general rather nice that this approach doesn't seem to take that much hacking in the name and type resolver and all is localized here!

[cameel]

Yeah. I was expecting way worse.

Though this could grow if we allow using forall with things other than just functions.

Actually, would you use it for types or instantiations as well? Or is the current way of declaring type variables there better? I initially thought that it would fit there, but after thinking about it, it actually just makes things more verbose. Especially since, unlike with functions, repeating a type variable is not really possible in those cases:

type T(A, B) = (A, B)

instantiation T(A: C1, B: C2): C {}

vs

forall (A, B)
type T(A, B) = (A, B)

forall (A: C1, B: C2)
instantiation T(A, B): C {}

or would something like this even make sense?

forall (A, B)
type T = (A, B)

forall (A: C1, B: C2)
instantiation T: C {}

[cameel]

Since this is experimental-only, we can also wait and see if and when this will cause problems.

After taking a closer look at how the registration and scope() annotation work, I think this will not cause any problems now, but it may make the interpretation of scope() on functions a bit error prone.

The declaration->scope mapping from annotations seems to be the used by name resolver only to construct the reverse scope->declaration mapping and then it's that reverse mapping that's used for name lookups. So this will work just fine.

The issue with code accessing scope() directly, on the other hand, is that it will have to explicitly account for the quantifier. Right now I allowed the quantifier only on free functions and I have not seen any checks that would be affected, but when we reintroduce contracts, this will break a lot of checks whether a function belongs to a contract. Currently they assume that the contract must be the function's scope.

I made a quick attempt to change quantified function scope in Scoper, but this breaks DeclarationRegistrationHelper's assumptions about tree traversal - it assumes that scopes follow the nesting of ScopeOpeners. This can be adjusted, but I did not want the special-casing to spread to multiple places so I reverted that change in the end.

One final thing to keep in mind is also that the scope is visible in the AST output. So it may also break external tools that make assumptions about how functions are nested.

[cameel]

I think that this PR with dependencies now covers everything mentioned in #14570.

[github-actions]

This pull request is stale because it has been open for 14 days with no activity.
It will be closed in 7 days unless the stale label is removed.

[github-actions]

This pull request is stale because it has been open for 14 days with no activity.
It will be closed in 7 days unless the stale label is removed.

[github-actions]

This pull request is stale because it has been open for 14 days with no activity.
It will be closed in 7 days unless the stale label is removed.

[cameel]

Some jobs are failing, but this does not seem related to the PR. Looks like #14839 might not have fixed everything.

[nikola-matic]

Some jobs are failing, but this does not seem related to the PR. Looks like #14839 might not have fixed everything.

Well, this is lame; looks like the image used in this PR has a different version of Python

circleci@packer-651dab20-1061-caa7-7f59-31ffa2e7d7e2  ~
$ which python
/c/Python311/python

It's 311 instead of 312, so obviously can't find the binary to symlink since it doesn't exist.

[cameel]

Hmmm... so I guess CircleCI has multiple different versions of the Windows image and they assign them randomly to CI runs? This would also explain why miniconda just suddenly disappeared without us touching the config.

If that's the case, we might be best off just doing #14847 right away to get rid of the hard-coded path.

[nikola-matic]

Hmmm... so I guess CircleCI has multiple different versions of the Windows image and they assign them randomly to CI runs? This would also explain why miniconda just suddenly disappeared without us touching the config.

If that's the case, we might be best off just doing #14847 right away to get rid of the hard-coded path.

Agreed.