Skip to content

Commit

Permalink
Simplify singling of instance method types
Browse files Browse the repository at this point in the history 
Previously, `singletons-th` would always attempt to generate instance
signatures for singled instance methods, even if the original instance code
lacks instance signatures. To do so, `singletons-th` will infer an instance
signature by reifying the type of the method (or, if that cannot be found, the
singled version of the method) and manually applying a substitution from class
variables to instance types. This process is quite involved, and what's more,
it doesn't work in all cases:

* As noted in #358, inferred instance signatures can sometimes be ill-kinded.
* In order to support singling examples like the ones from #581, we need type
  variables from class method defaults and instance methods to scope over their
  bodies. However, the approach that `singletons-th` used to reify the method
  type for the singled code will sometimes reify _different_ type variables
  than the ones used in the promoted code, leading to disaster.

This convention of inferring the instance signature dates all the way back to
commit
c9beec5,
and it's unclear why this choice was made. At the time of writing #358, I was
convinced that inferred instance signatures were necessary to support examples
like the one in
#358 (comment).
However, this example is only problematic due to the use of an explicit kind
annotation on a promoted `case` expression, and these explicit kind annotations
were removed in the fix for #547. As such, this convention no longer serves a
useful purpose.

This patch removes the instance signature inference code, greatly simplifying
the overall process of singling instance declarations.

Fixes #590.
  • Loading branch information
@RyanGlScott
RyanGlScott committed May 19, 2024
1 parent 33f2992 commit b9b357b
Show file tree
Hide file tree
Showing 31 changed files with 10 additions and 527 deletions.
1 change: 0 additions & 1 deletion README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -634,7 +634,6 @@ instance POrd Bool where
type Compare 'True 'True = 'EQ

