Fix bug in embedding from DeBruijn to named var represenations.
Fix bug in embedding from DeBruijn to named var represenations.

@larrytheliquid I believe this implementation is correct, but then
I've uncovered another, unknown, capture bug: the definition of
substitution for DeBruijn terms is wrong, because the term being
substituted is not weakened when going under a binder. I will fix this
tomorrow, assuming you agree that I've identified the problem.

I believe the problem is `subExtend`, in
`Spire.Canonical.HereditarySubstitution`:

  subExtend :: Var -> Val -> Bound Val -> Bound Val
  subExtend i x (Bound (l , a)) = Bound (l , subV (succ i) x a)

It should instead be

  subExtend i x (Bound (l , a)) = Bound (l , subV (succ i) (weaken1 x) a)

where `weaken1 x` is a weakening function that increments free
variables in `x` by 1.  Alternatively, and much more efficiently, we
could probably change the first case of `subN`:

  subN :: Var -> Val -> Neut -> Val
  subN i x (NVar (NomVar (l , j))) | i == j = x

to:

  subN i x (NVar (NomVar (l , j))) | i == j = weaken (succ i) x

where now `weaken i x` is a function that increments free variables in
`x` by `i`.  The idea is that `i` counts how many binders we went
under since the substitution started, since we always start at
`i = 0`.

Probably unrelated, I don't understand the second case of `subN`, but
it seems suspicious:

  subN i x (NVar (NomVar (l , j))) | i < j = Neut (NVar (NomVar (l , (j - succ i))))

It seems that the `j - succ i` should be `pred j`! Here is an example
of the problem, where xk stands for the variable `NVar (NomVar (x , k))`:

  \ x -> (\ y -> \ z . x2) tt    ~>
  \ x -> subN 0 tt (\ z . x2)    ~>
  \ x -> \ z -> (subN 1 tt x2)   ~>
  \ x -> \ z -> x0

because `0 = 2 - (succ 1)`, but here the correct answer is

  \ x -> \ z -> x1

where `1 = pred 2`.  I will add this to the capture examples.

spire/spire