Skip to content

Commit

Permalink
Adapt to DLamCasesE in th-desugar-1.18
Browse files Browse the repository at this point in the history
This patch bumps the pinned `th-desugar` commit to bring in the changes from
goldfirere/th-desugar#218, which replaces `DLamE` and
`DCaseE` in favor of `DLamCasesE`. Quite happily, this actually _simplifies_
how singling works in `singletons-th`. Previously, we went through great
efforts to annotate promoted `case` expressions with their overall return type,
as described in `Note [Annotate case return type]` and `Note [The id hack; or,
how singletons-th learned to stop worrying and avoid kind generalization]` in
`D.S.TH.Single`. After this patch, however, all `case` expressions are
desugared to `\cases` expressions, and because we already annotate singled
`\cases` expressions (by generating code like `singFun1 @LamCasesSym0 (\cases
...)`), we no longer need to use the tricks describes in those two Notes.
Hooray!

One interesting knock-on effect of these simplifications is that given code
like this:

```hs
map (\x -> ()) xs -- Note that `x` is unused
```

`singletons-th` would previously generate code that looked like this:

```hs
sMap (singFun1 @LamdaSym0 (\sX -> case sX of (_ :: Sing x) -> STuple0)) sXs
```

Unlike the original code, this singled code would compile without warnings.
This is because `sX` is "used" in the sense that it is passed to a `case`
expression. It's a very silly `case` expression, as it doesn't do anything
meaningful with `sX`, but it still technically counts as a use.

Now that `singletons-th` uses a `\cases`-based approach to singling, however,
the singled code will instead look like this:

```hs
sMap (singFun1 @LamCasesSym0 (\cases (sX :: Sing x) -> STuple0)) sXs
```

This time, GHC _does_ recognize that `sX` is unused and emits a warning. This
actually affects the way that `singletons-th` generates code for derived
`Functor` and `Foldable` instances, so I needed to generate wildcard patterns
instead of variable patterns in certain parts of
`D.S.TH.Promote.Deriving.{Functor,Foldable}`. I have also mentioned the
possibility of `singletons-th` generating more warnings in the `CHANGELOG`.
  • Loading branch information
RyanGlScott committed Jun 25, 2024
1 parent a351105 commit 2107048
Show file tree
Hide file tree
Showing 79 changed files with 3,145 additions and 2,928 deletions.
2 changes: 1 addition & 1 deletion .github/workflows/haskell-ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -215,7 +215,7 @@ jobs:
source-repository-package
type: git
location: https://github.com/goldfirere/th-desugar
tag: ae6c075edb50175a99b35f0bdcf475b695a5ee78
tag: 1d17abf8add216424790f10bbb3e4c33d2d736f5
EOF
$HCPKG list --simple-output --names-only | perl -ne 'for (split /\s+/) { print "constraints: any.$_ installed\n" unless /^(Cabal|Cabal-syntax|singletons|singletons-base|singletons-th)$/; }' >> cabal.project.local
cat cabal.project
Expand Down
2 changes: 1 addition & 1 deletion cabal.project
Original file line number Diff line number Diff line change
Expand Up @@ -5,4 +5,4 @@ packages: ./singletons
source-repository-package
type: git
location: https://github.com/goldfirere/th-desugar
tag: ae6c075edb50175a99b35f0bdcf475b695a5ee78
tag: 1d17abf8add216424790f10bbb3e4c33d2d736f5
2 changes: 1 addition & 1 deletion singletons-base/singletons-base.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -78,7 +78,7 @@ library
singletons-th >= 3.4 && < 3.5,
template-haskell >= 2.22 && < 2.23,
text >= 1.2,
th-desugar >= 1.17 && < 1.18
th-desugar >= 1.18 && < 1.19
default-language: GHC2021
other-extensions: TemplateHaskell
exposed-modules: Data.Singletons.Base.CustomStar
Expand Down
1,417 changes: 709 additions & 708 deletions singletons-base/tests/compile-and-dump/GradingClient/Database.golden

