HB commands telescope inferrence is dumb about hierarchy-builder HOT 4 CLOSED

Also, it does not (always?) take into account Implicit Types

from hierarchy-builder.

I think we can do better for builders, but not in general.

• Context P1 P2 T of F ... here I think we know that F ... must type in this exact context.
• Record foo P1 P2 T of F1 ... & F2 ... are we sure F1 ... and F2 ... typecheck? I guess so for F1 ... but maybe F2 has phantom arguments on T requiring F1's provides to be loaded.

Am I right?

from hierarchy-builder.

This is also true in the simple case:

HB.factory Record Ring_of_AddComoid A of AddComoid A := {
  opp : A -> A;
  one : A;
  mul : A -> A -> A;
  addNr : left_inverse zero opp add;
  mulrA : associative mul;
  mul1r : left_id one mul;
  mulr1 : right_id one mul;
  mulrDl : left_distributive mul add;
  mulrDr : right_distributive mul add;
}.

HB.builders Context A (a : Ring_of_AddComoid A).

Here Ring_of_AddComoid A is not well typed unless you first postulate the requires of the factory.

from hierarchy-builder.

bottom line, just typing F Params T is not good, one should at least prune the id_phant

from hierarchy-builder.