Define SingI instances for TyCon{N} once-and-for-all (#382)

* Define SingI instances for TyCon{N} once-and-for-all

Fixes #381.

* Delete overlapping SingI instances for TyCon{N}s

CHANGES.md

@@ -57,6 +57,18 @@ Changelog for singletons project
   `TypeApplications` extension. (The generated code was always using
   `TypeApplications` under the hood, but it's only now that GHC is detecting
   it.)
+* `Data.Singletons` now defines a family of `SingI` instances for `TyCon1`
+  through `TyCon8`:
+
+  ```haskell
+  instance (forall a.    SingI a           => SingI (f a),   ...) => SingI (TyCon1 f)
+  instance (forall a b. (SingI a, SingI b) => SingI (f a b), ...) => SingI (TyCon2 f)
+  ...
+  ```
+
+  As a result, `singletons` no longer generates instances for `SingI` instances
+  for applications of `TyCon{N}` to particular type constructors, as they have
+  been superseded by the instances above.
 * Redefine `Σ` such that it is now a partial application of `Sigma`, like so:
 
   ```haskell

src/Data/Singletons.hs

@@ -1,12 +1,15 @@
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE MagicHash #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
@@ -92,9 +95,23 @@ import Data.Singletons.Prelude.Ord
 import Data.Singletons.Prelude.Semigroup
 import Data.Singletons.Promote
 import Data.Singletons.ShowSing
+import Data.Singletons.Single (singITyConInstances)
 import Data.String
 import qualified Data.Text as T (pack)
 
+----------------------------------------------------------------------
+---- SingI TyCon{N} instances ----------------------------------------
+----------------------------------------------------------------------
+
+{-
+Generates SingI instances for TyCon1 through TyCon8:
+
+  instance (forall a.    SingI a           => SingI (f a),   ...) => SingI (TyCon1 f)
+  instance (forall a b. (SingI a, SingI b) => SingI (f a b), ...) => SingI (TyCon2 f)
+  ...
+-}
+$(singITyConInstances [1..8])
+
 ----------------------------------------------------------------------
 ---- SomeSing instances ----------------------------------------------
 ----------------------------------------------------------------------

src/Data/Singletons/Internal.hs

@@ -201,11 +201,39 @@ data family TyCon :: (k1 -> k2) -> unmatchable_fun
 -- here because dealing with inequality like this is hard, and
 -- I (Richard) wasn't sure what concrete value the ticket would
 -- have, given that we don't know how to begin fixing it.
-type family ApplyTyCon (f :: k1 -> k2) (x :: k1) :: k3 where
-  ApplyTyCon (f :: k1 -> k2 -> k3) x = TyCon (f x)
-  ApplyTyCon f x                     = f x
-
-type instance Apply (TyCon f) x = ApplyTyCon f x
+type family ApplyTyCon :: (k1 -> k2) -> (k1 ~> unmatchable_fun) where
+  ApplyTyCon = (ApplyTyConAux2 :: (k1 -> k2 -> k3) -> (k1 ~> unmatchable_fun))
+  ApplyTyCon = (ApplyTyConAux1 :: (k1 -> k2)       -> (k1 ~> k2))
+-- Upon first glance, the definition of ApplyTyCon (as well as the
+-- corresponding Apply instance for TyCon) seems a little indirect. One might
+-- wonder why these aren't defined like so:
+--
+--   type family ApplyTyCon (f :: k1 -> k2) (x :: k1) :: k3 where
+--     ApplyTyCon (f :: k1 -> k2 -> k3) x = TyCon (f x)
+--     ApplyTyCon f x                     = f x
+--
+--   type instance Apply (TyCon f) x = ApplyTyCon f x
+--
+-- This also works, but it requires that ApplyTyCon always be applied to a
+-- minimum of two arguments. In particular, this rules out a trick that we use
+-- elsewhere in the library to write SingI instances for different TyCons,
+-- which relies on partial applications of ApplyTyCon:
+--
+--   instance forall k1 k2 (f :: k1 -> k2).
+--            ( forall a. SingI a => SingI (f a)
+--            , (ApplyTyCon :: (k1 -> k2) -> (k1 ~> k2)) ~ ApplyTyConAux1
+--            ) => SingI (TyCon1 f) where
+type instance Apply (TyCon f) x = ApplyTyCon f @@ x
+
+-- | An \"internal\" defunctionalization symbol used primarily in the
+-- definition of 'ApplyTyCon', as well as the 'SingI' instances for 'TyCon1',
+-- 'TyCon2', etc.
+data ApplyTyConAux1 :: (k1 -> k2) -> (k1 ~> k2)
+-- | An \"internal\" defunctionalization symbol used primarily in the
+-- definition of 'ApplyTyCon'.
+data ApplyTyConAux2 :: (k1 -> k2) -> (k1 ~> unmatchable_fun)
+type instance Apply (ApplyTyConAux1 f) x = f x
+type instance Apply (ApplyTyConAux2 f) x = TyCon (f x)
 
 -- | Wrapper for converting the normal type-level arrow into a '~>'.
 -- For example, given:

src/Data/Singletons/Names.hs

@@ -26,9 +26,10 @@ import Control.Monad
 boolName, andName, tyEqName, compareName, minBoundName,
   maxBoundName, repName,
   nilName, consName, listName, tyFunArrowName,
-  applyName, natName, symbolName, typeRepName, stringName,
+  applyName, applyTyConName, applyTyConAux1Name,
+  natName, symbolName, typeRepName, stringName,
   eqName, ordName, boundedName, orderingName,
-  singFamilyName, singIName, singMethName, demoteName,
+  singFamilyName, singIName, singMethName, demoteName, withSingIName,
   singKindClassName, sEqClassName, sEqMethName, sconsName, snilName, strueName,
   sIfName,
   someSingTypeName, someSingDataName,
@@ -58,6 +59,8 @@ consName = '(:)
 listName = ''[]
 tyFunArrowName = ''(~>)
 applyName = ''Apply
+applyTyConName = ''ApplyTyCon
+applyTyConAux1Name = ''ApplyTyConAux1
 symbolName = ''Symbol
 natName = ''Nat
 typeRepName = ''TypeRep
@@ -72,6 +75,7 @@ singMethName = 'sing
 toSingName = 'toSing
 fromSingName = 'fromSing
 demoteName = ''Demote
+withSingIName = 'withSingI
 singKindClassName = ''SingKind
 sEqClassName = mk_name_tc "Data.Singletons.Prelude.Eq" "SEq"
 sEqMethName = mk_name_v "Data.Singletons.Prelude.Eq" "%=="

src/Data/Singletons/Prelude/Const.hs

@@ -1,5 +1,4 @@
 {-# LANGUAGE DataKinds #-}
-{-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE InstanceSigs #-}
 {-# LANGUAGE PolyKinds #-}
@@ -85,8 +84,6 @@ instance SingI a => SingI ('Const a) where
 $(genDefunSymbols [''Const])
 instance SingI ConstSym0 where
   sing = singFun1 SConst
-instance SingI (TyCon1 'Const) where
-  sing = singFun1 SConst
 
 $(singletons [d|
   type family GetConst (x :: Const a b) :: a where

src/Data/Singletons/Single.hs

@@ -210,6 +210,55 @@ showSingInstance name = do
 showSingInstances :: DsMonad q => [Name] -> q [Dec]
 showSingInstances = concatMapM showSingInstance
 
+-- | Create an instance for @'SingI' TyCon{N}@, where @N@ is the positive
+-- number provided as an argument.
+--
+-- Note that the generated code requires the use of the @QuantifiedConstraints@
+-- language extension.
+singITyConInstances :: DsMonad q => [Int] -> q [Dec]
+singITyConInstances = concatMapM singITyConInstance
+
+-- | Create an instance for @'SingI' TyCon{N}@, where @N@ is the positive
+-- number provided as an argument.
+--
+-- Note that the generated code requires the use of the @QuantifiedConstraints@
+-- language extension.
+singITyConInstance :: DsMonad q => Int -> q [Dec]
+singITyConInstance n
+  | n <= 0
+  = fail $ "Argument must be a positive number (given " ++ show n ++ ")"
+  | otherwise
+  = do as <- replicateM n (qNewName "a")
+       ks <- replicateM n (qNewName "k")
+       k_last <- qNewName "k_last"
+       f      <- qNewName "f"
+       x      <- qNewName "x"
+       let k_penult = last ks
+           k_fun = ravel (map DVarT ks) (DVarT k_last)
+           f_ty  = DVarT f
+           a_tys = map DVarT as
+           mk_fun arrow t1 t2 = arrow `DAppT` t1 `DAppT` t2
+           matchable_apply_fun   = mk_fun DArrowT                (DVarT k_penult) (DVarT k_last)
+           unmatchable_apply_fun = mk_fun (DConT tyFunArrowName) (DVarT k_penult) (DVarT k_last)
+           ctxt = [ DForallT (map DPlainTV as)
+                             (map (DAppT (DConT singIName)) a_tys)
+                             (DConT singIName `DAppT` foldType f_ty a_tys)
+                  , DConT equalityName
+                      `DAppT` (DConT applyTyConName `DSigT`
+                                mk_fun DArrowT matchable_apply_fun unmatchable_apply_fun)
+                      `DAppT` DConT applyTyConAux1Name
+                  ]
+       pure $ decToTH
+            $ DInstanceD
+                Nothing ctxt
+                (DConT singIName `DAppT` (DConT (mkTyConName n) `DAppT` (f_ty `DSigT` k_fun)))
+                [DLetDec $ DFunD singMethName
+                           [DClause [] $
+                            wrapSingFun 1 DWildCardT $
+                            DLamE [x] $
+                            DVarE withSingIName `DAppE` DVarE x
+                                                `DAppE` DVarE singMethName]]
+
 singInstance :: DsMonad q => DerivDesc q -> String -> Name -> q [Dec]
 singInstance mk_inst inst_name name = do
   (tvbs, cons) <- getDataD ("I cannot make an instance of " ++ inst_name

src/Data/Singletons/Single/Defun.hs

@@ -45,15 +45,9 @@ import Language.Haskell.TH.Syntax
 -- Note that singDefuns takes Maybe DKinds for the promoted argument and result
 -- types, in case we have an entity whose type needs to be inferred.
 -- See Note [singDefuns and type inference].
---
--- Note that in the particular case of a data constructor, we actually generate
--- /two/ SingI instances partial application—one for the defunctionalization
--- symbol, and one for the data constructor placed inside TyCon{N}.
--- See Note [SingI instances for partially applied constructors].
 singDefuns :: Name      -- The Name of the thing to promote.
            -> NameSpace -- Whether the above Name is a value, data constructor,
                         -- or a type constructor.
-                        -- See Note [SingI instances for partially applied constructors]
            -> DCxt      -- The type's context.
            -> [Maybe DKind] -- The promoted argument types (if known).
            -> Maybe DKind   -- The promoted result type (if known).
@@ -119,28 +113,20 @@ singDefuns n ns ty_ctxt mb_ty_args mb_ty_res =
         mb_inst_kind = foldr buildTyFunArrow_maybe mb_ty_res mb_tyss
 
         new_insts :: [DDec]
-        new_insts
-          | DataName <- ns
-          = -- See Note [SingI instances for partially applied constructors]
-            let s_data_con = DConE $ singDataConName n in
-            [ mk_inst defun_inst_ty s_data_con
-            , mk_inst tycon_inst_ty s_data_con ]
-          | otherwise
-          = [mk_inst defun_inst_ty $ DVarE $ singValName n]
+        new_insts = [DInstanceD Nothing
+                                (sty_ctxt ++ singI_ctxt)
+                                (DConT singIName `DAppT` mk_inst_ty defun_inst_ty)
+                                [DLetDec $ DValD (DVarP singMethName)
+                                         $ wrapSingFun sing_fun_num defun_inst_ty
+                                         $ mk_sing_fun_expr sing_exp ]]
           where
-            mk_inst :: DType -> DExp -> DDec
-            mk_inst inst_head sing_exp
-              = DInstanceD Nothing
-                           (sty_ctxt ++ singI_ctxt)
-                           (DConT singIName `DAppT` mk_inst_ty inst_head)
-                           [DLetDec $ DValD (DVarP singMethName)
-                                    $ wrapSingFun sing_fun_num inst_head
-                                    $ mk_sing_fun_expr sing_exp ]
-
-            defun_inst_ty, tycon_inst_ty :: DType
+            defun_inst_ty :: DType
             defun_inst_ty = foldType (DConT (promoteTySym n sym_num)) tvb_tys
-            tycon_inst_ty = DConT (mkTyConName sing_fun_num) `DAppT`
-                            foldType (DConT n) tvb_tys
+
+            sing_exp :: DExp
+            sing_exp = case ns of
+                         DataName -> DConE $ singDataConName n
+                         _        -> DVarE $ singValName n
 
 {-
 Note [singDefuns and type inference]
@@ -176,38 +162,4 @@ This is true, but also not unprecedented, as the singled version of bar, sBar,
 will /also/ fail to typecheck due to a missing SEq constraint. Therefore, this
 design choice fits within the existing tradition of type inference in
 singletons.
-
-Note [SingI instances for partially applied constructors]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Unlike normal functions, where we generate one SingI instance for each of its
-partial applications (one per defunctionalization symbol), we generate *two*
-SingI instances for each partial application of a data constructor. That is,
-if we have:
-
-  data D a where
-    K :: a -> D a
-
-K has an partial application, so we will generate the following two SingI
-instances:
-
-  instance SingI KSym0          where sing = singFun1 SK
-  instance SingI (TyCon1 KSym0) where sing = singFun1 SK
-
-The first instance is exactly the same as what we'd generate for a normal,
-partially applied function's defun symbol. The second one, while functionally
-equivalent, is a bit dissatisfying: in general, adopting this approach means
-that we end up generating many instances of the form:
-
-  instance SingI (TyCon1 S1)
-  instance SingI (TyCon1 S2)
-  ...
-
-Ideally, we'd have a single instance SingI (TyCon1 s) to rule them all. But
-doing so would require writing something akin to:
-
-  instance (forall a. SingI a => SingI (f a)) => SingI (TyCon1 f) where
-    sing = SLambda $ \(x :: Sing a) -> withSingI x $ sing @_ @(f a)
-
-But this would require quantified constraints. Until GHC gains these, we
-compensate by generating out several SingI (TyCon1 s) instances.
 -}

src/Data/Singletons/TH.hs

@@ -44,6 +44,7 @@ module Data.Singletons.TH (
   singShowInstances, singShowInstance,
 
   -- ** Utility functions
+  singITyConInstances, singITyConInstance,
   cases, sCases,
 
   -- * Basic singleton definitions

src/Data/Singletons/TypeError.hs

@@ -158,31 +158,19 @@ $(genDefunSymbols [''ErrorMessage', ''TypeError])
 
 instance SingI (TextSym0 :: Symbol ~> PErrorMessage) where
   sing = singFun1 SText
-instance SingI (TyCon1 'Text :: Symbol ~> PErrorMessage) where
-  sing = singFun1 SText
 
 instance SingI (ShowTypeSym0 :: t ~> PErrorMessage) where
   sing = singFun1 SShowType
-instance SingI (TyCon1 'ShowType :: t ~> PErrorMessage) where
-  sing = singFun1 SShowType
 
 instance SingI ((:<>:@#@$) :: PErrorMessage ~> PErrorMessage ~> PErrorMessage) where
   sing = singFun2 (:%<>:)
-instance SingI (TyCon2 '(:<>:) :: PErrorMessage ~> PErrorMessage ~> PErrorMessage) where
-  sing = singFun2 (:%<>:)
 instance SingI x => SingI ((:<>:@#@$$) x :: PErrorMessage ~> PErrorMessage) where
   sing = singFun1 (sing @x :%<>:)
-instance SingI x => SingI (TyCon1 ('(:<>:) x) :: PErrorMessage ~> PErrorMessage) where
-  sing = singFun1 (sing @x :%<>:)
 
 instance SingI ((:$$:@#@$) :: PErrorMessage ~> PErrorMessage ~> PErrorMessage) where
   sing = singFun2 (:%$$:)
-instance SingI (TyCon2 '(:$$:) :: PErrorMessage ~> PErrorMessage ~> PErrorMessage) where
-  sing = singFun2 (:%$$:)
 instance SingI x => SingI ((:$$:@#@$$) x :: PErrorMessage ~> PErrorMessage) where
   sing = singFun1 (sing @x :%$$:)
-instance SingI x => SingI (TyCon1 ('(:$$:) x) :: PErrorMessage ~> PErrorMessage) where
-  sing = singFun1 (sing @x :%$$:)
 
 instance SingI TypeErrorSym0 where
   sing = singFun1 sTypeError

tests/compile-and-dump/GradingClient/Database.ghc86.template

@@ -116,8 +116,6 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
       sing = SSucc sing
     instance SingI (SuccSym0 :: (~>) Nat Nat) where
       sing = (singFun1 @SuccSym0) SSucc
-    instance SingI (TyCon1 Succ :: (~>) Nat Nat) where
-      sing = (singFun1 @(TyCon1 Succ)) SSucc
 GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
     singletons
       [d| append :: Schema -> Schema -> Schema
@@ -2524,13 +2522,8 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
       sing = (SVEC sing) sing
     instance SingI (VECSym0 :: (~>) U ((~>) Nat U)) where
       sing = (singFun2 @VECSym0) SVEC
-    instance SingI (TyCon2 VEC :: (~>) U ((~>) Nat U)) where
-      sing = (singFun2 @(TyCon2 VEC)) SVEC
     instance SingI d => SingI (VECSym1 (d :: U) :: (~>) Nat U) where
       sing = (singFun1 @(VECSym1 (d :: U))) (SVEC (sing @d))
-    instance SingI d =>
-             SingI (TyCon1 (VEC (d :: U)) :: (~>) Nat U) where
-      sing = (singFun1 @(TyCon1 (VEC (d :: U)))) (SVEC (sing @d))
     instance SingI CA where
       sing = SCA
     instance SingI CB where
@@ -2588,20 +2581,13 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
       sing = (SAttr sing) sing
     instance SingI (AttrSym0 :: (~>) [AChar] ((~>) U Attribute)) where
       sing = (singFun2 @AttrSym0) SAttr
-    instance SingI (TyCon2 Attr :: (~>) [AChar] ((~>) U Attribute)) where
-      sing = (singFun2 @(TyCon2 Attr)) SAttr
     instance SingI d =>
              SingI (AttrSym1 (d :: [AChar]) :: (~>) U Attribute) where
       sing = (singFun1 @(AttrSym1 (d :: [AChar]))) (SAttr (sing @d))
-    instance SingI d =>
-             SingI (TyCon1 (Attr (d :: [AChar])) :: (~>) U Attribute) where
-      sing = (singFun1 @(TyCon1 (Attr (d :: [AChar])))) (SAttr (sing @d))
     instance SingI n => SingI (Sch (n :: [Attribute])) where
       sing = SSch sing
     instance SingI (SchSym0 :: (~>) [Attribute] Schema) where
       sing = (singFun1 @SchSym0) SSch
-    instance SingI (TyCon1 Sch :: (~>) [Attribute] Schema) where
-      sing = (singFun1 @(TyCon1 Sch)) SSch
 GradingClient/Database.hs:0:0:: Splicing declarations
     return [] ======>
 GradingClient/Database.hs:(0,0)-(0,0): Splicing expression

tests/compile-and-dump/InsertionSort/InsertionSortImp.ghc86.template

@@ -32,8 +32,6 @@ InsertionSort/InsertionSortImp.hs:(0,0)-(0,0): Splicing declarations
       sing = SSucc sing
     instance SingI (SuccSym0 :: (~>) Nat Nat) where
       sing = (singFun1 @SuccSym0) SSucc
-    instance SingI (TyCon1 Succ :: (~>) Nat Nat) where
-      sing = (singFun1 @(TyCon1 Succ)) SSucc
 InsertionSort/InsertionSortImp.hs:(0,0)-(0,0): Splicing declarations
     singletons
       [d| leq :: Nat -> Nat -> Bool