Skip to content
This repository has been archived by the owner on Oct 18, 2021. It is now read-only.

Default methods not visited in Verify #254

Open
SquidDev opened this issue Dec 29, 2019 · 2 comments
Open

Default methods not visited in Verify #254

SquidDev opened this issue Dec 29, 2019 · 2 comments
Labels
bug Verify Issues/PRs concerning the rest of the verifier

Comments

@SquidDev
Copy link
Member

Default methods within type classes are not visited within the verify pass, meaning that potential problems are not detected:

let id x = x

class bifunctor 'f
  val bimap : ('a -> 'a₂) -> ('b -> 'b₂) -> 'f 'a 'b -> 'f 'a₂ 'bval first : ('a -> 'a₂) -> 'f 'a 'b -> 'f 'a₂ 'b
  let first f = let unused = () (* Should warn but doesn't *)
                bimap f id

More seriously, this will not reject ill-formed terms such as let x = x within default methods.

@SquidDev SquidDev added bug X-soundness Soundness bugs. Verify Issues/PRs concerning the rest of the verifier labels Dec 29, 2019
@plt-amy
Copy link
Member

plt-amy commented Dec 29, 2019

It's not a soundness bug, default methods are not shared. They're pasted into instance bodies and will get verified there

@SquidDev SquidDev removed the X-soundness Soundness bugs. label Dec 29, 2019
@SquidDev
Copy link
Member Author

SquidDev commented Jan 2, 2020

Fixing this would also allow us to remove this disaster:

(* use inside classes doesn't count for verify *)
let _ = (swap, dup)

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
bug Verify Issues/PRs concerning the rest of the verifier
Projects
None yet
Development

No branches or pull requests

2 participants