unable to synthesize 'MonadEval' instance

Stream: new members

[aron]

Lean won't let me eval this code

def inferTypeFromPatterns (patterns : List Pattern) : Except IncompatibleTypes Universe := ...

instance [ToString IncompatibleTypes] : MonadEval (Except IncompatibleTypes) IO where
  monadEval m := IO.ofExcept m

#eval inferTypeFromPatterns patternsListOfList

because of error:

unable to synthesize 'MonadEval' instance to adapt
  Except IncompatibleTypes Universe
to 'IO' or 'Lean.Elab.Command.CommandElabM'.

even though I have explicitly implemented a MonadEval instance for Except IncompatibleTypes? What's the problem here?

Screenshot 2025-01-15 at 00.36.39.png

[Kyle Miller]

Do you have a ToString IncompatibleTypes instance?

[aron]

Yes I do

structure IncompatibleTypes where
  t1 : Universe
  t2 : Universe

instance [ToString Universe] : ToString Universe where
  toString :=
    fun u =>
      match u with
      | Universe.unit => "()"
      | Universe.option u => "Option " ++ toString u
      | Universe.result ok err => "Result " ++ toString ok ++ " " ++ toString err
      | Universe.list u => "List " ++ toString u
      | Universe.any => "*"

instance [ToString Universe] : ToString IncompatibleTypes where
  toString := fun e =>
      "Incompatible types: " ++ toString e.t1 ++ " and " ++ toString e.t2

[Kyle Miller]

instance [ToString Universe] : ToString Universe doesn't work as a way to define that instance. You should be able to check that #synth ToString Universe fails, or you should observe that if you apply toString to a term of Universe there will be an error.

Instead, you should define a recursive function first that creates that string, and then you can define the instance with it, without this [ToString Universe] argument.

If you posted a #mwe, I might have had a moment to write it and test that it worked.

[aron]

Ah ok that makes sense, yes. I did instance [ToString Universe] : ToString Universe because it it insisted that Universe needed to be an instance of ToString, otherwise it didn't let me call toString on it recursively

But this now works!