Remove special-casing when singling error and friends

singletons-base/CHANGES.md

@@ -1,6 +1,29 @@
 Changelog for the `singletons-base` project
 ===========================================
 
+next [????.??.??]
+-----------------
+* The types of `sError`, `sErrorWithoutStackTrace`, and `sUndefined` are now
+  less polymorphic than they were before:
+
+  ```diff
+  -sError :: forall a (str :: Symbol). HasCallStack => Sing str -> a
+  +sError :: forall a (str :: Symbol). HasCallStack => Sing str -> Sing (Error @a str)
+
+  -sErrorWithoutStackTrace :: forall a (str :: Symbol). Sing str -> a
+  +sErrorWithoutStackTrace :: forall a (str :: Symbol). Sing str -> Sing (ErrorWithoutStackTrace @a str)
+
+  -sUndefined :: forall a. HasCallStack => a
+  +sUndefined :: forall a. HasCallStack => Sing (Undefined @a)
+  ```
+
+  This is because the old type signatures were _too_ polymorphic, and they
+  required _ad hoc_ special casing in `singletons-th` in order to make them
+  work in generated code. The more specific type signatures that these functions
+  now have improve type inference and avoid the need for special casing. If you
+  truly need the full polymorphism of the old type signatures, use `error`,
+  `errorWithoutStackTrace`, or `undefined` instead.
+
 3.4 [2024.05.12]
 ----------------
 * Require building with GHC 9.10.

singletons-base/src/GHC/TypeLits/Singletons/Internal.hs

@@ -218,7 +218,7 @@ instance SingI (ErrorSym0 :: TL.Symbol ~> a) where
   sing = singFun1 sError
 
 -- | The singleton for 'error'.
-sError :: HasCallStack => Sing (str :: TL.Symbol) -> a
+sError :: forall a (str :: TL.Symbol). HasCallStack => Sing str -> Sing (Error @a str)
 sError sstr = error (T.unpack (fromSing sstr))
 
 -- | The promotion of 'errorWithoutStackTrace'.
@@ -229,7 +229,7 @@ instance SingI (ErrorWithoutStackTraceSym0 :: TL.Symbol ~> a) where
   sing = singFun1 sErrorWithoutStackTrace
 
 -- | The singleton for 'errorWithoutStackTrace'.
-sErrorWithoutStackTrace :: Sing (str :: TL.Symbol) -> a
+sErrorWithoutStackTrace :: forall a (str :: TL.Symbol). Sing str -> Sing (ErrorWithoutStackTrace @a str)
 sErrorWithoutStackTrace sstr = errorWithoutStackTrace (T.unpack (fromSing sstr))
 
 -- | The promotion of 'undefined'.
@@ -238,7 +238,7 @@ type family Undefined :: a where {}
 $(genDefunSymbols [''Undefined])
 
 -- | The singleton for 'undefined'.
-sUndefined :: HasCallStack => a
+sUndefined :: forall a. HasCallStack => Sing (Undefined @a)
 sUndefined = undefined
 
 -- | The singleton analogue of '(TN.^)' for 'Natural's.

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

@@ -131,7 +131,10 @@ Singletons/EnumDeriving.hs:(0,0)-(0,0): Splicing declarations
                                        (sFromInteger (sing :: Sing 2))
                                  of
                                    STrue -> SBum
-                                   SFalse -> sError (sing :: Sing "toEnum: bad argument"))))
+                                   SFalse
+                                     -> applySing
+                                          (singFun1 @ErrorSym0 sError)
+                                          (sing :: Sing "toEnum: bad argument"))))
       sFromEnum SBar = sFromInteger (sing :: Sing 0)
       sFromEnum SBaz = sFromInteger (sing :: Sing 1)
       sFromEnum SBum = sFromInteger (sing :: Sing 2)
@@ -218,6 +221,9 @@ Singletons/EnumDeriving.hs:0:0:: Splicing declarations
                              (sFromInteger (sing :: Sing 1))
                        of
                          STrue -> SQ2
-                         SFalse -> sError (sing :: Sing "toEnum: bad argument")))
+                         SFalse
+                           -> applySing
+                                (singFun1 @ErrorSym0 sError)
+                                (sing :: Sing "toEnum: bad argument")))
       sFromEnum SQ1 = sFromInteger (sing :: Sing 0)
       sFromEnum SQ2 = sFromInteger (sing :: Sing 1)

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

