Make embedders use an error monad.
Make embedders use an error monad.

It is problematic when embedders fail while printing error messages.
So, I put the embedders in an error monad.  However, there aren't
really any "important" errors in the embedders: I thought the one for
free variables was important (the 'NVar' case of 'embedN''), because
it could be due to DeBruijn errors, but then I realized it also
happens for (DeBruijn correct) open terms :P

So, what we really need to do is handle the free variables correctly.
The approaches that come immediately to mind are:

1. take the free variables into account when alpha renaming bound
variables.

2. return a substitution, in addition to the embedded term.

It seems (1) is much easier to work worth, so I'll try that ... since
I'm already in a monad, it's easy to add another 'Reader' field, for
the free variables.

For the hypothetical problem of pretty printing itself, when DeBruijn
errors mess up the embedding, a better solution is probably the many
pretty printers I had before, which didn't use embedding: this way we
would be able to pretty print while debugging DeBruijn errors.

More details about the problem we need to address: When going from
DeBruijn to names, the canonical embedders ('embedV', 'embedN') must
sometimes create fresh variables ('extendIdents').  However, this
freshness check is not done w.r.t. the free variables in the original
term, but only w.r.t. the enclosing binders.

E.g., consider the term, which has a free occurrence of x' (x'2):

  \x. \x. (x0 , x'2)

When going from DeBruijn to names, we freshen (using 'extendIdents')
to:

  \x. \x'. (x'0 , <<free variable error>>)

and so it would *not* be safe to instead replace the fresh variable
with it's name, since it would be captured:

  \x. \x'. (x'0 , x'2)

And actually, this example is overly complicated, e.g. we may have
already captured a free variable (name) when (safely DeBruijn)
substituting.  E.g., evaluting

  (\x. \y. x1) y0 ~> (\y. y1)

captures the (name of the) free y.

spire/spire