Inference rules in type class resolution

Stream: lean4

[Henrik Böving]

I'm currently trying to port the code from here https://github.com/leanprover-community/mathlib/blob/master/src/testing/slim_check/sampleable.lean and this is what I've come up with so far:

import Mathlib.Testing.SlimCheck.Gen

namespace SlimCheck

abbrev shrinkFn (α : Type u) [sz : SizeOf α] := (x : α) → List { y : α // sz.sizeOf y < sz.sizeOf x}

class Sampleable (α : Type u) where
  [wf : SizeOf α]
  sample : Gen α
  shrink : shrinkFn α := λ _ => []

class SampleableFunctor (f : Type u → Type v) extends Functor f where
  [wf (α : Type u) [SizeOf α] : SizeOf (f α)]
  [repr (α : Type u) [Repr α] : Repr (f α)]
  sample : Gen α → Gen (f α)
  shrink [SizeOf α] : shrinkFn α → shrinkFn (f α)

class SampleableExt (α : Sort u) where
  proxyRepr : Type v
  [wf : SizeOf proxyRepr]
  interp : proxyRepr → α -- TODO what does the trivial interp do here
  [pRepr : Repr proxyRepr]
  sample : Gen proxyRepr
  shrink : shrinkFn proxyRepr

instance SampleableExt.ofSampleable {α : Type u} [Sampleable α] [Repr α] : SampleableExt α :=
  SampleableExt.mk α id Sampleable.sample Sampleable.shrink

end SlimCheck

Just a little remark before I explain my issue: As far as I understand the SizeOfsystem every type gets a SizeOf instance thats just fun _ => 0 per default, the inductive compiler is however very much capable of generating sensible instances but you have to explicitly let the type class system pass them to you by carrying all these explicitly mentioned SizeOf instances around. This understanding is based on the fact that:

def foo {α : Type u} (x : α) : Nat := sizeOf x
#eval foo 12

evals to 0 but:

def bar {α : Type u} [SizeOf α] (x : α) : Nat := sizeOf x
#eval bar 12

evals to 12, the correct value. Is my understanding based on this observation correct?

Now to my actual questions:

1. https://github.com/leanprover-community/mathlib/blob/master/src/testing/slim_check/sampleable.lean#L159 what does this syntax do here? It appears the author basically wrote a trivial "custom inference producedure" for this value here? How does this work? What is the correct way to do stuff like this in Lean 4?
2. When defining the rather trivial SampleableExt of Sampleable instance in the above manner the compiler will throw a:

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  instSizeOf α
inferred
  Sampleable.wf

at me. Now I suspect this is due to the priority stuff that is explicitly set in the file via attributes and I guess I could just change the priorities in the same way and cross fingers that the typeclass inference will work out but I actually want to understand what's going on here and how to fix it

[Simon Hudon]

1. (interp [] : proxy_repr → α . sampleable.mk_trivial_interp) invokes a tactic to create that function. I think you would write the same as interp : proxy_repr → α := by sampleable.mk_trivial_interp in Lean 4

[Simon Hudon]

2. Can you narrow down which field it throws that error at? For instance, comment out one declaration after another

[Simon Hudon]

Btw, if ShrinkFn gets awkward to use, you could consider making that type into a structure with fn : a -> List a and separately a proof that fn only creates objects that are smaller that the argument.