Yeah, but I realise now I could have simply used fmap.

Sure, you can encode the Term type as a final coalgebra as well, but this is not what the "tagless final" encoding does. The "tagless final" thing is just the usual impredicative/CPS/Church/... encoding of an initial algebra (see for example: http://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt).

Indeed, the authors say that they are using the coalgebraic structure, so they do mean "final" in the conventional sense. I'm really confused by this statement, though, as I don't see any coalgebra in the encoding. Ignoring the indexing, which is inessential, the type class Language r specifies an algebra f r -> r, where f is a functor obtained as a coproduct of a bunch of simple functors corresponding to the various algebra operations. The type forall r . Language r => r then corresponds exactly, via the dictionary translation, to the encoding of initial algebras developed in the above note by Wadler.

A real final encoding would consist of a coalgebra for an existential type s, together with a "seed" value of type s. This is also explained later in the same note. This kind of encoding is used a lot in the context of "fusion": see for example http://hackage.haskell.org/package/stream-fusion.

This was fun, thanks :)

I'm confused by the naming, though. Why is this called "final"? An instance of Language r is exactly an (indexed) algebra for the signature of the language, and the type forall r . Language r => r h a is the usual encoding of an initial algebra. So why is this final as opposed to initial? Does the paper explain the choice of terminology? I couldn't find an explanation there.

I had to change my Haskell solution to a simple visit of the tree, since the test cases are testing the wrong thing. It seems that the tests are working under the assumption that buildTree and treeByLevels are inverses, but this is not the case. This should be fixed.