Use noExactTyVars when promoting functions with local variables

Whenever we promote a function that closes over one or more local variables, we
now use `noExactTyVars` to ensure that none of the local variables reuse unique
`Name`s.  This isn't strictly necessary right now, but this will be required in
a future patch that will panic (triggering
https://gitlab.haskell.org/ghc/ghc/-/issues/11812) unless `noExactTyVars` is
used.

While I was in the neighborhood, I took the opportunity to write `Note
[Pitfalls of NameU/NameL]` with more context about why `noExactTyVars` is
necessary in the first place, and I added references to the Note in all the
places where we use it.

singletons-base/tests/compile-and-dump/GradingClient/Database.golden

@@ -449,9 +449,9 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
                ())
     type family Let0123456789876543210Scrutinee_0123456789876543210Sym4 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210 where
       Let0123456789876543210Scrutinee_0123456789876543210Sym4 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210
-    type family Let0123456789876543210Scrutinee_0123456789876543210 name name' u attrs where
+    type family Let0123456789876543210Scrutinee_0123456789876543210 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210 where
       Let0123456789876543210Scrutinee_0123456789876543210 name name' u attrs = Apply (Apply (==@#@$) name) name'
-    type family Case_0123456789876543210 name name' u attrs t where
+    type family Case_0123456789876543210 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210 t where
       Case_0123456789876543210 name name' u attrs 'True = u
       Case_0123456789876543210 name name' u attrs 'False = Apply (Apply LookupSym0 name) (Apply SchSym0 attrs)
     type LookupSym0 :: (~>) [AChar] ((~>) Schema U)

singletons-base/tests/compile-and-dump/InsertionSort/InsertionSortImp.golden

@@ -96,9 +96,9 @@ InsertionSort/InsertionSortImp.hs:(0,0)-(0,0): Splicing declarations
                ())
     type family Let0123456789876543210Scrutinee_0123456789876543210Sym3 n0123456789876543210 h0123456789876543210 t0123456789876543210 where
       Let0123456789876543210Scrutinee_0123456789876543210Sym3 n0123456789876543210 h0123456789876543210 t0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210 n0123456789876543210 h0123456789876543210 t0123456789876543210
-    type family Let0123456789876543210Scrutinee_0123456789876543210 n h t where
+    type family Let0123456789876543210Scrutinee_0123456789876543210 n0123456789876543210 h0123456789876543210 t0123456789876543210 where
       Let0123456789876543210Scrutinee_0123456789876543210 n h t = Apply (Apply LeqSym0 n) h
-    type family Case_0123456789876543210 n h t t where
+    type family Case_0123456789876543210 n0123456789876543210 h0123456789876543210 t0123456789876543210 t where
       Case_0123456789876543210 n h t 'True = Apply (Apply (:@#@$) n) (Apply (Apply (:@#@$) h) t)
       Case_0123456789876543210 n h t 'False = Apply (Apply (:@#@$) h) (Apply (Apply InsertSym0 n) t)
     type InsertionSortSym0 :: (~>) [Nat] [Nat]

singletons-base/tests/compile-and-dump/Singletons/AsPattern.golden

@@ -75,7 +75,7 @@ Singletons/AsPattern.hs:(0,0)-(0,0): Splicing declarations
         = snd ((,) Let0123456789876543210PSym0KindInference ())
     type family Let0123456789876543210PSym1 wild_01234567898765432100123456789876543210 where
       Let0123456789876543210PSym1 wild_01234567898765432100123456789876543210 = Let0123456789876543210P wild_01234567898765432100123456789876543210
