Why cant i instance this class?

Stream: new members

[lorã]

inductive MyNat where
  | zero
  | succ (n : MyNat)
set_option diagnostics true

instance : ToString MyNat where
  toString
    | MyNat.zero => "O"
    | MyNat.succ n => "S " ++ toString n

[lorã]

It keeps bringing me error

[lorã]

But why? The option diagnostics was not very helpful

[Yan Yablonovskiy 🇺🇦]

lorã said:

inductive MyNat where
  | zero
  | succ (n : MyNat)
set_option diagnostics true

instance : ToString MyNat where
  toString
    | MyNat.zero => "O"
    | MyNat.succ n => "S " ++ toString n

Certainly weird, i can see that if you do

def string_of_MyNat: MyNat → String
| MyNat.zero => "0"
| (MyNat.succ) n =>  "S " ++ string_of_MyNat n

#eval string_of_MyNat (MyNat.zero)


instance : ToString MyNat where
  toString
    | MyNat.zero => string_of_MyNat MyNat.zero
    | (MyNat.succ) n => string_of_MyNat n

seems to work, so i think it must be a particularity of the type class variables / equation compiler, since the toString takes in a class argument

I guess that only answers "How" you might instance that , not "Why" you can't do it that way. But its something.

[lorã]

i would also like to know why

[Yan Yablonovskiy 🇺🇦]

lorã said:

i would also like to know why

A brief look at
https://leanprover.github.io/reference/declarations.html?highlight=equation%20compiler

Seems to say that equation compiler is syntactic sugar for using MyNat.below, MyNat.ibelow.

I guess in that setting, the equation compiler must also recognise its in an instance and construct instances using those functions.

There wasn't much in the reference about equation compiler, i think this might be a fairly technical reason.

If you use core lean without equation compiler, using recOn with an appropriate motive, it could work.

Edit:

instance : ToString MyNat where
 toString := fun n:MyNat => by
  apply MyNat.recOn (motive := fun n:MyNat ↦ String) n (zero := "0")
  intro k S
  exact ("S " ++ S)

has a different error, and seems to be constructed fine. It has "code generator does not support recursor 'MyNat.recOn' yet, consider using 'match ... with' and/or structural recursion"

I think my next reply has the reason finally.. was a journey.

[Yan Yablonovskiy 🇺🇦]

lorã said:

i would also like to know why

I think i finally found why:
https://lean-lang.org/doc/reference/latest///Type-Classes/Instance-Declarations/#recursive-instances

"The standard idiom to work around this limitation is to create a local instance in a recursively-defined function that includes a reference to the function being defined, taking advantage of the fact that instance synthesis may use every binding in the local context with the right type."

It has an example of the exact same error you are seeing, including lack of synth log i think.