Help compiling simple finally tagless DSL

Stream: lean4

[Mario Carneiro]

/me moved the conversation so the link above is now dead

[Alexander Bentkamp]

https://leanprover.github.io/lean4/doc/autobound.html
"any unbound identifier is automatically added as an implicit argument if it is a single lower case or greek letter"

[Alexander Bentkamp]

Apparently you can switch the feature off with set_option autoBoundImplicitLocal false if you don't like it.