instance SOrd Bool where
sCompare :: forall (x :: a) (y :: a). Sing x -> Sing y -> Sing (Compare x y)
sCompare SFalse SFalse = SEQ
sCompare SFalse STrue = SLT
sCompare STrue SFalse = SGT
Expand Down
36 changes: 0 additions & 36 deletions singletons-base/tests/compile-and-dump/GradingClient/Database.golden
View file
Original file line number Diff line number Diff line change
Expand Up @@ -92,11 +92,6 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
toSing (Succ (b :: Demote Nat))
= case toSing b :: SomeSing Nat of SomeSing c -> SomeSing (SSucc c)
instance SEq Nat => SEq Nat where
(%==) ::
forall (t1 :: Nat) (t2 :: Nat). Sing t1
-> Sing t2
-> Sing (Apply (Apply ((==@#@$) :: TyFun Nat ((~>) Nat Bool)
-> Type) t1) t2)
(%==) SZero SZero = STrue
(%==) SZero (SSucc _) = SFalse
(%==) (SSucc _) SZero = SFalse
Expand All @@ -107,11 +102,6 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
(applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210)
sB_0123456789876543210
instance SOrd Nat => SOrd Nat where
sCompare ::
forall (t1 :: Nat) (t2 :: Nat). Sing t1
-> Sing t2
-> Sing (Apply (Apply (CompareSym0 :: TyFun Nat ((~>) Nat Ordering)
-> Type) t1) t2)
sCompare SZero SZero
= applySing
(applySing
Expand Down Expand Up @@ -1670,11 +1660,6 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
= case toSing b :: SomeSing [Attribute] of
SomeSing c -> SomeSing (SSch c)
instance (SEq U, SEq Nat) => SEq U where
(%==) ::
forall (t1 :: U) (t2 :: U). Sing t1
-> Sing t2
-> Sing (Apply (Apply ((==@#@$) :: TyFun U ((~>) U Bool)
-> Type) t1) t2)
(%==) SBOOL SBOOL = STrue
(%==) SBOOL SSTRING = SFalse
(%==) SBOOL SNAT = SFalse
Expand Down Expand Up @@ -1705,14 +1690,6 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
(applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210)
sB_0123456789876543210)
instance (SShow U, SShow Nat) => SShow U where
sShowsPrec ::
forall (t1 :: GHC.Num.Natural.Natural)
(t2 :: U)
(t3 :: Symbol). Sing t1
-> Sing t2
-> Sing t3
-> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Num.Natural.Natural ((~>) U ((~>) Symbol Symbol))
-> Type) t1) t2) t3)
sShowsPrec
_
SBOOL
Expand Down Expand Up @@ -1772,14 +1749,6 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
sArg_0123456789876543210)))))
sA_0123456789876543210
instance SShow AChar where
sShowsPrec ::
forall (t1 :: GHC.Num.Natural.Natural)
(t2 :: AChar)
(t3 :: Symbol). Sing t1
-> Sing t2
-> Sing t3
-> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Num.Natural.Natural ((~>) AChar ((~>) Symbol Symbol))
-> Type) t1) t2) t3)
sShowsPrec
_
SCA
Expand Down Expand Up @@ -1989,11 +1958,6 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
(singFun2 @ShowStringSym0 sShowString) (sing :: Sing "CZ"))
sA_0123456789876543210
instance SEq AChar where
(%==) ::
forall (t1 :: AChar) (t2 :: AChar). Sing t1
-> Sing t2
-> Sing (Apply (Apply ((==@#@$) :: TyFun AChar ((~>) AChar Bool)
-> Type) t1) t2)
(%==) SCA SCA = STrue
(%==) SCA SCB = SFalse
(%==) SCA SCC = SFalse
Expand Down
10 changes: 0 additions & 10 deletions singletons-base/tests/compile-and-dump/Singletons/BoundedDeriving.golden
View file
Original file line number Diff line number Diff line change
Expand Up @@ -220,28 +220,18 @@ Singletons/BoundedDeriving.hs:(0,0)-(0,0): Splicing declarations
of
(,) (SomeSing c) (SomeSing c) -> SomeSing (SPair c c)
instance SBounded Foo1 where
sMinBound :: Sing (MinBoundSym0 :: Foo1)
sMaxBound :: Sing (MaxBoundSym0 :: Foo1)
sMinBound = SFoo1
sMaxBound = SFoo1
instance SBounded Foo2 where
sMinBound :: Sing (MinBoundSym0 :: Foo2)
sMaxBound :: Sing (MaxBoundSym0 :: Foo2)
sMinBound = SA
sMaxBound = SE
instance SBounded a => SBounded (Foo3 a) where
sMinBound :: Sing (MinBoundSym0 :: Foo3 a)
sMaxBound :: Sing (MaxBoundSym0 :: Foo3 a)
sMinBound = applySing (singFun1 @Foo3Sym0 SFoo3) sMinBound
sMaxBound = applySing (singFun1 @Foo3Sym0 SFoo3) sMaxBound
instance SBounded (Foo4 a b) where
sMinBound :: Sing (MinBoundSym0 :: Foo4 a b)
sMaxBound :: Sing (MaxBoundSym0 :: Foo4 a b)
sMinBound = SFoo41
sMaxBound = SFoo42
instance SBounded Bool => SBounded Pair where
sMinBound :: Sing (MinBoundSym0 :: Pair)
sMaxBound :: Sing (MaxBoundSym0 :: Pair)
sMinBound
= applySing
(applySing (singFun2 @PairSym0 SPair) sMinBound) sMinBound
Expand Down
25 changes: 0 additions & 25 deletions singletons-base/tests/compile-and-dump/Singletons/Classes.golden
View file
Original file line number Diff line number Diff line change
Expand Up @@ -376,31 +376,16 @@ Singletons/Classes.hs:(0,0)-(0,0): Splicing declarations
(singFun2 @MycompareSym0 sMycompare) sA_0123456789876543210)
sA_0123456789876543210
instance SMyOrd Nat where
sMycompare ::
(forall (t :: Nat) (t :: Nat).
Sing t
-> Sing t
-> Sing (Apply (Apply MycompareSym0 t) t :: Ordering) :: Type)
sMycompare SZero SZero = SEQ
sMycompare SZero (SSucc _) = SLT
sMycompare (SSucc _) SZero = SGT
sMycompare (SSucc (sN :: Sing n)) (SSucc (sM :: Sing m))
= applySing (applySing (singFun2 @MycompareSym0 sMycompare) sM) sN
instance SMyOrd () where
sMycompare ::
(forall (t :: ()) (t :: ()).
Sing t
-> Sing t
-> Sing (Apply (Apply MycompareSym0 t) t :: Ordering) :: Type)
sMycompare _ (sA_0123456789876543210 :: Sing a_0123456789876543210)
= applySing
(applySing (singFun2 @ConstSym0 sConst) SEQ) sA_0123456789876543210
instance SMyOrd Foo where
sMycompare ::
(forall (t :: Foo) (t :: Foo).
Sing t
-> Sing t
-> Sing (Apply (Apply MycompareSym0 t) t :: Ordering) :: Type)
sMycompare
(sA_0123456789876543210 :: Sing a_0123456789876543210)
(sA_0123456789876543210 :: Sing a_0123456789876543210)
Expand All @@ -409,11 +394,6 @@ Singletons/Classes.hs:(0,0)-(0,0): Splicing declarations
(singFun2 @FooCompareSym0 sFooCompare) sA_0123456789876543210)
sA_0123456789876543210
instance SEq Foo2 where
(%==) ::
forall (t1 :: Foo2) (t2 :: Foo2). Sing t1
-> Sing t2
-> Sing (Apply (Apply ((==@#@$) :: TyFun Foo2 ((~>) Foo2 Bool)
-> Type) t1) t2)
(%==) SF SF = STrue
(%==) SG SG = STrue
(%==) SF SG = SFalse
Expand Down Expand Up @@ -596,11 +576,6 @@ Singletons/Classes.hs:(0,0)-(0,0): Splicing declarations
= case toSing b :: SomeSing Nat' of
SomeSing c -> SomeSing (SSucc' c)
instance SMyOrd Nat' where
sMycompare ::
forall (t :: Nat') (t :: Nat'). Sing t
-> Sing t
-> Sing (Apply (Apply (MycompareSym0 :: TyFun Nat' ((~>) Nat' Ordering)
-> Type) t) t)
sMycompare SZero' SZero' = SEQ
sMycompare SZero' (SSucc' _) = SLT
sMycompare (SSucc' _) SZero' = SGT
Expand Down
5 changes: 0 additions & 5 deletions singletons-base/tests/compile-and-dump/Singletons/Classes2.golden
View file
Original file line number Diff line number Diff line change
Expand Up @@ -74,11 +74,6 @@ Singletons/Classes2.hs:(0,0)-(0,0): Splicing declarations
= case toSing b :: SomeSing NatFoo of
SomeSing c -> SomeSing (SSuccFoo c)
instance SMyOrd NatFoo where
sMycompare ::
forall (t1 :: NatFoo) (t2 :: NatFoo). Sing t1
-> Sing t2
-> Sing (Apply (Apply (MycompareSym0 :: TyFun NatFoo ((~>) NatFoo Ordering)
-> Type) t1) t2)
sMycompare SZeroFoo SZeroFoo = SEQ
sMycompare SZeroFoo (SSuccFoo _) = SLT
sMycompare (SSuccFoo _) SZeroFoo = SGT
Expand Down
8 changes: 0 additions & 8 deletions singletons-base/tests/compile-and-dump/Singletons/DataValues.golden
View file
Original file line number Diff line number Diff line change
Expand Up @@ -142,14 +142,6 @@ Singletons/DataValues.hs:(0,0)-(0,0): Splicing declarations
= case (,) (toSing b :: SomeSing a) (toSing b :: SomeSing b) of
(,) (SomeSing c) (SomeSing c) -> SomeSing (SPair c c)
instance (SShow a, SShow b) => SShow (Pair a b) where
sShowsPrec ::
forall (t1 :: GHC.Num.Natural.Natural)
(t2 :: Pair a b)
(t3 :: Symbol). Sing t1
-> Sing t2
-> Sing t3
-> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Num.Natural.Natural ((~>) (Pair a b) ((~>) Symbol Symbol))
-> Type) t1) t2) t3)
sShowsPrec
(sP_0123456789876543210 :: Sing p_0123456789876543210)
(SPair (sArg_0123456789876543210 :: Sing arg_0123456789876543210)
Expand Down
8 changes: 0 additions & 8 deletions singletons-base/tests/compile-and-dump/Singletons/EmptyShowDeriving.golden
View file
Original file line number Diff line number Diff line change
Expand Up @@ -53,14 +53,6 @@ Singletons/EmptyShowDeriving.hs:(0,0)-(0,0): Splicing declarations
fromSing x = case x of {}
toSing x = SomeSing (case x of {})
instance SShow Foo where
sShowsPrec ::
forall (t1 :: GHC.Num.Natural.Natural)
(t2 :: Foo)
(t3 :: GHC.Types.Symbol). Sing t1
-> Sing t2
-> Sing t3
-> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Num.Natural.Natural ((~>) Foo ((~>) GHC.Types.Symbol GHC.Types.Symbol))
-> Type) t1) t2) t3)
sShowsPrec
_
(sV_0123456789876543210 :: Sing v_0123456789876543210)
Expand Down
16 changes: 0 additions & 16 deletions singletons-base/tests/compile-and-dump/Singletons/EnumDeriving.golden
View file
Original file line number Diff line number Diff line change
Expand Up @@ -96,14 +96,6 @@ Singletons/EnumDeriving.hs:(0,0)-(0,0): Splicing declarations
toSing Q1 = SomeSing SQ1
toSing Q2 = SomeSing SQ2
instance SEnum Foo where
sToEnum ::
forall (t :: GHC.Num.Natural.Natural). Sing t
-> Sing (Apply (Data.Singletons.Base.Enum.ToEnumSym0 :: TyFun GHC.Num.Natural.Natural Foo
-> Type) t)
sFromEnum ::
forall (t :: Foo). Sing t
-> Sing (Apply (Data.Singletons.Base.Enum.FromEnumSym0 :: TyFun Foo GHC.Num.Natural.Natural
-> Type) t)
sToEnum (sN :: Sing n)
= id
@(Sing (Case_0123456789876543210 n (Apply (Apply (==@#@$) n) (FromInteger 0))))
Expand Down Expand Up @@ -192,14 +184,6 @@ Singletons/EnumDeriving.hs:0:0:: Splicing declarations
type ToEnum a = Apply ToEnum_0123456789876543210Sym0 a
type FromEnum a = Apply FromEnum_0123456789876543210Sym0 a
instance SEnum Quux where
sToEnum ::
forall (t :: GHC.Num.Natural.Natural). Sing t
-> Sing (Apply (Data.Singletons.Base.Enum.ToEnumSym0 :: TyFun GHC.Num.Natural.Natural Quux
-> Type) t)
sFromEnum ::
forall (t :: Quux). Sing t
-> Sing (Apply (Data.Singletons.Base.Enum.FromEnumSym0 :: TyFun Quux GHC.Num.Natural.Natural
-> Type) t)
sToEnum (sN :: Sing n)
= id
@(Sing (Case_0123456789876543210 n (Apply (Apply (==@#@$) n) (FromInteger 0))))
Expand Down
10 changes: 0 additions & 10 deletions singletons-base/tests/compile-and-dump/Singletons/EqInstances.golden
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,11 +31,6 @@ Singletons/EqInstances.hs:0:0:: Splicing declarations
instance PEq Foo where
type (==) a a = Apply (Apply TFHelper_0123456789876543210Sym0 a) a
instance SEq Foo => SEq Foo where
(%==) ::
forall (t1 :: Foo) (t2 :: Foo). Sing t1
-> Sing t2
-> Sing (Apply (Apply ((==@#@$) :: TyFun Foo ((~>) Foo Bool)
-> Type) t1) t2)
(%==) SFLeaf SFLeaf = STrue
(%==) SFLeaf ((:%+:) _ _) = SFalse
(%==) ((:%+:) _ _) SFLeaf = SFalse
Expand Down Expand Up @@ -80,9 +75,4 @@ Singletons/EqInstances.hs:0:0:: Splicing declarations
instance PEq Empty where
type (==) a a = Apply (Apply TFHelper_0123456789876543210Sym0 a) a
instance SEq Empty where
(%==) ::
forall (t1 :: Empty) (t2 :: Empty). Sing t1
-> Sing t2
-> Sing (Apply (Apply ((==@#@$) :: TyFun Empty ((~>) Empty Bool)
-> Type) t1) t2)
(%==) _ _ = STrue
6 changes: 0 additions & 6 deletions singletons-base/tests/compile-and-dump/Singletons/FunDeps.golden
View file
Original file line number Diff line number Diff line change
Expand Up @@ -90,12 +90,6 @@ Singletons/FunDeps.hs:(0,0)-(0,0): Splicing declarations
sL2r ::
(forall (t :: a). Sing t -> Sing (Apply L2rSym0 t :: b) :: Type)
instance SFD Bool Natural where
sMeth ::
(forall (t :: Bool).
Sing t -> Sing (Apply MethSym0 t :: Bool) :: Type)
sL2r ::
(forall (t :: Bool).
Sing t -> Sing (Apply L2rSym0 t :: Natural) :: Type)
sMeth (sA_0123456789876543210 :: Sing a_0123456789876543210)
= applySing (singFun1 @NotSym0 sNot) sA_0123456789876543210
sL2r SFalse = sFromInteger (sing :: Sing 0)
Expand Down
Loading

0 comments on commit b9b357b

Please sign in to comment.