Could not solve typeclass constraint

[franziskuskiefer]

use hax_lib::*;

trait Op {
   fn x() -> Self;
   fn y() -> Self;
}

struct S {}

impl Op for S {
   fn x() -> Self {
      S{}
   }

   fn y() -> Self {
      Self::x()
   }
}

Open this code snippet in the playground

* Error 228 at Playground.fst(58,9-58,40):
  - Could not solve typeclass constraint `Playground.t_Op Playground.t_S`
  - See also FStar.Tactics.Typeclasses.fst(297,6-300,7)
1 error was reported (see above)
make[1]: *** [Makefile:79: Playground.fst.checked] Error 1
make: *** [Makefile:12: all] Error 2

[github-actions[bot]]

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[bot]]

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.

[W95Psp]

Related to https://github.com/cryspen/hax-evit/issues/24

[github-actions[bot]]

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.

[clementblaudeau]

Still relevant, and also present in the Lean backend. The workaround is to extract the functions (at least x) out of the impl :

use hax_lib::*;

trait Op {
   fn x() -> Self;
   fn y() -> Self;
}

struct S {}

fn impl_Op_S_x() -> S {
   S {}
}

impl Op for S {
   fn x() -> Self {
      impl_Op_S_x()
   }

   fn y() -> Self {
      impl_Op_S_x()
   }
}

Open this code snippet in the playground