Support scoped type variables in class/instance declarations

Although #573 added some support for promoting/singling uses of scoped type variables, it did not properly support scoped type variables in class or instance declarations due to an oversight. This patch aims to correct that oversight. The key tricks to making this work are: * When promoting class or instance methods, we explicitly quantify the type variables in the "helper" type family so that we can bind them on the left-hand sides of the promoted type family equations. * In addition, we take care to only bring the _scoped_ type variables into scope over the right-hand sides of the promoted type family equations. See the new `Note [Scoped type variables and class methods]` in `Data.Singletons.TH.Promote.Monad` for the full details. Fixes #581.
goldfirere · Jun 6, 2024 · e854192 · e854192
1 parent 0c3c7dd
commit e854192
Show file tree

Hide file tree

Showing 23 changed files with 1,302 additions and 571 deletions.
diff --git a/singletons-base/tests/SingletonsBaseTestSuite.hs b/singletons-base/tests/SingletonsBaseTestSuite.hs
@@ -152,6 +152,7 @@ tests =
     , compileAndDumpStdTest "T563"
     , compileAndDumpStdTest "T567"
     , compileAndDumpStdTest "T571"
+    , compileAndDumpStdTest "T581"
     , compileAndDumpStdTest "T585"
     , compileAndDumpStdTest "TypeAbstractions"
     ],

diff --git a/singletons-base/tests/compile-and-dump/Singletons/BoundedDeriving.golden b/singletons-base/tests/compile-and-dump/Singletons/BoundedDeriving.golden
@@ -115,31 +115,31 @@ Singletons/BoundedDeriving.hs:(0,0)-(0,0): Splicing declarations
     instance PBounded Foo2 where
       type MinBound = MinBound_0123456789876543210Sym0
       type MaxBound = MaxBound_0123456789876543210Sym0
-    type MinBound_0123456789876543210 :: Foo3 a
+    type MinBound_0123456789876543210 :: forall a. Foo3 a
     type family MinBound_0123456789876543210 @a :: Foo3 a where
-      MinBound_0123456789876543210 = Apply Foo3Sym0 MinBoundSym0
-    type MinBound_0123456789876543210Sym0 :: Foo3 a
+      MinBound_0123456789876543210 @a = Apply Foo3Sym0 MinBoundSym0
+    type MinBound_0123456789876543210Sym0 :: forall a. Foo3 a
     type family MinBound_0123456789876543210Sym0 @a :: Foo3 a where
       MinBound_0123456789876543210Sym0 = MinBound_0123456789876543210
-    type MaxBound_0123456789876543210 :: Foo3 a
+    type MaxBound_0123456789876543210 :: forall a. Foo3 a
     type family MaxBound_0123456789876543210 @a :: Foo3 a where
-      MaxBound_0123456789876543210 = Apply Foo3Sym0 MaxBoundSym0
-    type MaxBound_0123456789876543210Sym0 :: Foo3 a
+      MaxBound_0123456789876543210 @a = Apply Foo3Sym0 MaxBoundSym0
+    type MaxBound_0123456789876543210Sym0 :: forall a. Foo3 a
     type family MaxBound_0123456789876543210Sym0 @a :: Foo3 a where
       MaxBound_0123456789876543210Sym0 = MaxBound_0123456789876543210
     instance PBounded (Foo3 a) where
       type MinBound = MinBound_0123456789876543210Sym0
       type MaxBound = MaxBound_0123456789876543210Sym0
-    type MinBound_0123456789876543210 :: Foo4 a b
+    type MinBound_0123456789876543210 :: forall a b. Foo4 a b
     type family MinBound_0123456789876543210 @a @b :: Foo4 a b where
-      MinBound_0123456789876543210 = Foo41Sym0
-    type MinBound_0123456789876543210Sym0 :: Foo4 a b
+      MinBound_0123456789876543210 @a @b = Foo41Sym0
+    type MinBound_0123456789876543210Sym0 :: forall a b. Foo4 a b
     type family MinBound_0123456789876543210Sym0 @a @b :: Foo4 a b where
       MinBound_0123456789876543210Sym0 = MinBound_0123456789876543210
-    type MaxBound_0123456789876543210 :: Foo4 a b
+    type MaxBound_0123456789876543210 :: forall a b. Foo4 a b
     type family MaxBound_0123456789876543210 @a @b :: Foo4 a b where
-      MaxBound_0123456789876543210 = Foo42Sym0
-    type MaxBound_0123456789876543210Sym0 :: Foo4 a b
+      MaxBound_0123456789876543210 @a @b = Foo42Sym0
+    type MaxBound_0123456789876543210Sym0 :: forall a b. Foo4 a b
     type family MaxBound_0123456789876543210Sym0 @a @b :: Foo4 a b where
       MaxBound_0123456789876543210Sym0 = MaxBound_0123456789876543210
     instance PBounded (Foo4 a b) where

