F* translation for trait inheritance is buggy

[karthikbhargavan]

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.

[github-actions]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[github-actions]

This issue has been closed due to a lack of activity since being marked as stale. If you believe this issue is still relevant, please reopen it with an update or comment.

[W95Psp]

The issue regarding super fields missing tcinstance attributes is still relevant, here is a repro in the playground:

trait A {}
trait B {}
trait T: A + B {}

impl A for () {}
impl B for () {}
impl T for () {}

Open this code snippet in the playground

The other bug is fixed.