@@ -25,6 +25,8 @@ Singletons/Error.hs:(0,0)-(0,0): Splicing declarations
     sHead ::
       (forall (t :: [a]). Sing t -> Sing (Apply HeadSym0 t :: a) :: Type)
     sHead (SCons (sA :: Sing a) _) = sA
-    sHead SNil = sError (sing :: Sing "head: empty list")
+    sHead SNil
+      = applySing
+          (singFun1 @ErrorSym0 sError) (sing :: Sing "head: empty list")
     instance SingI (HeadSym0 :: (~>) [a] a) where
       sing = singFun1 @HeadSym0 sHead

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

@@ -499,7 +499,10 @@ Singletons/StandaloneDeriving.hs:(0,0)-(0,0): Splicing declarations
                              (sFromInteger (sing :: Sing 1))
                        of
                          STrue -> SS2
-                         SFalse -> sError (sing :: Sing "toEnum: bad argument")))
+                         SFalse
+                           -> applySing
+                                (singFun1 @ErrorSym0 sError)
+                                (sing :: Sing "toEnum: bad argument")))
       sFromEnum SS1 = sFromInteger (sing :: Sing 0)
       sFromEnum SS2 = sFromInteger (sing :: Sing 1)
     instance SDecide a => SDecide (T a ()) where

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

