Pretty printer should avoid accidental capturing

[favonia]

The variables could be accidentally captured (to the user's eyes) when being printed.

[jonsterling]

Can you give an example please?

[favonia]

You can change some c2 or c1 in semi-simplicial.prl to c and we will see...

...
    c : ($ Pick n m)
    f : ($ folder' (! proj1 (tuple [proj1 x] [proj2 y])) n)
    g : (->
         [c : ($ Pick n p')]
         ($
          (! proj2 (tuple [proj1 x] [proj2 y]))
          ($ proj' (! proj1 (tuple [proj1 x] [proj2 y])) n p' c f)))
    ----------------------------------------------------------------
    (->
     [c : ($ Pick m p')]
     ($
      (! proj2 (tuple [proj1 x] [proj2 y]))
      ($
       proj'
       (! proj1 (tuple [proj1 x] [proj2 y]))
       m
       p'
       c
       ($ proj' x n m c f))))

The c in the conclusion are not the same.

[jonsterling]

I think I may see what you mean generally. If we shadow a name in a binder, we keep printing the outer variable with the same name. I think what it means is that the printer for binders should not be allowed to choose names that induce shadowing. Does that make sense?

[favonia]

Yes. I have not put any thought into how we should solve this yet.