From 3903de5312cbc996d39194af41db050ef8e9a47b Mon Sep 17 00:00:00 2001
From: Ryan Scott <ryan.gl.scott@gmail.com>
Date: Mon, 3 Jun 2024 07:33:43 -0400
Subject: [PATCH] Make Sing instances more explicit on their left-hand sides

This makes it clearer what the `Sing` instances are actually matching on. Moreover,
this will be required in order to make these instances compile after
[GHC#23515](https://gitlab.haskell.org/ghc/ghc/-/issues/23515) is implemented.

This resolves the "`Sing` instances without explicit left-hand sides" section
of #601.
---
 .../src/Data/Foldable/Singletons.hs           |  2 +-
 .../src/Data/Functor/Compose/Singletons.hs    |  2 +-
 .../src/Data/Functor/Const/Singletons.hs      |  2 +-
 .../src/Data/Functor/Product/Singletons.hs    |  2 +-
 .../src/Data/Functor/Sum/Singletons.hs        |  2 +-
 singletons-base/src/Data/Proxy/Singletons.hs  |  2 +-
 .../src/Data/Singletons/Base/TypeError.hs     |  2 +-
 .../src/Data/Traversable/Singletons.hs        |  4 +-
 .../src/GHC/TypeLits/Singletons/Internal.hs   |  6 +-
 .../src/Data/Singletons/TH/CustomStar.hs      |  2 +-
 singletons/src/Data/Singletons.hs             | 21 +++++-
 singletons/src/Data/Singletons/Sigma.hs       |  7 +-
 singletons/tests/ByHand.hs                    | 66 ++++++++++++++++---
 singletons/tests/ByHand2.hs                   | 21 +++++-
 14 files changed, 111 insertions(+), 30 deletions(-)

diff --git a/singletons-base/src/Data/Foldable/Singletons.hs b/singletons-base/src/Data/Foldable/Singletons.hs
index 9b56db26..18350071 100644
--- a/singletons-base/src/Data/Foldable/Singletons.hs
+++ b/singletons-base/src/Data/Foldable/Singletons.hs
@@ -127,7 +127,7 @@ newtype Endo a = Endo (a ~> a)
 type SEndo :: Endo a -> Type
 data SEndo e where
   SEndo :: Sing x -> SEndo ('Endo x)
-type instance Sing = SEndo
+type instance Sing @(Endo a) = SEndo
 type EndoSym0 :: (a ~> a) ~> Endo a
 data EndoSym0 tf
 type instance Apply EndoSym0 x = 'Endo x
diff --git a/singletons-base/src/Data/Functor/Compose/Singletons.hs b/singletons-base/src/Data/Functor/Compose/Singletons.hs
index 056971fc..bd12764d 100644
--- a/singletons-base/src/Data/Functor/Compose/Singletons.hs
+++ b/singletons-base/src/Data/Functor/Compose/Singletons.hs
@@ -53,7 +53,7 @@ type SCompose :: Compose f g a -> Type
 data SCompose :: Compose f g a -> Type where
   SCompose :: forall f g a (x :: f (g a)).
               Sing x -> SCompose ('Compose @f @g @a x)
-type instance Sing = SCompose
+type instance Sing @(Compose f g a) = SCompose
 instance SingI x => SingI ('Compose x) where
   sing = SCompose sing
 instance SingI1 'Compose where
diff --git a/singletons-base/src/Data/Functor/Const/Singletons.hs b/singletons-base/src/Data/Functor/Const/Singletons.hs
index c0ee9d0f..58cdb5d9 100644
--- a/singletons-base/src/Data/Functor/Const/Singletons.hs
+++ b/singletons-base/src/Data/Functor/Const/Singletons.hs
@@ -75,7 +75,7 @@ type SConst :: Const a b -> Type
 data SConst :: Const a b -> Type where
   SConst :: forall {k} a (b :: k) (x :: a).
             Sing x -> SConst ('Const @a @b x)
-type instance Sing = SConst
+type instance Sing @(Const a b) = SConst
 instance SingKind a => SingKind (Const a b) where
   type Demote (Const a b) = Const (Demote a) b
   fromSing (SConst sa) = Const (fromSing sa)
diff --git a/singletons-base/src/Data/Functor/Product/Singletons.hs b/singletons-base/src/Data/Functor/Product/Singletons.hs
index b31e1125..caf33a2b 100644
--- a/singletons-base/src/Data/Functor/Product/Singletons.hs
+++ b/singletons-base/src/Data/Functor/Product/Singletons.hs
@@ -57,7 +57,7 @@ type SProduct :: Product f g a -> Type
 data SProduct :: Product f g a -> Type where
   SPair :: forall f g a (x :: f a) (y :: g a).
            Sing x -> Sing y -> SProduct ('Pair @f @g @a x y)
-type instance Sing = SProduct
+type instance Sing @(Product f g a) = SProduct
 instance (SingI x, SingI y) => SingI ('Pair x y) where
   sing = SPair sing sing
 instance SingI x => SingI1 ('Pair x) where
diff --git a/singletons-base/src/Data/Functor/Sum/Singletons.hs b/singletons-base/src/Data/Functor/Sum/Singletons.hs
index d216dd32..2056447b 100644
--- a/singletons-base/src/Data/Functor/Sum/Singletons.hs
+++ b/singletons-base/src/Data/Functor/Sum/Singletons.hs
@@ -53,7 +53,7 @@ data SSum :: Sum f g a -> Type where
           Sing x -> SSum ('InL @f @g @a x)
   SInR :: forall f g a (y :: g a).
           Sing y -> SSum ('InR @f @g @a y)
-type instance Sing = SSum
+type instance Sing @(Sum f g a) = SSum
 instance SingI x => SingI ('InL x) where
   sing = SInL sing
 instance SingI1 'InL where
diff --git a/singletons-base/src/Data/Proxy/Singletons.hs b/singletons-base/src/Data/Proxy/Singletons.hs
index 2a07ff9c..0cad9048 100644
--- a/singletons-base/src/Data/Proxy/Singletons.hs
+++ b/singletons-base/src/Data/Proxy/Singletons.hs
@@ -60,7 +60,7 @@ module for more details on this choice.)
 type SProxy :: Proxy t -> Type
 data SProxy :: Proxy t -> Type where
   SProxy :: forall t. SProxy ('Proxy @t)
-type instance Sing = SProxy
+type instance Sing @(Proxy t) = SProxy
 instance SingKind (Proxy t) where
   type Demote (Proxy t) = Proxy t
   fromSing SProxy = Proxy
diff --git a/singletons-base/src/Data/Singletons/Base/TypeError.hs b/singletons-base/src/Data/Singletons/Base/TypeError.hs
index cd9a7af1..0785ebaf 100644
--- a/singletons-base/src/Data/Singletons/Base/TypeError.hs
+++ b/singletons-base/src/Data/Singletons/Base/TypeError.hs
@@ -82,7 +82,7 @@ data SErrorMessage :: PErrorMessage -> Type where
 infixl 6 :%<>:
 infixl 5 :%$$:
 
-type instance Sing = SErrorMessage
+type instance Sing @PErrorMessage = SErrorMessage
 
 instance SingKind PErrorMessage where
   type Demote PErrorMessage = ErrorMessage
diff --git a/singletons-base/src/Data/Traversable/Singletons.hs b/singletons-base/src/Data/Traversable/Singletons.hs
index 49e829f7..6df8b8e2 100644
--- a/singletons-base/src/Data/Traversable/Singletons.hs
+++ b/singletons-base/src/Data/Traversable/Singletons.hs
@@ -64,7 +64,7 @@ newtype StateL s a = StateL (s ~> (s, a))
 type SStateL :: forall s a. StateL s a -> Type
 data SStateL state where
   SStateL :: Sing x -> SStateL ('StateL x)
-type instance Sing = SStateL
+type instance Sing @(StateL s a) = SStateL
 type StateLSym0 :: forall s a. (s ~> (s, a)) ~> StateL s a
 data StateLSym0 z
 type instance Apply StateLSym0 x = 'StateL x
@@ -74,7 +74,7 @@ newtype StateR s a = StateR (s ~> (s, a))
 type SStateR :: forall s a. StateR s a -> Type
 data SStateR state where
   SStateR :: Sing x -> SStateR ('StateR x)
-type instance Sing = SStateR
+type instance Sing @(StateR s a) = SStateR
 type StateRSym0 :: forall s a. (s ~> (s, a)) ~> StateR s a
 data StateRSym0 z
 type instance Apply StateRSym0 x = 'StateR x
diff --git a/singletons-base/src/GHC/TypeLits/Singletons/Internal.hs b/singletons-base/src/GHC/TypeLits/Singletons/Internal.hs
index d9ae4480..5dd2ae74 100644
--- a/singletons-base/src/GHC/TypeLits/Singletons/Internal.hs
+++ b/singletons-base/src/GHC/TypeLits/Singletons/Internal.hs
@@ -66,7 +66,7 @@ import Data.Text ( Text )
 ----------------------------------------------------------------------
 
 -- SNat
-type instance Sing = TN.SNat
+type instance Sing @Natural = TN.SNat
 
 instance TN.KnownNat n => SingI n where
   sing = TN.natSing
@@ -77,7 +77,7 @@ instance SingKind Natural where
   toSing n = TN.withSomeSNat n SomeSing
 
 -- STL.Symbol
-type instance Sing = TL.SSymbol
+type instance Sing @TL.Symbol = TL.SSymbol
 
 -- | An alias for the 'TL.SSymbol' pattern synonym.
 pattern SSym :: forall s. () => TL.KnownSymbol s => TL.SSymbol s
@@ -93,7 +93,7 @@ instance SingKind TL.Symbol where
   toSing s = TL.withSomeSSymbol (T.unpack s) SomeSing
 
 -- SChar
-type instance Sing = TL.SChar
+type instance Sing @Char = TL.SChar
 
 instance TL.KnownChar c => SingI c where
   sing = TL.charSing
diff --git a/singletons-th/src/Data/Singletons/TH/CustomStar.hs b/singletons-th/src/Data/Singletons/TH/CustomStar.hs
index bb653943..aa585dcb 100644
--- a/singletons-th/src/Data/Singletons/TH/CustomStar.hs
+++ b/singletons-th/src/Data/Singletons/TH/CustomStar.hs
@@ -66,7 +66,7 @@ import Language.Haskell.TH.Desugar
 -- >   SNat :: Sing Nat
 -- >   SBool :: Sing Bool
 -- >   SMaybe :: Sing a -> Sing (Maybe a)
--- > type instance Sing = SRep
+-- > type instance Sing @(*) = SRep
 --
 -- The unexpected part is that @Nat@, @Bool@, and @Maybe@ above are the real @Nat@,
 -- @Bool@, and @Maybe@, not just promoted data constructors.
diff --git a/singletons/src/Data/Singletons.hs b/singletons/src/Data/Singletons.hs
index 7107fc54..c6bf5970 100644
--- a/singletons/src/Data/Singletons.hs
+++ b/singletons/src/Data/Singletons.hs
@@ -405,7 +405,12 @@ type SWrappedSing :: forall k (a :: k). WrappedSing a -> Type
 newtype SWrappedSing :: forall k (a :: k). WrappedSing a -> Type where
   SWrapSing :: forall k (a :: k) (ws :: WrappedSing a).
                { sUnwrapSing :: Sing a } -> SWrappedSing ws
-type instance Sing = SWrappedSing
+#if __GLASGOW_HASKELL__ >= 808
+type instance Sing @(WrappedSing a) =
+#else
+type instance Sing =
+#endif
+  SWrappedSing
 
 #if __GLASGOW_HASKELL__ >= 810
 type UnwrapSing :: forall k (a :: k). WrappedSing a -> Sing a
@@ -591,7 +596,12 @@ type family ApplyTyCon :: (k1 -> k2) -> (k1 ~> unmatchable_fun) where
 --            ( 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
+#if __GLASGOW_HASKELL__ >= 808
+type instance Apply @k1 @k3 (TyCon @k1 @k2 @(k1 ~> k3) f) x =
+#else
+type instance Apply (TyCon f) x =
+#endif
+  ApplyTyCon f @@ x
 
 -- | An \"internal\" defunctionalization symbol used primarily in the
 -- definition of 'ApplyTyCon', as well as the 'SingI' instances for 'TyCon1',
@@ -730,7 +740,12 @@ type SLambda :: (k1 ~> k2) -> Type
 #endif
 newtype SLambda (f :: k1 ~> k2) =
   SLambda { applySing :: forall t. Sing t -> Sing (f @@ t) }
-type instance Sing = SLambda
+#if __GLASGOW_HASKELL__ >= 808
+type instance Sing @(k1 ~> k2) =
+#else
+type instance Sing =
+#endif
+  SLambda
 
 -- | An infix synonym for `applySing`
 (@@) :: forall k1 k2 (f :: k1 ~> k2) (t :: k1). Sing f -> Sing t -> Sing (f @@ t)
diff --git a/singletons/src/Data/Singletons/Sigma.hs b/singletons/src/Data/Singletons/Sigma.hs
index 9934dbfd..09fff6b0 100644
--- a/singletons/src/Data/Singletons/Sigma.hs
+++ b/singletons/src/Data/Singletons/Sigma.hs
@@ -99,7 +99,12 @@ data SSigma :: forall s t. Sigma s t -> Type where
   (:%&:) :: forall s t (fst :: s) (sfst :: Sing fst) (snd :: t @@ fst).
             Sing ('WrapSing sfst) -> Sing snd -> SSigma (sfst ':&: snd :: Sigma s t)
 infixr 4 :%&:
-type instance Sing = SSigma
+#if __GLASGOW_HASKELL__ >= 808
+type instance Sing @(Sigma s t) =
+#else
+type instance Sing =
+#endif
+  SSigma
 
 instance forall s t (fst :: s) (a :: Sing fst) (b :: t @@ fst).
        (SingI fst, SingI b)
diff --git a/singletons/tests/ByHand.hs b/singletons/tests/ByHand.hs
index 43489d64..995a76b3 100644
--- a/singletons/tests/ByHand.hs
+++ b/singletons/tests/ByHand.hs
@@ -98,9 +98,15 @@ type SNat :: Nat -> Type
 data SNat :: Nat -> Type where
   SZero :: SNat Zero
   SSucc :: SNat n -> SNat (Succ n)
-type instance Sing = SNat
+#if __GLASGOW_HASKELL__ >= 808
+type instance Sing @Nat =
+#else
+type instance Sing =
+#endif
+  SNat
 
-#if __GLASGOW_HASKELL__ >= 810
+#if _
+_GLASGOW_HASKELL__ >= 810
 type SuccSym0 :: Nat ~> Nat
 #endif
 data SuccSym0 :: Nat ~> Nat
@@ -152,7 +158,12 @@ type SBool :: Bool -> Type
 data SBool :: Bool -> Type where
   SFalse :: SBool False
   STrue :: SBool True
-type instance Sing = SBool
+#if __GLASGOW_HASKELL__ >= 808
+type instance Sing @Bool =
+#else
+type instance Sing =
+#endif
+  SBool
 
 {-
 (&&) :: Bool -> Bool -> Bool
@@ -192,7 +203,12 @@ type SMaybe :: forall k. Maybe k -> Type
 data SMaybe :: forall k. Maybe k -> Type where
   SNothing :: SMaybe Nothing
   SJust :: forall k (a :: k). Sing a -> SMaybe (Just a)
-type instance Sing = SMaybe
+#if __GLASGOW_HASKELL__ >= 808
+type instance Sing @(Maybe k) =
+#else
+type instance Sing =
+#endif
+  SMaybe
 
 #if __GLASGOW_HASKELL__ >= 810
 type EqualsMaybe :: Maybe k -> Maybe k -> Bool
@@ -242,7 +258,12 @@ type SList :: forall k. List k -> Type
 data SList :: forall k. List k -> Type where
   SNil :: SList Nil
   SCons :: forall k (h :: k) (t :: List k). Sing h -> SList t -> SList (Cons h t)
-type instance Sing = SList
+#if __GLASGOW_HASKELL__ >= 808
+type instance Sing @(List k) =
+#else
+type instance Sing =
+#endif
+  SList
 
 #if __GLASGOW_HASKELL__ >= 810
 type NilSym0 :: List a
@@ -315,7 +336,12 @@ type SEither :: forall k1 k2. Either k1 k2 -> Type
 data SEither :: forall k1 k2. Either k1 k2 -> Type where
   SLeft :: forall k1 (a :: k1). Sing a -> SEither (Left a)
   SRight :: forall k2 (b :: k2). Sing b -> SEither (Right b)
-type instance Sing = SEither
+#if __GLASGOW_HASKELL__ >= 808
+type instance Sing @(Either k1 k2) =
+#else
+type instance Sing =
+#endif
+  SEither
 
 instance (SingI a) => SingI (Left (a :: k)) where
   sing = SLeft sing
@@ -361,7 +387,12 @@ type SComposite :: forall k1 k2. Composite k1 k2 -> Type
 #endif
 data SComposite :: forall k1 k2. Composite k1 k2 -> Type where
   SMkComp :: forall k1 k2 (a :: Either (Maybe k1) k2). SEither a -> SComposite (MkComp a)
-type instance Sing = SComposite
+#if __GLASGOW_HASKELL__ >= 808
+type instance Sing @(Composite k1 k2) =
+#else
+type instance Sing =
+#endif
+  SComposite
 
 instance SingI a => SingI (MkComp (a :: Either (Maybe k1) k2)) where
   sing = SMkComp sing
@@ -393,7 +424,12 @@ type SEmpty :: Empty -> Type
 #endif
 data SEmpty :: Empty -> Type
 
-type instance Sing = SEmpty
+#if __GLASGOW_HASKELL__ >= 808
+type instance Sing @Empty =
+#else
+type instance Sing =
+#endif
+  SEmpty
 instance SingKind Empty where
   type Demote Empty = Empty
   fromSing = \case
@@ -420,7 +456,12 @@ data SRep :: Type -> Type where
   SNat :: SRep Nat
   SMaybe :: SRep a -> SRep (Maybe a)
   SVec :: SRep a -> SNat n -> SRep (Vec a n)
-type instance Sing = SRep
+#if __GLASGOW_HASKELL__ >= 808
+type instance Sing @Type =
+#else
+type instance Sing =
+#endif
+  SRep
 
 instance SingI Nat where
   sing = SNat
@@ -1039,4 +1080,9 @@ type SG :: forall a. G a -> Type
 #endif
 data SG :: forall a. G a -> Type where
   SMkG :: SG MkG
-type instance Sing = SG
+#if __GLASGOW_HASKELL__ >= 808
+type instance Sing @(G a) =
+#else
+type instance Sing =
+#endif
+  SG
diff --git a/singletons/tests/ByHand2.hs b/singletons/tests/ByHand2.hs
index 3ebe2033..28b6af6e 100644
--- a/singletons/tests/ByHand2.hs
+++ b/singletons/tests/ByHand2.hs
@@ -27,7 +27,12 @@ type SNat :: Nat -> Type
 data SNat :: Nat -> Type where
   SZero :: SNat 'Zero
   SSucc :: SNat n -> SNat ('Succ n)
-type instance Sing = SNat
+#if __GLASGOW_HASKELL__ >= 808
+type instance Sing @Nat =
+#else
+type instance Sing =
+#endif
+  SNat
 
 {-
 type Bool :: Type
@@ -40,7 +45,12 @@ type SBool :: Bool -> Type
 data SBool :: Bool -> Type where
   SFalse :: SBool 'False
   STrue  :: SBool 'True
-type instance Sing = SBool
+#if __GLASGOW_HASKELL__ >= 808
+type instance Sing @Bool =
+#else
+type instance Sing =
+#endif
+  SBool
 
 {-
 type Ordering :: Type
@@ -54,7 +64,12 @@ data SOrdering :: Ordering -> Type where
   SLT :: SOrdering 'LT
   SEQ :: SOrdering 'EQ
   SGT :: SOrdering 'GT
-type instance Sing = SOrdering
+#if __GLASGOW_HASKELL__ >= 808
+type instance Sing @Ordering =
+#else
+type instance Sing =
+#endif
+  SOrdering
 
 {-
 not :: Bool -> Bool