Remembering the binder name when there is no occurrence

[Ptival]

Hey, I've been using bound for quite a while for a personal project, and it satisfies almost all of my needs, except for one issue.

The family of abstractName allows remembering names of binder occurrences after abstraction as a forgettable property, and that's pretty neat. But when a binder does not occur in a term, abtracting over it forgets it entirely.

I have been wondering whether it would be feasible / worth it to remember this as a forgettable property stored in the Scope itself, rather than in B, so that one could re-instantiate the scoped variables with the same name.

I'm not sure whether this is clearly explained. In my use case, I have some dependent types like:

∀ (A : Type) (v : A) , Type

And, when representing them using bound, the binder v gets completely forgotten (which makes sense, since it has no occurrence). But for debugging purposes, it'd be nice to be able to have the Scope remember it.

Let me know what people think about this. Is this unwanted/unfeasible for some reason I'm not thinking about?

[Ptival]

I guess this does not make much sense when the abstraction is done via a function a -> Maybe b. Maybe I'm stuck with remembering this one the side, oh well!