Large diffs are not rendered by default.

Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,8 @@ InsertionSort/InsertionSortImp.hs:(0,0)-(0,0): Splicing declarations
fromSing (SSucc b) = Succ (fromSing b)
toSing Zero = SomeSing SZero
toSing (Succ (b :: Demote Nat))
= case toSing b :: SomeSing Nat of SomeSing c -> SomeSing (SSucc c)
= (\cases (SomeSing c) -> SomeSing (SSucc c))
(toSing b :: SomeSing Nat)
instance SingI Zero where
sing = SZero
instance SingI n => SingI (Succ (n :: Nat)) where
Expand Down Expand Up @@ -61,13 +62,19 @@ InsertionSort/InsertionSortImp.hs:(0,0)-(0,0): Splicing declarations
insertionSort :: [Nat] -> [Nat]
insertionSort [] = []
insertionSort (h : t) = insert h (insertionSort t)
type family Let0123456789876543210Scrutinee_0123456789876543210Sym0 n0123456789876543210 h0123456789876543210 t0123456789876543210 where
Let0123456789876543210Scrutinee_0123456789876543210Sym0 n0123456789876543210 h0123456789876543210 t0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210 n0123456789876543210 h0123456789876543210 t0123456789876543210
type family Let0123456789876543210Scrutinee_0123456789876543210 n0123456789876543210 h0123456789876543210 t0123456789876543210 where
Let0123456789876543210Scrutinee_0123456789876543210 n h t = Apply (Apply LeqSym0 n) h
type family Case_0123456789876543210 n0123456789876543210 h0123456789876543210 t0123456789876543210 t where
Case_0123456789876543210 n h t 'True = Apply (Apply (:@#@$) n) (Apply (Apply (:@#@$) h) t)
Case_0123456789876543210 n h t 'False = Apply (Apply (:@#@$) h) (Apply (Apply InsertSym0 n) t)
type family LamCases_0123456789876543210 n0123456789876543210 h0123456789876543210 t0123456789876543210 a_0123456789876543210 where
LamCases_0123456789876543210 n h t 'True = Apply (Apply (:@#@$) n) (Apply (Apply (:@#@$) h) t)
LamCases_0123456789876543210 n h t 'False = Apply (Apply (:@#@$) h) (Apply (Apply InsertSym0 n) t)
data LamCases_0123456789876543210Sym0 n0123456789876543210 h0123456789876543210 t0123456789876543210 a_01234567898765432100123456789876543210
where
LamCases_0123456789876543210Sym0KindInference :: SameKind (Apply (LamCases_0123456789876543210Sym0 n0123456789876543210 h0123456789876543210 t0123456789876543210) arg) (LamCases_0123456789876543210Sym1 n0123456789876543210 h0123456789876543210 t0123456789876543210 arg) =>
LamCases_0123456789876543210Sym0 n0123456789876543210 h0123456789876543210 t0123456789876543210 a_01234567898765432100123456789876543210
type instance Apply @_ @_ (LamCases_0123456789876543210Sym0 n0123456789876543210 h0123456789876543210 t0123456789876543210) a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 n0123456789876543210 h0123456789876543210 t0123456789876543210 a_01234567898765432100123456789876543210
instance SuppressUnusedWarnings (LamCases_0123456789876543210Sym0 n0123456789876543210 h0123456789876543210 t0123456789876543210) where
suppressUnusedWarnings
= snd ((,) LamCases_0123456789876543210Sym0KindInference ())
type family LamCases_0123456789876543210Sym1 n0123456789876543210 h0123456789876543210 t0123456789876543210 a_01234567898765432100123456789876543210 where
LamCases_0123456789876543210Sym1 n0123456789876543210 h0123456789876543210 t0123456789876543210 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 n0123456789876543210 h0123456789876543210 t0123456789876543210 a_01234567898765432100123456789876543210
type InsertionSortSym0 :: (~>) [Nat] [Nat]
data InsertionSortSym0 :: (~>) [Nat] [Nat]
where
Expand Down Expand Up @@ -125,7 +132,7 @@ InsertionSort/InsertionSortImp.hs:(0,0)-(0,0): Splicing declarations
type Insert :: Nat -> [Nat] -> [Nat]
type family Insert (a :: Nat) (a :: [Nat]) :: [Nat] where
Insert n '[] = Apply (Apply (:@#@$) n) NilSym0
Insert n ('(:) h t) = Case_0123456789876543210 n h t (Let0123456789876543210Scrutinee_0123456789876543210Sym0 n h t)
Insert n ('(:) h t) = Apply (LamCases_0123456789876543210Sym0 n h t) (Apply (Apply LeqSym0 n) h)
type Leq :: Nat -> Nat -> Bool
type family Leq (a :: Nat) (a :: Nat) :: Bool where
Leq 'Zero _ = TrueSym0
Expand All @@ -148,23 +155,19 @@ InsertionSort/InsertionSortImp.hs:(0,0)-(0,0): Splicing declarations
sInsert (sN :: Sing n) SNil
= applySing (applySing (singFun2 @(:@#@$) SCons) sN) SNil
sInsert (sN :: Sing n) (SCons (sH :: Sing h) (sT :: Sing t))
= let
sScrutinee_0123456789876543210 ::
Sing @_ (Let0123456789876543210Scrutinee_0123456789876543210 n h t)
sScrutinee_0123456789876543210
= applySing (applySing (singFun2 @LeqSym0 sLeq) sN) sH
in
id
@(Sing (Case_0123456789876543210 n h t (Let0123456789876543210Scrutinee_0123456789876543210Sym0 n h t)))
(case sScrutinee_0123456789876543210 of
STrue
-> applySing
(applySing (singFun2 @(:@#@$) SCons) sN)
(applySing (applySing (singFun2 @(:@#@$) SCons) sH) sT)
SFalse
-> applySing
(applySing (singFun2 @(:@#@$) SCons) sH)
(applySing (applySing (singFun2 @InsertSym0 sInsert) sN) sT))
= applySing
(singFun1
@(LamCases_0123456789876543210Sym0 n h t)
(\cases
STrue
-> applySing
(applySing (singFun2 @(:@#@$) SCons) sN)
(applySing (applySing (singFun2 @(:@#@$) SCons) sH) sT)
SFalse
-> applySing
(applySing (singFun2 @(:@#@$) SCons) sH)
(applySing (applySing (singFun2 @InsertSym0 sInsert) sN) sT)))
(applySing (applySing (singFun2 @LeqSym0 sLeq) sN) sH)
sLeq SZero _ = STrue
sLeq (SSucc _) SZero = SFalse
sLeq (SSucc (sA :: Sing a)) (SSucc (sB :: Sing b))
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -286,13 +286,10 @@ Singletons/AsPattern.hs:(0,0)-(0,0): Splicing declarations
type Demote Baz = Baz
fromSing (SBaz b b b) = Baz (fromSing b) (fromSing b) (fromSing b)
toSing (Baz (b :: Demote Nat) (b :: Demote Nat) (b :: Demote Nat))
= case
(,,)
(toSing b :: SomeSing Nat) (toSing b :: SomeSing Nat)
(toSing b :: SomeSing Nat)
of
(,,) (SomeSing c) (SomeSing c) (SomeSing c)
-> SomeSing (SBaz c c c)
= (\cases
(SomeSing c) (SomeSing c) (SomeSing c) -> SomeSing (SBaz c c c))
(toSing b :: SomeSing Nat) (toSing b :: SomeSing Nat)
(toSing b :: SomeSing Nat)
instance (SingI n, SingI n, SingI n) =>
SingI (Baz (n :: Nat) (n :: Nat) (n :: Nat)) where
sing = SBaz sing sing sing
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -164,7 +164,8 @@ Singletons/BoundedDeriving.hs:(0,0)-(0,0): Splicing declarations
type Demote (Foo3 a) = Foo3 (Demote a)
fromSing (SFoo3 b) = Foo3 (fromSing b)
toSing (Foo3 (b :: Demote a))
= case toSing b :: SomeSing a of SomeSing c -> SomeSing (SFoo3 c)
= (\cases (SomeSing c) -> SomeSing (SFoo3 c))
(toSing b :: SomeSing a)
data SFoo4 :: forall (a :: Type) (b :: Type). Foo4 a b -> Type
where
SFoo41 :: forall (a :: Type) (b :: Type). SFoo4 (Foo41 :: Foo4 a b)
Expand All @@ -185,10 +186,8 @@ Singletons/BoundedDeriving.hs:(0,0)-(0,0): Splicing declarations
type Demote Pair = Pair
fromSing (SPair b b) = Pair (fromSing b) (fromSing b)
toSing (Pair (b :: Demote Bool) (b :: Demote Bool))
= case
(,) (toSing b :: SomeSing Bool) (toSing b :: SomeSing Bool)
of
(,) (SomeSing c) (SomeSing c) -> SomeSing (SPair c c)
= (\cases (SomeSing c) (SomeSing c) -> SomeSing (SPair c c))
(toSing b :: SomeSing Bool) (toSing b :: SomeSing Bool)
instance SBounded Foo1 where
sMinBound = SFoo1
sMaxBound = SFoo1
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -46,7 +46,8 @@ Singletons/BoxUnBox.hs:(0,0)-(0,0): Splicing declarations
type Demote (Box a) = Box (Demote a)
fromSing (SFBox b) = FBox (fromSing b)
toSing (FBox (b :: Demote a))
= case toSing b :: SomeSing a of SomeSing c -> SomeSing (SFBox c)
= (\cases (SomeSing c) -> SomeSing (SFBox c))
(toSing b :: SomeSing a)
instance SingI n => SingI (FBox (n :: a)) where
sing = SFBox sing
instance SingI1 FBox where
Expand Down
Loading

0 comments on commit 2107048

Please sign in to comment.