Example in widget docs doesn't work

[bryangingechen]

The following was reported on Zulip by @SnobbyDragon. This example from https://leanprover-community.github.io/mathlib_docs/init/meta/widget/basic.html doesn't work:

meta def Hello : component string empty := component.pure (λ s, ["hello, ", s, ", good day!"])
#html Hello "lean" -- renders "hello, lean, good day!"

maximum class-instance resolution depth has been reached
(the limit can be increased by setting option 'class.instance_max_depth')
(the class-instance resolution trace can be visualized by setting option 'trace.class_instances')

@EdAyers commented:

So the problem is that when you write Hello "lean", there is a function coercion, but the typeclass inference system is getting stuck in a loop for some reason. I suggest that you just use the clunkier version with html.of_component for now. Maybe someone who actually understands typeclasses knows what needs to change to get this to work.

[EdAyers]

I think that the actual problem was that the coe_to_fun got removed at some point... oops.