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.

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

Engine: F*: impl missing bounds on trait generic types #1144

Open
W95Psp opened this issue Nov 27, 2024 · 0 comments
Open

Engine: F*: impl missing bounds on trait generic types #1144

W95Psp opened this issue Nov 27, 2024 · 0 comments
Labels
backend Issue in one of the backends (i.e. F*, Coq, EC...) bug Something isn't working engine Issue in the engine f* F* backend

Comments

@W95Psp
Copy link
Collaborator

W95Psp commented Nov 27, 2024

The following Rust snippet:

trait TraitA {}
trait TraitB<T: TraitA> {}

impl TraitA for () {}
impl TraitB<()> for () {}

Open this code snippet in the playground

Extracts to the following F*:

class t_TraitA (v_Self: Type0) = {
  __marker_trait_t_TraitA:Prims.unit
}

[@@ FStar.Tactics.Typeclasses.tcinstance]
let impl_TraitA_for_tuple_: t_TraitA
Prims.unit = { __marker_trait = () }

class t_TraitB
  (v_Self: Type0) (v_T: Type0)
  = {
  [@@@ FStar.Tactics.Typeclasses.no_method]_super_9060164045790606315:t_TraitA
  v_T
}

[@@ FStar.Tactics.Typeclasses.tcinstance]
let impl_1: t_TraitB Prims.unit Prims.unit =
  { __marker_trait = () }

impl_1 lacks a super field.

@W95Psp W95Psp added backend Issue in one of the backends (i.e. F*, Coq, EC...) bug Something isn't working engine Issue in the engine f* F* backend labels Nov 27, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
backend Issue in one of the backends (i.e. F*, Coq, EC...) bug Something isn't working engine Issue in the engine f* F* backend
Projects
None yet
Development

No branches or pull requests

1 participant