update code using Plausible

Stream: general

[Asei Inoue]

this code did work in v4.24.0 but breaks in v4.25.0-rc2

import Plausible

open Plausible

inductive MyNat where
  | zero
  | succ (n : MyNat)
deriving Repr

def MyNat.shrink : MyNat → List MyNat
  | zero => []
  | succ n => n :: n.shrink

instance : Shrinkable MyNat where
  shrink := MyNat.shrink

def MyNat.ofNat : Nat → MyNat
  | 0 => zero
  | n + 1 => succ (ofNat n)

open SampleableExt in

instance : SampleableExt MyNat := mkSelfContained do
  let x ← SampleableExt.interpSample Nat
  return MyNat.ofNat x

/- (kernel) application type mismatch
  Arbitrary.arbitrary
argument has type
  Arbitrary (SampleableExt.proxy MyNat)
but function has type
  [self : Arbitrary MyNat] → Gen MyNat -/
#sample MyNat

How to fix this?

[Henrik Böving]

CC @Cody Roux seems likely to me that the recent refactoring broke this. Would you like to fix it + add a test or should I?

[Cody Roux]

If you have time to fix it, great! I'm actually not sure what's happening here; did I mess up the mkSelfContained too opaque or is the SampleableExt instance from Arbitrary wrong?

As a side note: should we deprecate mkSelfContained in favor of directly defining Arbitrary? That way we encourage using deriving etc (which, I just noticed, is not included by default on import Arbitrary, also my bad)

[Henrik Böving]

If you have time to fix it, great! I'm actually not sure what's happening here; did I mess up the mkSelfContained too opaque or is the SampleableExt instance from Arbitrary wrong?

None of that, you just didn't update the #sample elaborator and we had no test for it, i'll fix it

[Cody Roux]

Oh whew

[Cody Roux]

Thanks, I can do it a bit later if you don't get to it

[Henrik Böving]

Hm, when I try it in a local plausible checkout it very much does work though. Maybe this is because of the currently broken cache and just a transient issue

[Cody Roux]

Works for me too at the moment.

[Cody Roux]

As does (happily) deriving Arbitrary