Skip to content

Commit

Permalink
Remove special-casing when singling error and friends
Browse files Browse the repository at this point in the history
Previously, `singExp` had a number of _ad hoc_ special cases for handling
functions that look like exceptions (e.g., `sError` and `sUndefined`). This was
because their return types are `a` rather than, say, `Sing (Undefined @A)`,
which impaired GHC's ability to typecheck `singletons-th`–generated code. As
discussed in #588, however, there doesn't appear to be any good reason for
these functions to have return types that are so polymorphic, which called into
question why we are maintained these _ad hoc_ special cases in the first place.

This patch removes the special casing and gives `sError`,
`sErrorWithoutStackTrace`, and `sUndefined` less polymorphic return types. The
upshot is that I was able to delete a fair bit of ugly code from
`D.S.TH.Single`, which is a nice payoff.

Fixes #588.
RyanGlScott committed May 30, 2024
1 parent 7e5c92d commit 54c0fbe
Showing 11 changed files with 60 additions and 54 deletions.
23 changes: 23 additions & 0 deletions singletons-base/CHANGES.md
Original file line number Diff line number Diff line change
@@ -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.
6 changes: 3 additions & 3 deletions singletons-base/src/GHC/TypeLits/Singletons/Internal.hs
Original file line number Diff line number Diff line change
@@ -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.
Original file line number Diff line number Diff line change
@@ -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)
Original file line number Diff line number Diff line change
@@ -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
Original file line number Diff line number Diff line change
@@ -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
7 changes: 5 additions & 2 deletions singletons-base/tests/compile-and-dump/Singletons/T136.golden
Original file line number Diff line number Diff line change
@@ -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))))
Original file line number Diff line number Diff line change
@@ -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]).
Original file line number Diff line number Diff line change
@@ -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)
4 changes: 3 additions & 1 deletion singletons-base/tests/compile-and-dump/Singletons/T89.golden
Original file line number Diff line number Diff line change
@@ -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
Original file line number Diff line number Diff line change
@@ -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
41 changes: 1 addition & 40 deletions singletons-th/src/Data/Singletons/TH/Single.hs
Original file line number Diff line number Diff line change
@@ -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

0 comments on commit 54c0fbe

Please sign in to comment.