@@ -135,7 +135,8 @@ Singletons/T136.hs:(0,0)-(0,0): Splicing declarations
         = applySing
             (applySing (singFun2 @(:@#@$) SCons) SFalse)
             (applySing (singFun1 @SuccSym0 sSucc) sAs)
-      sPred SNil = sError (sing :: Sing "pred 0")
+      sPred SNil
+        = applySing (singFun1 @ErrorSym0 sError) (sing :: Sing "pred 0")
       sPred (SCons SFalse (sAs :: Sing as))
         = applySing
             (applySing (singFun2 @(:@#@$) SCons) STrue)
@@ -154,7 +155,9 @@ Singletons/T136.hs:(0,0)-(0,0): Splicing declarations
                              (applySing (singFun2 @(<@#@$) (%<)) sI)
                              (sFromInteger (sing :: Sing 0))
                        of
-                         STrue -> sError (sing :: Sing "negative toEnum")
+                         STrue
+                           -> applySing
+                                (singFun1 @ErrorSym0 sError) (sing :: Sing "negative toEnum")
                          SFalse
                            -> id
                                 @(Sing (Case_0123456789876543210 i arg_0123456789876543210 (Apply (Apply (==@#@$) i) (FromInteger 0))))

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

@@ -144,7 +144,9 @@ Singletons/T167.hs:(0,0)-(0,0): Splicing declarations
       sFooList
         (sA_0123456789876543210 :: Sing a_0123456789876543210)
         (sA_0123456789876543210 :: Sing a_0123456789876543210)
-        = sUndefined sA_0123456789876543210 sA_0123456789876543210
+        = applySing
+            (applySing sUndefined sA_0123456789876543210)
+            sA_0123456789876543210
     instance SFoo a => SFoo [a] where
       sFoosPrec ::
         (forall (t :: Natural) (t :: [a]) (t :: [Bool]).

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

@@ -196,7 +196,9 @@ Singletons/T190.hs:0:0:: Splicing declarations
                    (sFromInteger (sing :: Sing 0))
              of
                STrue -> ST
-               SFalse -> sError (sing :: Sing "toEnum: bad argument"))
+               SFalse
+                 -> applySing
+                      (singFun1 @ErrorSym0 sError) (sing :: Sing "toEnum: bad argument"))
       sFromEnum ST = sFromInteger (sing :: Sing 0)
     instance SBounded T where
       sMinBound :: Sing (MinBoundSym0 :: T)

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

@@ -73,7 +73,9 @@ Singletons/T89.hs:0:0:: Splicing declarations
              of
                STrue -> SFoo
                SFalse
-                 -> sError (sFromString (sing :: Sing "toEnum: bad argument")))
+                 -> applySing
+                      (singFun1 @ErrorSym0 sError)
+                      (sFromString (sing :: Sing "toEnum: bad argument")))
       sFromEnum SFoo = sFromInteger (sing :: Sing 0)
     instance SingI Foo where
       sing = SFoo

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

@@ -44,9 +44,11 @@ Singletons/Undef.hs:(0,0)-(0,0): Splicing declarations
       (forall (t :: Bool).
        Sing t -> Sing (Apply FooSym0 t :: Bool) :: Type)
     sBar (sA_0123456789876543210 :: Sing a_0123456789876543210)
-      = sError (sing :: Sing "urk") sA_0123456789876543210
+      = applySing
+          (applySing (singFun1 @ErrorSym0 sError) (sing :: Sing "urk"))
+          sA_0123456789876543210
     sFoo (sA_0123456789876543210 :: Sing a_0123456789876543210)
-      = sUndefined sA_0123456789876543210
+      = applySing sUndefined sA_0123456789876543210
     instance SingI (BarSym0 :: (~>) Bool Bool) where
       sing = singFun1 @BarSym0 sBar
     instance SingI (FooSym0 :: (~>) Bool Bool) where

singletons-th/src/Data/Singletons/TH/Single.hs

@@ -792,20 +792,6 @@ mkSigPaCaseE exps_with_sigs exp
 -- Note [The id hack; or, how singletons-th learned to stop worrying and avoid
 -- kind generalization] for an explanation of why we do this.
 
--- Note [Why error is so special]
--- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
--- Some of the transformations that happen before this point produce impossible
--- case matches. We must be careful when processing these so as not to make
--- an error GHC will complain about. When binding the case-match variables, we
--- normally include an equality constraint saying that the scrutinee is equal
--- to the matched pattern. But, we can't do this in inaccessible matches, because
--- equality is bogus, and GHC (rightly) complains. However, we then have another
--- problem, because GHC doesn't have enough information when type-checking the
--- RHS of the inaccessible match to deem it type-safe. The solution: treat error
--- as super-special, so that GHC doesn't look too hard at singletonized error
--- calls. Specifically, DON'T do the applySing stuff. Just use sError, which
--- has a custom type (Sing x -> a) anyway.
-
 -- Note [Singling pattern signatures]
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 -- We want to single a pattern signature, like so:
@@ -883,22 +869,13 @@ mkSigPaCaseE exps_with_sigs exp
 --    And now everything is hunky-dory.
 
 singExp :: ADExp -> SgM DExp
-  -- See Note [Why error is so special]
-singExp (ADVarE err `ADAppE` arg)
-  | err == errorName = do opts <- getOptions
-                          DAppE (DVarE (singledValueName opts err)) <$>
-                            singExp arg
 singExp (ADVarE name) = lookupVarE name
 singExp (ADConE name) = lookupConE name
 singExp (ADLitE lit)  = singLit lit
 singExp (ADAppE e1 e2) = do
   e1' <- singExp e1
   e2' <- singExp e2
-  -- `applySing undefined x` kills type inference, because GHC can't figure
-  -- out the type of `undefined`. So we don't emit `applySing` there.
-  if isException e1'
-  then return $ e1' `DAppE` e2'
-  else return $ (DVarE applySingName) `DAppE` e1' `DAppE` e2'
+  pure $ DVarE applySingName `DAppE` e1' `DAppE` e2'
 singExp (ADLamE ty_names prom_lam names exp) = do
   opts <- getOptions
   let sNames = map (singledValueName opts) names
@@ -989,22 +966,6 @@ singDerivedShowDecs (DerivedDecl { ded_mb_cxt     = mb_cxt
                       (DConT showName `DAppT` (DConT sty_tycon `DAppT` DSigT (DVarT z) ki))
     pure [show_inst]
 
-isException :: DExp -> Bool
-isException (DVarE n)             = nameBase n == "sUndefined"
-isException (DConE {})            = False
-isException (DLitE {})            = False
-isException (DAppE (DVarE fun) _) | nameBase fun == "sError" = True
-isException (DAppE fun _)         = isException fun
-isException (DAppTypeE e _)       = isException e
-isException (DLamE _ _)           = False
-isException (DCaseE e _)          = isException e
-isException (DLetE _ e)           = isException e
-isException (DSigE e _)           = isException e
-isException (DStaticE e)          = isException e
-isException (DTypedBracketE e)    = isException e
-isException (DTypedSpliceE e)     = isException e
-isException (DTypeE _)            = False
-
 singMatch :: ADMatch -> SgM DMatch
 singMatch (ADMatch var_proms pat exp) = do
   opts <- getOptions