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

Type-class implicits are not eager enough #183

Open
gebner opened this issue Aug 22, 2024 · 0 comments
Open

Type-class implicits are not eager enough #183

gebner opened this issue Aug 22, 2024 · 0 comments

Comments

@gebner
Copy link
Contributor

gebner commented Aug 22, 2024

When a function has a final type-class argument, then F* will apply it (and solve it via type-class search), but Pulse will not:
 

module TCArg
open Pulse
#lang-pulse

class droppable (p: slprop) = {
  drop_: stt unit p (fun _ -> emp)
}

let drop (p: slprop) {| droppable p |} = drop_ #p

instance droppable_emp : droppable emp = { drop_ = return_stt_noeq _ _ }

let foo_in_fstar = drop emp // works

fn foo_in_pulse () requires emp ensures emp {
(*
Expected type unit
  but drop emp
  has type {| _: droppable emp |} -> stt unit emp (fun _ -> emp)
*)
  drop emp; // doesn't work
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant