amuletml / amulet

An ML-like functional programming language
https://amulet.works/
BSD 3-Clause "New" or "Revised" License
324 stars 14 forks source link

Default methods not visited in Verify #254

Open SquidDev opened 4 years ago

SquidDev commented 4 years ago

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₂ 'b₂

  val 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.

plt-amy commented 4 years ago

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

SquidDev commented 4 years ago

Fixing this would also allow us to remove this disaster:

https://github.com/amuletml/amulet/blob/7d2f15a08dee8461bfb044a05caa10f5f30a51de/lib/amulet/category.ml#L50-L51