diff --git a/singletons-base/tests/compile-and-dump/Singletons/Classes.golden b/singletons-base/tests/compile-and-dump/Singletons/Classes.golden
@@ -159,10 +159,10 @@ Singletons/Classes.hs:(0,0)-(0,0): Splicing declarations
     type family (<=>@#@$$$) @a (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: Ordering where
       (<=>@#@$$$) a0123456789876543210 a0123456789876543210 = (<=>) a0123456789876543210 a0123456789876543210
     infix 4 <=>@#@$$$
-    type TFHelper_0123456789876543210 :: a -> a -> Ordering
+    type TFHelper_0123456789876543210 :: forall a. a -> a -> Ordering
     type family TFHelper_0123456789876543210 @a (a :: a) (a :: a) :: Ordering where
-      TFHelper_0123456789876543210 a_0123456789876543210 a_0123456789876543210 = Apply (Apply MycompareSym0 a_0123456789876543210) a_0123456789876543210
-    type TFHelper_0123456789876543210Sym0 :: (~>) a ((~>) a Ordering)
+      TFHelper_0123456789876543210 @a (a_0123456789876543210 :: a) (a_0123456789876543210 :: a) = Apply (Apply MycompareSym0 a_0123456789876543210) a_0123456789876543210
+    type TFHelper_0123456789876543210Sym0 :: forall a. (~>) a ((~>) a Ordering)
     data TFHelper_0123456789876543210Sym0 :: (~>) a ((~>) a Ordering)
       where
         TFHelper_0123456789876543210Sym0KindInference :: SameKind (Apply TFHelper_0123456789876543210Sym0 arg) (TFHelper_0123456789876543210Sym1 arg) =>
@@ -171,7 +171,8 @@ Singletons/Classes.hs:(0,0)-(0,0): Splicing declarations
     instance SuppressUnusedWarnings TFHelper_0123456789876543210Sym0 where
       suppressUnusedWarnings
         = snd ((,) TFHelper_0123456789876543210Sym0KindInference ())
-    type TFHelper_0123456789876543210Sym1 :: a -> (~>) a Ordering
+    type TFHelper_0123456789876543210Sym1 :: forall a. a
+                                                       -> (~>) a Ordering
     data TFHelper_0123456789876543210Sym1 (a0123456789876543210 :: a) :: (~>) a Ordering
       where
         TFHelper_0123456789876543210Sym1KindInference :: SameKind (Apply (TFHelper_0123456789876543210Sym1 a0123456789876543210) arg) (TFHelper_0123456789876543210Sym2 a0123456789876543210 arg) =>
@@ -180,7 +181,8 @@ Singletons/Classes.hs:(0,0)-(0,0): Splicing declarations
     instance SuppressUnusedWarnings (TFHelper_0123456789876543210Sym1 a0123456789876543210) where
       suppressUnusedWarnings
         = snd ((,) TFHelper_0123456789876543210Sym1KindInference ())
-    type TFHelper_0123456789876543210Sym2 :: a -> a -> Ordering
+    type TFHelper_0123456789876543210Sym2 :: forall a. a
+                                                       -> a -> Ordering
     type family TFHelper_0123456789876543210Sym2 @a (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: Ordering where
       TFHelper_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = TFHelper_0123456789876543210 a0123456789876543210 a0123456789876543210
     class PMyOrd a where

diff --git a/singletons-base/tests/compile-and-dump/Singletons/DataValues.golden b/singletons-base/tests/compile-and-dump/Singletons/DataValues.golden
@@ -51,11 +51,13 @@ Singletons/DataValues.hs:(0,0)-(0,0): Splicing declarations
       Complex = Apply (Apply PairSym0 (Apply (Apply PairSym0 (Apply JustSym0 ZeroSym0)) ZeroSym0)) FalseSym0
     type family Pr where
       Pr = Apply (Apply PairSym0 (Apply SuccSym0 ZeroSym0)) (Apply (Apply (:@#@$) ZeroSym0) NilSym0)
-    type ShowsPrec_0123456789876543210 :: GHC.Num.Natural.Natural
-                                          -> Pair a b -> Symbol -> Symbol
+    type ShowsPrec_0123456789876543210 :: forall a
+                                                 b. GHC.Num.Natural.Natural
+                                                    -> Pair a b -> Symbol -> Symbol
     type family ShowsPrec_0123456789876543210 @a @b (a :: GHC.Num.Natural.Natural) (a :: Pair a b) (a :: Symbol) :: Symbol where
-      ShowsPrec_0123456789876543210 p_0123456789876543210 (Pair arg_0123456789876543210 arg_0123456789876543210) a_0123456789876543210 = Apply (Apply (Apply ShowParenSym0 (Apply (Apply (>@#@$) p_0123456789876543210) (FromInteger 10))) (Apply (Apply (.@#@$) (Apply ShowStringSym0 "Pair ")) (Apply (Apply (.@#@$) (Apply (Apply ShowsPrecSym0 (FromInteger 11)) arg_0123456789876543210)) (Apply (Apply (.@#@$) ShowSpaceSym0) (Apply (Apply ShowsPrecSym0 (FromInteger 11)) arg_0123456789876543210))))) a_0123456789876543210
-    type ShowsPrec_0123456789876543210Sym0 :: (~>) GHC.Num.Natural.Natural ((~>) (Pair a b) ((~>) Symbol Symbol))
+      ShowsPrec_0123456789876543210 @a @b (p_0123456789876543210 :: GHC.Num.Natural.Natural) (Pair arg_0123456789876543210 arg_0123456789876543210 :: Pair a b) (a_0123456789876543210 :: Symbol) = Apply (Apply (Apply ShowParenSym0 (Apply (Apply (>@#@$) p_0123456789876543210) (FromInteger 10))) (Apply (Apply (.@#@$) (Apply ShowStringSym0 "Pair ")) (Apply (Apply (.@#@$) (Apply (Apply ShowsPrecSym0 (FromInteger 11)) arg_0123456789876543210)) (Apply (Apply (.@#@$) ShowSpaceSym0) (Apply (Apply ShowsPrecSym0 (FromInteger 11)) arg_0123456789876543210))))) a_0123456789876543210
+    type ShowsPrec_0123456789876543210Sym0 :: forall a
+                                                     b. (~>) GHC.Num.Natural.Natural ((~>) (Pair a b) ((~>) Symbol Symbol))
     data ShowsPrec_0123456789876543210Sym0 :: (~>) GHC.Num.Natural.Natural ((~>) (Pair a b) ((~>) Symbol Symbol))
       where
         ShowsPrec_0123456789876543210Sym0KindInference :: SameKind (Apply ShowsPrec_0123456789876543210Sym0 arg) (ShowsPrec_0123456789876543210Sym1 arg) =>
@@ -64,8 +66,9 @@ Singletons/DataValues.hs:(0,0)-(0,0): Splicing declarations
     instance SuppressUnusedWarnings ShowsPrec_0123456789876543210Sym0 where
       suppressUnusedWarnings
         = snd ((,) ShowsPrec_0123456789876543210Sym0KindInference ())
-    type ShowsPrec_0123456789876543210Sym1 :: GHC.Num.Natural.Natural
-                                              -> (~>) (Pair a b) ((~>) Symbol Symbol)
+    type ShowsPrec_0123456789876543210Sym1 :: forall a
+                                                     b. GHC.Num.Natural.Natural
+                                                        -> (~>) (Pair a b) ((~>) Symbol Symbol)
     data ShowsPrec_0123456789876543210Sym1 (a0123456789876543210 :: GHC.Num.Natural.Natural) :: (~>) (Pair a b) ((~>) Symbol Symbol)
       where
         ShowsPrec_0123456789876543210Sym1KindInference :: SameKind (Apply (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) arg) (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 arg) =>
@@ -74,8 +77,9 @@ Singletons/DataValues.hs:(0,0)-(0,0): Splicing declarations
     instance SuppressUnusedWarnings (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) where
       suppressUnusedWarnings
         = snd ((,) ShowsPrec_0123456789876543210Sym1KindInference ())
-    type ShowsPrec_0123456789876543210Sym2 :: GHC.Num.Natural.Natural
-                                              -> Pair a b -> (~>) Symbol Symbol
+    type ShowsPrec_0123456789876543210Sym2 :: forall a
+                                                     b. GHC.Num.Natural.Natural
+                                                        -> Pair a b -> (~>) Symbol Symbol
     data ShowsPrec_0123456789876543210Sym2 (a0123456789876543210 :: GHC.Num.Natural.Natural) (a0123456789876543210 :: Pair a b) :: (~>) Symbol Symbol
       where
         ShowsPrec_0123456789876543210Sym2KindInference :: SameKind (Apply (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) arg) (ShowsPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 arg) =>
@@ -84,8 +88,9 @@ Singletons/DataValues.hs:(0,0)-(0,0): Splicing declarations
     instance SuppressUnusedWarnings (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) where
       suppressUnusedWarnings
         = snd ((,) ShowsPrec_0123456789876543210Sym2KindInference ())
-    type ShowsPrec_0123456789876543210Sym3 :: GHC.Num.Natural.Natural
-                                              -> Pair a b -> Symbol -> Symbol
+    type ShowsPrec_0123456789876543210Sym3 :: forall a
+                                                     b. GHC.Num.Natural.Natural
+                                                        -> Pair a b -> Symbol -> Symbol
     type family ShowsPrec_0123456789876543210Sym3 @a @b (a0123456789876543210 :: GHC.Num.Natural.Natural) (a0123456789876543210 :: Pair a b) (a0123456789876543210 :: Symbol) :: Symbol where
       ShowsPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 = ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
     instance PShow (Pair a b) where