Define Σ as a partial application of Sigma (#373)

CHANGES.md

@@ -1,6 +1,18 @@
 Changelog for singletons project
 ================================
 
+2.6
+---
+* Redefine `Σ` such that it is now a partial application of `Sigma`, like so:
+
+  ```haskell
+  type Σ = Sigma
+  ```
+
+  One benefit of this change is that one no longer needs defunctionalization
+  symbols in order to partially apply `Σ`. As a result, `ΣSym0`, `ΣSym1`,
+  and `ΣSym2` have been removed.
+
 2.5.1
 -----
 * `ShowSing` is now a type class (with a single instance) instead of a type

src/Data/Singletons/Sigma.hs

@@ -1,12 +1,11 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE GADTs #-}
+{-# LANGUAGE ImpredicativeTypes #-} -- See Note [Impredicative Σ?]
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE TypeApplications #-}
-{-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 
 -----------------------------------------------------------------------------
@@ -26,22 +25,28 @@ module Data.Singletons.Sigma
     ( Sigma(..), Σ
     , projSigma1, projSigma2
     , mapSigma, zipSigma
-
-      -- * Defunctionalization symbols
-    , ΣSym0, ΣSym1, ΣSym2
     ) where
 
 import Data.Kind (Type)
 import Data.Singletons.Internal
-import Data.Singletons.Promote
 
 -- | A dependent pair.
 data Sigma (s :: Type) :: (s ~> Type) -> Type where
   (:&:) :: forall s t fst. Sing (fst :: s) -> t @@ fst -> Sigma s t
 infixr 4 :&:
 
 -- | Unicode shorthand for 'Sigma'.
-type Σ (s :: Type) (t :: s ~> Type) = Sigma s t
+type Σ = Sigma
+
+{-
+Note [Impredicative Σ?]
+~~~~~~~~~~~~~~~~~~~~~~~
+The definition of Σ currently will not typecheck without the use of
+ImpredicativeTypes. There isn't a fundamental reason that this should be the
+case, and the only reason that GHC currently requires this is due to Trac
+#13408. If someone ever fixes that bug, we could remove the use of
+ImpredicativeTypes.
+-}
 
 -- | Project the first element out of a dependent pair.
 projSigma1 :: forall s t. SingKind s => Sigma s t -> Demote s
@@ -71,5 +76,3 @@ zipSigma :: Sing (f :: a ~> b ~> c)
          -> Sigma a p -> Sigma b q -> Sigma c r
 zipSigma f g ((a :: Sing (fstA :: a)) :&: p) ((b :: Sing (fstB :: b)) :&: q) =
   (f @@ a @@ b) :&: (g @fstA @fstB p q)
-
-$(genDefunSymbols [''Σ])