Consider removing special-casing for error during singling

[RyanGlScott]

There is a surprising amount of special-casing for the error and undefined functions during singling:

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

Lines 886 to 890 in aad81c8

	-- See Note [Why error is so special]
	singExp (ADVarE err `ADAppE` arg)
	| err == errorName = do opts <- getOptions
	DAppE (DVarE (singledValueName opts err)) <$>
	singExp arg

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

Lines 894 to 901 in aad81c8

	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'

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

Lines 795 to 807 in aad81c8

	-- 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.

I've read Note [Why error is so special], but I'm still unclear on what exactly the motivation was, since the mention of impossible case matches doesn't ring a bell. Some git blame archaeology reveals that the original motivations for this code were:

• Singletonize overlapping patterns #30, which attempted to add support for overlapping patterns. However, support for overlapping patterns was later reverted in 87aa901.

• undefined doesn't really work. #85, which is specifically about applying undefined to an argument. Interestingly, I can actually trigger the error mentioned in undefined doesn't really work. #85 (comment) after reverting the special-casing above. However, I think the reason this happens is ultimately because the return type of sUndefined (and sError) is too polymorphic. If I apply this change:

  diff --git a/singletons-base/src/GHC/TypeLits/Singletons/Internal.hs b/singletons-base/src/GHC/TypeLits/Singletons/Internal.hs
  index 2bf6efc..5096ab1 100644
  --- a/singletons-base/src/GHC/TypeLits/Singletons/Internal.hs
  +++ b/singletons-base/src/GHC/TypeLits/Singletons/Internal.hs
  @@ -217,7 +217,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'.
  @@ -228,7 +228,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'.
  @@ -237,7 +237,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.
  diff --git a/singletons-th/src/Data/Singletons/TH/Single.hs b/singletons-th/src/Data/Singletons/TH/Single.hs
  index 1e2f4a5..cdc6b64 100644
  --- a/singletons-th/src/Data/Singletons/TH/Single.hs
  +++ b/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'
  +  return $ DVarE applySingName `DAppE` e1' `DAppE` e2'
   singExp (ADLamE ty_names prom_lam names exp

  Then singletons-base continues to compile, and the test suite continues to pass (after accepting some minor differences in -ddump-splices output). I'm rather unclear why the return types of sUndefined/sError are currently so polymorphic (e89113d, which introduces sError, doesn't list a reason), but the motivation seems dubious.

In light of this, I am inclined to rip out the special-casing, as it will get rid of some hairy code. Can anyone think of a reason not to do this?