Compile more of ink_env.v 13 - experimental

[bartlomiejkrolikowski]

The continuation of #222.
Trying to use tactics to define instances of traits of associated types:

Problem:
The associated types and their bounds are now translated to fields of a typeclass.
This causes a problem because Coq cannot automatically find the instances places inside those fields when they are needed.
For example:

trait SomeTrait {
    type AssocTy: OtherTrait;
}

will be translated to

Module SomeTrait.
  Class Trait (Self : Set) : Type := {
    AssocTy : Set;
    _ : Sigma `(OtherTrait.Trait AssocTy), unit;
  }.
  ...
End SomeTrait.

and later in a function

Definition some_fn {T : Set} `{SomeTrait.Trait T} : SomeStruct SomeTrait.AssocTy := ...

Coq is not aware of the instance of OtherTrait.Trait AssocTy and the code above does not compile.

My solution to this was to define an alias for the instance outside the typeclass in the following way:

  Module The_Bounds_Of_AssocTy.
    Module OtherTrait.
      Global Instance I `(Trait) : OtherTrait AssocTy.
      repeat (destruct __the_bounds_of_AssocTy as [? __the_bounds_of_AssocTy]; try assumption).
    End OtherTrait.
  End The_Bounds_Of_AssocTy.

The problem I tried to solve in this PR was that sometimes traits have supertraits, that are translated into superclasses which are just parameters of the class constructor.
Because they are parameters they have to be provided in order to use the class constructor in place of the type in instance definition:

Global Instance name : (* here *) := ... .

but because the only instance of the class avaliable to us is the one in a field of another class we have to extract them first.

My solutoin to that is to use tactics to automatically write the type of the instance we want to define, so an instance of OtherTrait AssocTy would be defined in the following way:

Global Instance I `(_Tr : Trait) : ltac:(unshelve eapply (OtherTrait (AssocTy (Trait := _Tr)));
  compute;
  destruct _Tr;
  repeat
    destruct
    (__the_bounds_of_AssocTy0
    as
    [? __the_bounds_of_AssocTy0];
    try assumption)).
  all:
    compute;
    destruct _Tr;
    repeat
      (destruct __the_bounds_of_AssocTy0 as [? __the_bounds_of_AssocTy0]);
    assumption.
Defined.

Unfortunately, it slows down the compilation by Coq and eats all the avaliable memory.
Another problem with it is that, although that code creates instances of desired classes (what I checked with

Check I ?[H] : OtherTrait (AssocTy (Trait := H)).

) Coq still doesn't apply this instance in places where it is necessary.

Unfortunatelly I wasn't able to find a better solution.
I uploaded the file in which I was testing out different solutions and marked the place that simulates the problem.
It may serve as a further clarification of what I am trying to do.
It is named experiment.v and I put it in tmp directory.

[bartlomiejkrolikowski]

I tried to use tactics to automatically extract instances (with instances of related superclasses) related to associated types from other instances.
Unfortunatelly, in the current state my computer runs out of memory during compilation and I currently run out of ideas.