Remove special case for [] in promoteValRhs

The comment claims that this case was needed at one point to work
around #21, but that no longer appears to be the case. Some test
cases' expected output changes due to occurrences of `'[]` changing
to `NilSym0`. To make the `Singletons.Nat` test case work in
particular, we now reexport `NilSym0` from `Data.Singletons.TH`,
just as the defunctionalization symbols for `(:)` are reexported.

Fixes #428.

src/Data/Singletons/Names.hs

@@ -190,12 +190,7 @@ promoteValNameLhsPrefix pres@(alpha, _) n
 -- used when a value name appears in an expression context
 -- works for both variables and datacons
 promoteValRhs :: Name -> DType
-promoteValRhs name
-  | name == nilName
-  = DConT nilName   -- workaround for #21
-
-  | otherwise
-  = DConT $ promoteTySym name 0
+promoteValRhs name = DConT $ promoteTySym name 0
 
 -- generates type-level symbol for a given name. Int parameter represents
 -- saturation: 0 - no parameters passed to the symbol, 1 - one parameter

src/Data/Singletons/TH.hs

@@ -105,7 +105,7 @@ module Data.Singletons.TH (
   type (<*>@#@$), type (<*>@#@$$), type (<*>@#@$$$),
   LiftA2Sym0, LiftA2Sym1, LiftA2Sym2, LiftA2Sym3,
   type (.@#@$), type (.@#@$$), type (.@#@$$$), type (.@#@$$$$),
-  (:@#@$), (:@#@$$), (:@#@$$$),
+  NilSym0, (:@#@$), (:@#@$$), (:@#@$$$),
 
   SuppressUnusedWarnings(..)
 

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

@@ -19,8 +19,8 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
     type SuccSym1 (t0123456789876543210 :: Nat) =
         Succ t0123456789876543210
     type family Compare_0123456789876543210 (a :: Nat) (a :: Nat) :: Ordering where
-      Compare_0123456789876543210 Zero Zero = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) '[]
-      Compare_0123456789876543210 (Succ a_0123456789876543210) (Succ b_0123456789876543210) = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) '[])
+      Compare_0123456789876543210 Zero Zero = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) NilSym0
+      Compare_0123456789876543210 (Succ a_0123456789876543210) (Succ b_0123456789876543210) = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) NilSym0)
       Compare_0123456789876543210 Zero (Succ _) = LTSym0
       Compare_0123456789876543210 (Succ _) Zero = GTSym0
     instance SuppressUnusedWarnings Compare_0123456789876543210Sym0 where

tests/compile-and-dump/GradingClient/Main.golden

@@ -39,19 +39,19 @@ GradingClient/Main.hs:(0,0)-(0,0): Splicing declarations
     type FirstNameSym0 = FirstName
     type LastNameSym0 = LastName
     type family Names :: Schema where
-      Names = Apply SchSym0 (Apply (Apply (:@#@$) (Apply (Apply AttrSym0 FirstNameSym0) STRINGSym0)) (Apply (Apply (:@#@$) (Apply (Apply AttrSym0 LastNameSym0) STRINGSym0)) '[]))
+      Names = Apply SchSym0 (Apply (Apply (:@#@$) (Apply (Apply AttrSym0 FirstNameSym0) STRINGSym0)) (Apply (Apply (:@#@$) (Apply (Apply AttrSym0 LastNameSym0) STRINGSym0)) NilSym0))
     type family GradingSchema :: Schema where
-      GradingSchema = Apply SchSym0 (Apply (Apply (:@#@$) (Apply (Apply AttrSym0 LastNameSym0) STRINGSym0)) (Apply (Apply (:@#@$) (Apply (Apply AttrSym0 FirstNameSym0) STRINGSym0)) (Apply (Apply (:@#@$) (Apply (Apply AttrSym0 YearNameSym0) NATSym0)) (Apply (Apply (:@#@$) (Apply (Apply AttrSym0 GradeNameSym0) NATSym0)) (Apply (Apply (:@#@$) (Apply (Apply AttrSym0 MajorNameSym0) BOOLSym0)) '[])))))
+      GradingSchema = Apply SchSym0 (Apply (Apply (:@#@$) (Apply (Apply AttrSym0 LastNameSym0) STRINGSym0)) (Apply (Apply (:@#@$) (Apply (Apply AttrSym0 FirstNameSym0) STRINGSym0)) (Apply (Apply (:@#@$) (Apply (Apply AttrSym0 YearNameSym0) NATSym0)) (Apply (Apply (:@#@$) (Apply (Apply AttrSym0 GradeNameSym0) NATSym0)) (Apply (Apply (:@#@$) (Apply (Apply AttrSym0 MajorNameSym0) BOOLSym0)) NilSym0)))))
     type family MajorName :: [AChar] where
-      MajorName = Apply (Apply (:@#@$) CMSym0) (Apply (Apply (:@#@$) CASym0) (Apply (Apply (:@#@$) CJSym0) (Apply (Apply (:@#@$) COSym0) (Apply (Apply (:@#@$) CRSym0) '[]))))
+      MajorName = Apply (Apply (:@#@$) CMSym0) (Apply (Apply (:@#@$) CASym0) (Apply (Apply (:@#@$) CJSym0) (Apply (Apply (:@#@$) COSym0) (Apply (Apply (:@#@$) CRSym0) NilSym0))))
     type family GradeName :: [AChar] where
-      GradeName = Apply (Apply (:@#@$) CGSym0) (Apply (Apply (:@#@$) CRSym0) (Apply (Apply (:@#@$) CASym0) (Apply (Apply (:@#@$) CDSym0) (Apply (Apply (:@#@$) CESym0) '[]))))
+      GradeName = Apply (Apply (:@#@$) CGSym0) (Apply (Apply (:@#@$) CRSym0) (Apply (Apply (:@#@$) CASym0) (Apply (Apply (:@#@$) CDSym0) (Apply (Apply (:@#@$) CESym0) NilSym0))))
     type family YearName :: [AChar] where
-      YearName = Apply (Apply (:@#@$) CYSym0) (Apply (Apply (:@#@$) CESym0) (Apply (Apply (:@#@$) CASym0) (Apply (Apply (:@#@$) CRSym0) '[])))
+      YearName = Apply (Apply (:@#@$) CYSym0) (Apply (Apply (:@#@$) CESym0) (Apply (Apply (:@#@$) CASym0) (Apply (Apply (:@#@$) CRSym0) NilSym0)))
     type family FirstName :: [AChar] where
-      FirstName = Apply (Apply (:@#@$) CFSym0) (Apply (Apply (:@#@$) CISym0) (Apply (Apply (:@#@$) CRSym0) (Apply (Apply (:@#@$) CSSym0) (Apply (Apply (:@#@$) CTSym0) '[]))))
+      FirstName = Apply (Apply (:@#@$) CFSym0) (Apply (Apply (:@#@$) CISym0) (Apply (Apply (:@#@$) CRSym0) (Apply (Apply (:@#@$) CSSym0) (Apply (Apply (:@#@$) CTSym0) NilSym0))))
     type family LastName :: [AChar] where
-      LastName = Apply (Apply (:@#@$) CLSym0) (Apply (Apply (:@#@$) CASym0) (Apply (Apply (:@#@$) CSSym0) (Apply (Apply (:@#@$) CTSym0) '[])))
+      LastName = Apply (Apply (:@#@$) CLSym0) (Apply (Apply (:@#@$) CASym0) (Apply (Apply (:@#@$) CSSym0) (Apply (Apply (:@#@$) CTSym0) NilSym0)))
     sNames :: Sing (NamesSym0 :: Schema)
     sGradingSchema :: Sing (GradingSchemaSym0 :: Schema)
     sMajorName :: Sing (MajorNameSym0 :: [AChar])

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

@@ -153,10 +153,10 @@ InsertionSort/InsertionSortImp.hs:(0,0)-(0,0): Splicing declarations
     type LeqSym2 (a0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) =
         Leq a0123456789876543210 a0123456789876543210
     type family InsertionSort (a :: [Nat]) :: [Nat] where
-      InsertionSort '[] = '[]
+      InsertionSort '[] = NilSym0
       InsertionSort ('(:) h t) = Apply (Apply InsertSym0 h) (Apply InsertionSortSym0 t)
     type family Insert (a :: Nat) (a :: [Nat]) :: [Nat] where
-      Insert n '[] = Apply (Apply (:@#@$) n) '[]
+      Insert n '[] = Apply (Apply (:@#@$) n) NilSym0
       Insert n ('(:) h t) = Case_0123456789876543210 n h t (Let0123456789876543210Scrutinee_0123456789876543210Sym3 n h t)
     type family Leq (a :: Nat) (a :: Nat) :: Bool where
       Leq 'Zero _ = TrueSym0

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

@@ -65,7 +65,7 @@ Singletons/AsPattern.hs:(0,0)-(0,0): Splicing declarations
         Baz t0123456789876543210 t0123456789876543210 t0123456789876543210
     type Let0123456789876543210PSym0 = Let0123456789876543210P
     type family Let0123456789876543210P where
-      Let0123456789876543210P = '[]
+      Let0123456789876543210P = NilSym0
     instance SuppressUnusedWarnings Let0123456789876543210PSym0 where
       suppressUnusedWarnings
         = snd (((,) Let0123456789876543210PSym0KindInference) ())
@@ -78,7 +78,7 @@ Singletons/AsPattern.hs:(0,0)-(0,0): Splicing declarations
     type Let0123456789876543210PSym1 wild_01234567898765432100123456789876543210 =
         Let0123456789876543210P wild_01234567898765432100123456789876543210
     type family Let0123456789876543210P wild_0123456789876543210 where
-      Let0123456789876543210P wild_0123456789876543210 = Apply (Apply (:@#@$) wild_0123456789876543210) '[]
+      Let0123456789876543210P wild_0123456789876543210 = Apply (Apply (:@#@$) wild_0123456789876543210) NilSym0
     instance SuppressUnusedWarnings Let0123456789876543210PSym0 where
       suppressUnusedWarnings
         = snd (((,) Let0123456789876543210PSym0KindInference) ())

tests/compile-and-dump/Singletons/DataValues.golden

@@ -42,13 +42,13 @@ Singletons/DataValues.hs:(0,0)-(0,0): Splicing declarations
     type ComplexSym0 = Complex
     type PrSym0 = Pr
     type family AList where
-      AList = Apply (Apply (:@#@$) ZeroSym0) (Apply (Apply (:@#@$) (Apply SuccSym0 ZeroSym0)) (Apply (Apply (:@#@$) (Apply SuccSym0 (Apply SuccSym0 ZeroSym0))) '[]))
+      AList = Apply (Apply (:@#@$) ZeroSym0) (Apply (Apply (:@#@$) (Apply SuccSym0 ZeroSym0)) (Apply (Apply (:@#@$) (Apply SuccSym0 (Apply SuccSym0 ZeroSym0))) NilSym0))
     type family Tuple where
       Tuple = Apply (Apply (Apply Tuple3Sym0 FalseSym0) (Apply JustSym0 ZeroSym0)) TrueSym0
     type family Complex where
       Complex = Apply (Apply PairSym0 (Apply (Apply PairSym0 (Apply JustSym0 ZeroSym0)) ZeroSym0)) FalseSym0
     type family Pr where
-      Pr = Apply (Apply PairSym0 (Apply SuccSym0 ZeroSym0)) (Apply (Apply (:@#@$) ZeroSym0) '[])
+      Pr = Apply (Apply PairSym0 (Apply SuccSym0 ZeroSym0)) (Apply (Apply (:@#@$) ZeroSym0) NilSym0)
     type family ShowsPrec_0123456789876543210 (a :: GHC.Types.Nat) (a :: Pair a b) (a :: Symbol) :: Symbol where
       ShowsPrec_0123456789876543210 p_0123456789876543210 (Pair arg_0123456789876543210 arg_0123456789876543210) a_0123456789876543210 = Apply (Apply (Apply ShowParenSym0 (Apply (Apply (>@#@$) p_0123456789876543210) (FromInteger 10))) (Apply (Apply (.@#@$) (Apply ShowStringSym0 "Pair ")) (Apply (Apply (.@#@$) (Apply (Apply ShowsPrecSym0 (FromInteger 11)) arg_0123456789876543210)) (Apply (Apply (.@#@$) ShowSpaceSym0) (Apply (Apply ShowsPrecSym0 (FromInteger 11)) arg_0123456789876543210))))) a_0123456789876543210
     instance SuppressUnusedWarnings ShowsPrec_0123456789876543210Sym0 where

tests/compile-and-dump/Singletons/HigherOrder.golden

@@ -309,14 +309,14 @@ Singletons/HigherOrder.hs:(0,0)-(0,0): Splicing declarations
       Foo f g a = Apply (Apply f g) a
     type family ZipWith (a :: (~>) a ((~>) b c)) (a :: [a]) (a :: [b]) :: [c] where
       ZipWith f ('(:) x xs) ('(:) y ys) = Apply (Apply (:@#@$) (Apply (Apply f x) y)) (Apply (Apply (Apply ZipWithSym0 f) xs) ys)
-      ZipWith _ '[] '[] = '[]
-      ZipWith _ ('(:) _ _) '[] = '[]
-      ZipWith _ '[] ('(:) _ _) = '[]
+      ZipWith _ '[] '[] = NilSym0
+      ZipWith _ ('(:) _ _) '[] = NilSym0
+      ZipWith _ '[] ('(:) _ _) = NilSym0
     type family LiftMaybe (a :: (~>) a b) (a :: Maybe a) :: Maybe b where
       LiftMaybe f ('Just x) = Apply JustSym0 (Apply f x)
       LiftMaybe _ 'Nothing = NothingSym0
     type family Map (a :: (~>) a b) (a :: [a]) :: [b] where
-      Map _ '[] = '[]
+      Map _ '[] = NilSym0
       Map f ('(:) h t) = Apply (Apply (:@#@$) (Apply f h)) (Apply (Apply MapSym0 f) t)
     sEtad ::
       forall (t :: [Nat]) (t :: [Bool]).

tests/compile-and-dump/Singletons/LambdasComprehensive.golden

@@ -28,9 +28,9 @@ Singletons/LambdasComprehensive.hs:(0,0)-(0,0): Splicing declarations
     type BarSym0 = Bar
     type FooSym0 = Foo
     type family Bar :: [Nat] where
-      Bar = Apply (Apply MapSym0 (Apply (Apply Either_Sym0 PredSym0) SuccSym0)) (Apply (Apply (:@#@$) (Apply LeftSym0 ZeroSym0)) (Apply (Apply (:@#@$) (Apply RightSym0 (Apply SuccSym0 ZeroSym0))) '[]))
+      Bar = Apply (Apply MapSym0 (Apply (Apply Either_Sym0 PredSym0) SuccSym0)) (Apply (Apply (:@#@$) (Apply LeftSym0 ZeroSym0)) (Apply (Apply (:@#@$) (Apply RightSym0 (Apply SuccSym0 ZeroSym0))) NilSym0))
     type family Foo :: [Nat] where
-      Foo = Apply (Apply MapSym0 Lambda_0123456789876543210Sym0) (Apply (Apply (:@#@$) (Apply LeftSym0 ZeroSym0)) (Apply (Apply (:@#@$) (Apply RightSym0 (Apply SuccSym0 ZeroSym0))) '[]))
+      Foo = Apply (Apply MapSym0 Lambda_0123456789876543210Sym0) (Apply (Apply (:@#@$) (Apply LeftSym0 ZeroSym0)) (Apply (Apply (:@#@$) (Apply RightSym0 (Apply SuccSym0 ZeroSym0))) NilSym0))
     sBar :: Sing (BarSym0 :: [Nat])
     sFoo :: Sing (FooSym0 :: [Nat])
     sBar

tests/compile-and-dump/Singletons/Nat.golden

@@ -108,8 +108,8 @@ Singletons/Nat.hs:(0,0)-(0,0): Splicing declarations
     instance PShow Nat where
       type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a
     type family Compare_0123456789876543210 (a :: Nat) (a :: Nat) :: Ordering where
-      Compare_0123456789876543210 Zero Zero = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) '[]
-      Compare_0123456789876543210 (Succ a_0123456789876543210) (Succ b_0123456789876543210) = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) '[])
+      Compare_0123456789876543210 Zero Zero = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) NilSym0
+      Compare_0123456789876543210 (Succ a_0123456789876543210) (Succ b_0123456789876543210) = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) NilSym0)
       Compare_0123456789876543210 Zero (Succ _) = LTSym0
       Compare_0123456789876543210 (Succ _) Zero = GTSym0
     instance SuppressUnusedWarnings Compare_0123456789876543210Sym0 where