Help compiling simple finally tagless DSL (cross-posted)

Stream: lean4

[Yuri de Wit]

I posted to general by mistake so just leaving a link to the original topic:

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Help.20compiling.20simple.20finally.20tagless.20.20DSL

The only thing still puzzling to me is that I get an error message depending on the length of the type variable in the t function definition.