Failed to synthesize instance ToString Term

Stream: lean4

[Yuri de Wit]

I am getting an error trying to define the ToString instance of my Term here: Failed to synthesize instance ToString Term.

Does this just mean I can't define the ToString instance and used it at the same time and that I need to extract the toString logic as a separate definition?

inductive Term where
  | Var (name : String)
  | Dup (nam0 : String) (name1 : String) (expr : Term) (body : Term)
  | Let (name : String) (expr : Term) (body : Term)
  | Lam (name : String) (body : Term)
  | App (func : Term) (argm : Term)
  | Ctr (name : String) (args: Array Term)
  | U32 (numb : UInt64)
  | Op2 (oper : Operation) (val0 : Term) (val1 : Term)

instance : ToString Term where
  toString
  | Term.Var n => s!"{n}"
  | Term.Dup n0 n1 e b => s!"dup {n0} {n1} = {e} {b}"
  | Term.Let n e b => s!"let {n} = {e}; {b}"
  | Term.Lam n b => s!"λ{n} {b}"
  | Term.App f a => s!"({f} {a})"
  | Term.Ctr n a => s!"{n}"
  | Term.U32 n => s!"{n}"
  | Term.Op2 op v0 v1 => s!"({op} {v0} {v1})"

instance : ToString Term where
  toString
  | Term.Var n => s!"{n}"
  | Term.Dup n0 n1 e b => s!"dup {n0} {n1} = {e} {b}"
  | Term.Let n e b => s!"let {n} = {e}; {b}"
  | Term.Lam n b => s!"λ{n} {b}"
  | Term.App f a => s!"({f} {a})"
  | Term.Ctr n a => s!"{n}"
  | Term.U32 n => s!"{n}"
  | Term.Op2 op v0 v1 => s!"({op} {v0} {v1})"

[Alexander Bentkamp]

I seems that you can't. Here's a hack that allows you to use the s! notation recursively:

partial instance : ToString Term where
  toString :=
    let rec toStr x :=
      have : ToString Term := ⟨toStr⟩
      match x with
      | Term.Var n => s!"{n}"
      | Term.Dup n0 n1 e b => s!"dup {n0} {n1} = {e} {b}"
      | Term.Let n e b => s!"let {n} = {e}; {b}"
      | Term.Lam n b => s!"λ{n} {b}"
      | Term.App f a => s!"({f} {a})"
      | Term.Ctr n a => s!"{n}"
      | Term.U32 n => s!"{n}"
      | Term.Op2 op v0 v1 => s!"({op} {v0} {v1})"
    toStr

But it only gives you a partial instance. Maybe you can prove it terminating somehow, but I don't know how.

[Yuri de Wit]

Thank you!

So, even though there are a few cases that are not recursive, the inductive type can always be infinite. It seems that unless I can add some sort of tree height check or something like that I would never be able to prove termination (assuming I understand your point correctly)

In this case, shouldn't partial be enough to define my instance without the alternative you provided?

[Alexander Bentkamp]

Since the recursive calls occur only on smaller terms, it should be possible to somehow prove termination, I just don't know how.

[Alexander Bentkamp]

Should partial be enough to do the job? I don't know. Currently, the new instance gets registered only when the command is completed. Maybe the instance command could be extended to allow this recursive behavior.