Description
In the refactoring to get instances before structure declaration, one must be careful to distinguish the two kinds of parameters.
Mixin parameters of an instance are the parameters that occur in the type of the mixin (as arguments of mixins), anything is allowed since anything can be inferred by type inference. However, instance parameters, which are the parameters of instances that do not occur in mixin arguments are only inferable if they are part of a resolution mechanism (HB or in mixed cases hand made declared CS or typeclass instances, which we should not care about in a first pass).
In the following example, P is a mixin parameter while T is an instance parameter.
HB.mixin Record is_foo P A := { op : P -> A -> A}.
HB.instance Definition foo_nat P := is_foo.Build P nat (fun _ x => x).
HB.instance Definition foo_list P T := is_foo.Build P (list T) (fun _ x => x).
When applying mixin-src->has-mixin-instance we should examine each parameter of the mixin instance and decide which is a mixin parameter and which is an instance parameter and write down their number encode it as a list of booleans for use in mk-src