Higher-order bindings in DSLs fail to shadow.

[Stoicheion]

module Lambda

import public Data.Fin

%access export

||| The base cases of Term used to end the recursion.
public export
data BaseTerm : Type -> (ctxt : Nat) -> Type where
  ||| A abstract (free) variable which doesn't depend on the context for
  ||| interpretation. Could be anything from meta variables/placeholders
  ||| in an incomplete program to even constants. Use "Void" as the type
  ||| to only allow construction of closed terms.
  Free : a -> BaseTerm a ctxt
  ||| A normally bound variable (reference to some binder) which can
  ||| dangling (free) if context allows.
  Ref : Fin ctxt -> BaseTerm a ctxt

||| A abstract representation of lambda calculus terms. Intended usage
||| involves using a string type for "id" if named terms are desired
||| or "()" (Unit) if nameless terms are wanted.
public export
data Term : Type -> Type -> (ctxt : Nat) -> Type where
  ||| A leaf node (usually containing bound variables) which contains data
  ||| which may depend on the context for correct interpretation.
  Leaf : BaseTerm fr ctxt -> Term id fr ctxt
  ||| A lambda abstraction containing a term with the same context + 1 more binder
  ||| in context.
  Lam : id -> Term id fr $ S ctxt -> Term id fr ctxt
  App : Term id fr ctxt -> Term id fr ctxt -> Term id fr ctxt

%name BaseTerm x, y, z
%name Term t, u, s, p, q, r
%name Fin n, m, i, j, k

||| A Term having "ctxt" = 0 ensures that there are no dangling references embedded within.
public export
ClosedBound : Type -> Type -> Type
ClosedBound id = flip (Term id) 0

||| A Term having "ctxt" = S _ ensures that the *maximum* number of dangling unique references
||| embedded within is greater than 0. There need not be any dangling references, however.
public export
OpenBound : Type -> Type -> Nat -> Type
OpenBound id fr p@(S _) = Term id fr p
OpenBound _ _ Z = Void

||| A Term with a "closed bound" using higher-order variable bindings.
public export
HTerm : Type -> Type
HTerm fr = ClosedBound TTName fr

mkLam : TTName -> Term TTName fr $ S p -> Term TTName fr p
mkLam x body = Lam x body

dsl term
  variable    = Leaf . Ref
  index_first = FZ
  index_next  = FS
  lambda      = mkLam

test0 : HTerm Void
test0 = term (\x => (\x => (\x => x)))

idris version 0.12.3 "x" in the body of "test0" refers to the outermost binder of "x" instead of the innermost.

[Melvar]

The code for desugaring binders in the dsl works from outside to inside, for each binder replacing all matching variables in its scope with de Bruijn indices. It does not stop at binders which bind the same variable, so in all every variable is associated to the outermost binder with a matching name. Relevant variable-replacing code.