[ fix ] fix shadowing issue in record elaboration and reflection

[dunhamsteve]

Description

Fixes an issue brought up in #3501. The change in #3468 causes a regression in record elaboration where the outer name is used when shadowing. The following fails to compile:

import Data.Vect
record Foo (th : Vect n a) where
  nIsZero     : n === 0
  vectIsEmpty : (th ===)
                 $ replace {p = \ n => Vect n a} (sym nIsZero)
                 $ Nil

If the n in the lambda is replaced by z, it succeeds.

The root cause is that record elaboration is calling unelaboration with NoSugar True, which tries to make the names unique. It changes n to {n:0}, but neglects to update the instances of n under the binder. This is the same issue as #2084 filed by @buzden.

I was initially going to address this by switching to NoSugar False, but I figured I would fix #2084 instead and make unelaboration work correctly. The root issue is that the unelaborator is making a fresh variable and using it in the emitted lambda expression, but it processes the sc with the original x :: vars.

I've included the reduced test case from #3501 and verified that it fixes the reported issue in Thin/Internal.idr. (The problem with cong noted at the top of that bug report is expected behavior from an earlier breaking change.) I've also included the test case linked from #2084, swapping out the commented lines so it would verify T is the same as T''.