-    type family Let0123456789876543210P wild_0123456789876543210 where
+    type family Let0123456789876543210P wild_01234567898765432100123456789876543210 where
       Let0123456789876543210P wild_0123456789876543210 = Apply (Apply (:@#@$) wild_0123456789876543210) NilSym0
     data Let0123456789876543210PSym0 wild_01234567898765432100123456789876543210
       where
@@ -103,7 +103,7 @@ Singletons/AsPattern.hs:(0,0)-(0,0): Splicing declarations
         = snd ((,) Let0123456789876543210PSym2KindInference ())
     type family Let0123456789876543210PSym3 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 where
       Let0123456789876543210PSym3 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 = Let0123456789876543210P wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210
-    type family Let0123456789876543210P wild_0123456789876543210 wild_0123456789876543210 wild_0123456789876543210 where
+    type family Let0123456789876543210P wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 where
       Let0123456789876543210P wild_0123456789876543210 wild_0123456789876543210 wild_0123456789876543210 = Apply (Apply (:@#@$) wild_0123456789876543210) (Apply (Apply (:@#@$) wild_0123456789876543210) wild_0123456789876543210)
     data Let0123456789876543210PSym0 wild_01234567898765432100123456789876543210
       where
@@ -123,7 +123,7 @@ Singletons/AsPattern.hs:(0,0)-(0,0): Splicing declarations
         = snd ((,) Let0123456789876543210PSym1KindInference ())
     type family Let0123456789876543210PSym2 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 where
       Let0123456789876543210PSym2 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 = Let0123456789876543210P wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210
-    type family Let0123456789876543210P wild_0123456789876543210 wild_0123456789876543210 where
+    type family Let0123456789876543210P wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 where
       Let0123456789876543210P wild_0123456789876543210 wild_0123456789876543210 = Apply (Apply Tuple2Sym0 wild_0123456789876543210) wild_0123456789876543210
     type family Let0123456789876543210PSym0 where
       Let0123456789876543210PSym0 = Let0123456789876543210P
@@ -155,7 +155,7 @@ Singletons/AsPattern.hs:(0,0)-(0,0): Splicing declarations
         = snd ((,) Let0123456789876543210PSym2KindInference ())
     type family Let0123456789876543210PSym3 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 where
       Let0123456789876543210PSym3 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 = Let0123456789876543210P wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210
-    type family Let0123456789876543210P wild_0123456789876543210 wild_0123456789876543210 wild_0123456789876543210 where
+    type family Let0123456789876543210P wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 where
       Let0123456789876543210P wild_0123456789876543210 wild_0123456789876543210 wild_0123456789876543210 = Apply JustSym0 (Apply (Apply (Apply BazSym0 wild_0123456789876543210) wild_0123456789876543210) wild_0123456789876543210)
     data Let0123456789876543210XSym0 wild_01234567898765432100123456789876543210
       where
@@ -167,7 +167,7 @@ Singletons/AsPattern.hs:(0,0)-(0,0): Splicing declarations
         = snd ((,) Let0123456789876543210XSym0KindInference ())
     type family Let0123456789876543210XSym1 wild_01234567898765432100123456789876543210 where
       Let0123456789876543210XSym1 wild_01234567898765432100123456789876543210 = Let0123456789876543210X wild_01234567898765432100123456789876543210
-    type family Let0123456789876543210X wild_0123456789876543210 where
+    type family Let0123456789876543210X wild_01234567898765432100123456789876543210 where
       Let0123456789876543210X wild_0123456789876543210 = Apply JustSym0 wild_0123456789876543210
     type family Let0123456789876543210PSym0 where
       Let0123456789876543210PSym0 = Let0123456789876543210P

singletons-base/tests/compile-and-dump/Singletons/CaseExpressions.golden

@@ -37,9 +37,9 @@ Singletons/CaseExpressions.hs:(0,0)-(0,0): Splicing declarations
                in z
     foo5 :: a -> a
     foo5 x = case x of y -> (\ _ -> x) y
-    type family Case_0123456789876543210 arg_0123456789876543210 y x t where
+    type family Case_0123456789876543210 arg_01234567898765432100123456789876543210 y0123456789876543210 x0123456789876543210 t where
       Case_0123456789876543210 arg_0123456789876543210 y x _ = x
-    type family Lambda_0123456789876543210 y x arg_0123456789876543210 where
+    type family Lambda_0123456789876543210 y0123456789876543210 x0123456789876543210 arg_0123456789876543210 where
       Lambda_0123456789876543210 y x arg_0123456789876543210 = Case_0123456789876543210 arg_0123456789876543210 y x arg_0123456789876543210
     data Lambda_0123456789876543210Sym0 y0123456789876543210
       where
@@ -67,7 +67,7 @@ Singletons/CaseExpressions.hs:(0,0)-(0,0): Splicing declarations
         = snd ((,) Lambda_0123456789876543210Sym2KindInference ())
     type family Lambda_0123456789876543210Sym3 y0123456789876543210 x0123456789876543210 arg_01234567898765432100123456789876543210 where
       Lambda_0123456789876543210Sym3 y0123456789876543210 x0123456789876543210 arg_01234567898765432100123456789876543210 = Lambda_0123456789876543210 y0123456789876543210 x0123456789876543210 arg_01234567898765432100123456789876543210
-    type family Case_0123456789876543210 x t where
+    type family Case_0123456789876543210 x0123456789876543210 t where
       Case_0123456789876543210 x y = Apply (Apply (Apply Lambda_0123456789876543210Sym0 y) x) y
     data Let0123456789876543210ZSym0 y0123456789876543210
       where
@@ -87,9 +87,9 @@ Singletons/CaseExpressions.hs:(0,0)-(0,0): Splicing declarations
         = snd ((,) Let0123456789876543210ZSym1KindInference ())
     type family Let0123456789876543210ZSym2 y0123456789876543210 x0123456789876543210 :: a0123456789876543210 where
       Let0123456789876543210ZSym2 y0123456789876543210 x0123456789876543210 = Let0123456789876543210Z y0123456789876543210 x0123456789876543210
-    type family Let0123456789876543210Z y x :: a where
+    type family Let0123456789876543210Z y0123456789876543210 x0123456789876543210 :: a where
       Let0123456789876543210Z y x = y
-    type family Case_0123456789876543210 x t where
+    type family Case_0123456789876543210 x0123456789876543210 t where
       Case_0123456789876543210 x y = Let0123456789876543210ZSym2 y x
     data Let0123456789876543210Scrutinee_0123456789876543210Sym0 a0123456789876543210
       where
@@ -115,9 +115,9 @@ Singletons/CaseExpressions.hs:(0,0)-(0,0): Splicing declarations
                ())
     type family Let0123456789876543210Scrutinee_0123456789876543210Sym2 a0123456789876543210 b0123456789876543210 where
       Let0123456789876543210Scrutinee_0123456789876543210Sym2 a0123456789876543210 b0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210 a0123456789876543210 b0123456789876543210
-    type family Let0123456789876543210Scrutinee_0123456789876543210 a b where
+    type family Let0123456789876543210Scrutinee_0123456789876543210 a0123456789876543210 b0123456789876543210 where
       Let0123456789876543210Scrutinee_0123456789876543210 a b = Apply (Apply Tuple2Sym0 a) b
-    type family Case_0123456789876543210 a b t where
+    type family Case_0123456789876543210 a0123456789876543210 b0123456789876543210 t where
       Case_0123456789876543210 a b '(p, _) = p
     data Let0123456789876543210Scrutinee_0123456789876543210Sym0 d0123456789876543210
       where
@@ -132,11 +132,11 @@ Singletons/CaseExpressions.hs:(0,0)-(0,0): Splicing declarations
                ())
     type family Let0123456789876543210Scrutinee_0123456789876543210Sym1 d0123456789876543210 where
       Let0123456789876543210Scrutinee_0123456789876543210Sym1 d0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210 d0123456789876543210
-    type family Let0123456789876543210Scrutinee_0123456789876543210 d where
+    type family Let0123456789876543210Scrutinee_0123456789876543210 d0123456789876543210 where
       Let0123456789876543210Scrutinee_0123456789876543210 d = Apply JustSym0 d
-    type family Case_0123456789876543210 d t where
+    type family Case_0123456789876543210 d0123456789876543210 t where
       Case_0123456789876543210 d ('Just y) = y
-    type family Case_0123456789876543210 d x t where
+    type family Case_0123456789876543210 d0123456789876543210 x0123456789876543210 t where
       Case_0123456789876543210 d x ('Just y) = y
       Case_0123456789876543210 d x 'Nothing = d
     type Foo5Sym0 :: (~>) a a

singletons-base/tests/compile-and-dump/Singletons/EmptyShowDeriving.golden

@@ -6,7 +6,7 @@ Singletons/EmptyShowDeriving.hs:(0,0)-(0,0): Splicing declarations
   ======>
     data Foo
     deriving instance Show Foo
-    type family Case_0123456789876543210 v_0123456789876543210 a_0123456789876543210 t where
+    type family Case_0123456789876543210 v_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 t where
     type ShowsPrec_0123456789876543210 :: GHC.Num.Natural.Natural
                                           -> Foo -> GHC.Types.Symbol -> GHC.Types.Symbol
     type family ShowsPrec_0123456789876543210 (a :: GHC.Num.Natural.Natural) (a :: Foo) (a :: GHC.Types.Symbol) :: GHC.Types.Symbol where

singletons-base/tests/compile-and-dump/Singletons/EnumDeriving.golden

@@ -24,13 +24,13 @@ Singletons/EnumDeriving.hs:(0,0)-(0,0): Splicing declarations
     type Q2Sym0 :: Quux
     type family Q2Sym0 :: Quux where
       Q2Sym0 = Q2
-    type family Case_0123456789876543210 n t where
+    type family Case_0123456789876543210 n0123456789876543210 t where
       Case_0123456789876543210 n 'True = BumSym0
       Case_0123456789876543210 n 'False = Apply ErrorSym0 "toEnum: bad argument"
-    type family Case_0123456789876543210 n t where
+    type family Case_0123456789876543210 n0123456789876543210 t where
       Case_0123456789876543210 n 'True = BazSym0
       Case_0123456789876543210 n 'False = Case_0123456789876543210 n (Apply (Apply (==@#@$) n) (FromInteger 2))
-    type family Case_0123456789876543210 n t where
+    type family Case_0123456789876543210 n0123456789876543210 t where
       Case_0123456789876543210 n 'True = BarSym0
       Case_0123456789876543210 n 'False = Case_0123456789876543210 n (Apply (Apply (==@#@$) n) (FromInteger 1))
     type ToEnum_0123456789876543210 :: GHC.Num.Natural.Natural -> Foo
@@ -148,10 +148,10 @@ Singletons/EnumDeriving.hs:(0,0)-(0,0): Splicing declarations
 Singletons/EnumDeriving.hs:0:0:: Splicing declarations
     singEnumInstance ''Quux
   ======>
-    type family Case_0123456789876543210 n t where
+    type family Case_0123456789876543210 n0123456789876543210 t where
       Case_0123456789876543210 n 'True = Q2Sym0
       Case_0123456789876543210 n 'False = Apply ErrorSym0 "toEnum: bad argument"
-    type family Case_0123456789876543210 n t where
+    type family Case_0123456789876543210 n0123456789876543210 t where
       Case_0123456789876543210 n 'True = Q1Sym0
       Case_0123456789876543210 n 'False = Case_0123456789876543210 n (Apply (Apply (==@#@$) n) (FromInteger 1))
     type ToEnum_0123456789876543210 :: GHC.Num.Natural.Natural -> Quux