F* translation for trait inheritance is buggy

[karthikbhargavan]

trafficstars

traits of the form:

trait T: A + B {
}

get translated to

class T  (v_Self:Type) = {
  [@@@ FStar.Tactics.Typeclasses.no_method]_super_16550665238208597986:t_A v_Self;
  [@@@ FStar.Tactics.Typeclasses.no_method]_super_9181983936900423582:t_B  v_Self;
  }

and its instances are of the form:

[@@ FStar.Tactics.Typeclasses.tcinstance]
let impl: t_T t_foo =
  {
    _super_16550665238208597986 = FStar.Tactics.Typeclasses.solve;
    _super_9181983936900423582 = FStar.Tactics.Typeclasses.solve;
    __marker_trait = ()
  }

This has two issues:

• in the class, the attribute on the _super values should be [@@ FStar.Tactics.Typeclasses.tcinstance]
• in the impl, there should be no __marker_trait or else this field should be declared in the class.