Fix typo
Implement Sec. 4.1-4.2
Mark more boilerplate as such
Add extra example
Implement Sec. 4.3 & add Cabal file
Implement Sec. 5
Implement Sec. 6.1 and parts of 6.2
Implement 6.2 + omitted code
Start implementing Sec. 7
Finish Sec. 7 with UndecidableInstances

That seems required, even though it seems to not be mentioned by the
paper.
Implement Sec. 8
Segregate code requiring UndecidableInstances
Sketch an implementation of zippers for Syntactic

This is almost great! I only need some HList to complete the job.
Remove existentials from Syntactic Zippers

Using HList worked exactly as planned, though I initially made some
small mistakes in applying the idea.
Refactor

Inline subcases of goUp: they were only there because I didn't like the
type for the main function.
Finish implementation of zippers

Now this adds goFirst and goSecond, completing the implementation of
Sec. 3.2 of Huet's "Zipper" paper.

However, both functions need to return an existential (which I encode
through CPS), which is slightly annoying. This time however there is no
easy fix, since the needed type is just not known (until we look). The
complicated fix would be to index the tree by a tree of types of the
various members, encoding essentially the "typing derivation" for the
correctness of the tree (in the metalanguage). However, that does not
look trivial.
Allow representing a zipper as a context "list"

Instead of having an inductive datatype for representing a zipper, we
can also use a "list" of the various fragments. Due to the type indexes,
we can't use a standard list but we need something fancier.

To show that we got this right, "prove" the equivalence of the two
representations by defining an isomorphism between the two.

I must say, I am positively amazed by how well GHC supported me in this
task. Agda has still the upper hand with its better tool support, but
writing this code was too much fun.
Translate zippers API to zipper lists

Now we have both available. The translation was really easy, but zipper
lists require a fixed bit more ceremony because one needs to write both
constructors.
Replace symbols with UnicodeSyntax equivalents

Commands:

gsed -i'' -e 's/->/→/g' src/*.hs
gsed -i'' -e 's/=>/⇒/g' src/*.hs
gsed -i'' -e 's/forall/∀/g' src/*.hs

(gsed is GNU sed).
More UnicodeSyntax: also :: ↦ ∷

More precisely, to avoid affecting (:::), I used:

$ gsed -i'' -re 's/([^:])::([^:])/\1∷\2/g' src/*.hs