Fixed type variables in function definitions in experimental analysis

[cameel]

Part of #14570.
Depends on #14635.

The PR introduces fixed free type variables and implements unification for them. Then replaces generic variables with fixed ones in a function definition once it's processed. It does not yet use fixed type variables for anything else.

[cameel]

Currently the PR breaks the type_classes.sol test case:

Error: Cannot unify "b:type and 'k:type.
  --> test/libsolidity/semanticTests/experimental/type_class.sol:10:5:
   |
10 |     function new() -> Self;
   |     ^^^^^^^^^^^^^^^^^^^^^^^

I think I need to replace the polymorphicInstance() call used on discovered type class functions with variable generalization. Or maybe the class variable should become a fixed variable?

[cameel]

Problem with the type class variable solved by making it a fixed type variable.

The remaining issue is that now this obviously won't unify with the concrete type used in the instantiation. I guess I have to do what I do for functions, that is, turn it into a generic variable before unification. The only complication is that it has to be a specific generic variable - the same one that was used to replace type class variable used in function definitions of that class.

[ekpyron]

I don't think this will work like done here - we will have to use unification as base mechanism here, i.e. recursively traverse the type and whenever we see a generic type variable create a new fixed one and unify (if you continue to resolve properly, unification will actually make the genericToFixed map obsolete...

If we don't do that, the function body during code generation will have generic type variables for which we cannot tell what they mean in relation to the function type.

[ekpyron]

For the reverse this will also be a bit of a headache - for that we'll need to use the concrete monomorphic function type and construct a substitution from fixed variables to instances to be used for codegen - but we can cross that bridge when we come to it, I expect this will mean a new kind of type environment that allows also tracking substitutions of fixed type variables not only generic ones to be used only in codegen (respectively for monomorphization)

[ekpyron]

Reading the PR and thinking through more implications for codegen, I actually increasingly think that it may be the better choice to just mark type variables as fixed in the type environment after all - we should talk about that.

[cameel]

This is where I stopped last week. The comparison between function type in the instantiation and the type in the class (after substitution) fails because type T(A) has a different type variable in each of these cases. The function from the instantiation has a fixed variable (like all function definitions now) while the type we substitute into the function from the class comes from instantiation header and is generalized.

[cameel]

@ekpyron I just pushed a cleaned up current state of the PR. Some of the other stuff I had in my branch went into #14635 and trivial stuff as fixups into #14510.

So currently I need to solve this problem with the type variable in polymorphic types ending up generalized and failing function type comparison when I'm processing instantiations. Then replace fixTypeVariables() with unification. I expect that to finally be enough to pass tests and be mergeable. Though TBH I've been at that point several times now and each time I end up discovering something new that I need to adjust to keep the other changed things working :)

[ekpyron]

By now, I'm quite convinced that the current attempt of introducing FixedTypeVariable as a new variant in Type is the wrong approach for this.

We should, instead, add a set of fixed type variables to TypeEnvironment. I.e. we keep it at one and the same TypeVariable and the TypeEnvironment can have some of them declared as fixed (changing the unification behaviour, which is already handled by the TypeEnvironment).

That means, that type checking a function can remain exactly the same as before, just at the end of the function you fix the types, by just adding the type variables involved in the function's signature to the set of fixed type variables in the global TypeEnvironment.

Then generalizing also remains fully identical to the current freshening.

And whenever you want to temporarily unify anything that is fixed (for example for unification during code generation) you can just create a new TypeEnvironment that does not have the variables in question marked as fixed.
(Don't worry about the fact that cloning type environments is an expensive operation at the moment, that can be implemented differently easily - same for the cost of resolving or unifying - neither will ever be a bottleneck.)

[ekpyron]

Conversely, if you want to declare a fixed type variable, you can just introduce them as the one-and-the-same-kind of TypeVariable, but just immediately mark them as fixed in the type environment.

It's a bit unfortunate that we spent some time on the other approach of introducing a completely separate kind of type variable, but that's normal for working on experimental stuff and moving the distinction to the TypeEnvironment has only advantages.

[cameel]

ok then. I'll put this PR on hold and switch to the approach with the type environment.

I think we'll still benefit from the time I spent on this because a lot of it went into trying to understand how things work and also getting some relevant tests that will tell me when I'm breaking something that's supposed to already work. So it should be quicker this time.

[cameel]

Closing in favor of #14606.

[r0qs]

Closing in favor of #14606.

Just a correction for anyone reading the comments on this PR, it was closed in favor of #14655.