Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

F* translation for trait inheritance is buggy #630

Closed
1 of 2 tasks
karthikbhargavan opened this issue Apr 24, 2024 · 3 comments · Fixed by #902 · May be fixed by #910
Closed
1 of 2 tasks

F* translation for trait inheritance is buggy #630

karthikbhargavan opened this issue Apr 24, 2024 · 3 comments · Fixed by #902 · May be fixed by #910
Labels
bug Something isn't working engine Issue in the engine f* F* backend

Comments

@karthikbhargavan
Copy link
Contributor

karthikbhargavan commented Apr 24, 2024 •
edited by W95Psp
Loading

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 GitHub Actions
Copy link

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 github-actions bot added the stale label Aug 30, 2024
@github-actions GitHub Actions
Copy link

github-actions bot commented Sep 6, 2024

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.

@github-actions github-actions bot closed this as not planned Won't fix, can't repro, duplicate, stale Sep 6, 2024
@github-project-automation github-project-automation bot moved this to Done in hax Sep 6, 2024
@W95Psp
Copy link
Collaborator

W95Psp commented Sep 16, 2024 •
edited
Loading

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.

@W95Psp W95Psp reopened this Sep 16, 2024
@W95Psp W95Psp added bug Something isn't working engine Issue in the engine f* F* backend and removed stale labels Sep 16, 2024
@W95Psp W95Psp mentioned this issue Sep 23, 2024
Merged
W95Psp added a commit that referenced this issue Sep 23, 2024
@W95Psp
fix(engine/fstar): fix super typeclasses attributes
725d5f4 
The PR #902 was reverted by #909 because #902 was generated redundant
fields names in classes for super clauses, which is a problem for F*.

This PR changes the naming scheme of super clauses for typeclasses in
F*. Those names now take into account the trait name. The super trait
names are now a 5 characters base 62 encoding of the hash of the
predicate ID concatenated with the trait name.

Fixes #630.
@W95Psp W95Psp mentioned this issue Sep 23, 2024
Draft
W95Psp added a commit that referenced this issue Sep 23, 2024
@W95Psp
fix(engine/fstar): fix super typeclasses attributes
66a1a6e 
The PR #902 was reverted by #909 because #902 was generated redundant
fields names in classes for super clauses, which is a problem for F*.

This PR changes the naming scheme of super clauses for typeclasses in
F*. Those names now take into account the trait name. The super trait
names are now a 5 characters base 62 encoding of the hash of the
predicate ID concatenated with the trait name.

Fixes #630.
W95Psp added a commit that referenced this issue Sep 23, 2024
@W95Psp
fix(engine/fstar): fix super typeclasses attributes
994b9c0 
The PR #902 was reverted by #909 because #902 was generated redundant
fields names in classes for super clauses, which is a problem for F*.

This PR changes the naming scheme of super clauses for typeclasses in
F*. Those names now take into account the trait name. The super trait
names are now a 5 characters base 62 encoding of the hash of the
predicate ID concatenated with the trait name.

Fixes #630.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
bug Something isn't working engine Issue in the engine f* F* backend
Projects
None yet
Milestone
No milestone
2 participants
@W95Psp @karthikbhargavan