Implement partial support for promoting scoped type variables

`singletons-th` can now promote a good number of uses of scoped type variables,
save for the two exceptions now listed in the `singletons` `README`. This is
accomplished by a combination of:

1. Bringing scoped type variables into scope on the left-hand sides of promoted
   type family equations through invisible `@` arguments when a function uses
   an outermost `forall` in its type signature (and does not close over any
   local variables).

2. Bringing scoped type variables into scope on the left-hand sides of promoted
   type family equations through explicit kind annotations on each of the type
   family's arguments when a function has an outermost `forall` in its type
   signature.

3. Closing over scoped type variables when lambda-lifting to ensure that the
   type variables are accessible when scoping over local definitions.

See the new `Note [Scoped type variables]` in
`Data.Singletons.TH.Promote.Monad` for more about how this is implemented.

Fixes #433.

README.md

@@ -839,6 +839,7 @@ The following constructs are fully supported:
 
 The following constructs are partially supported:
 
+* scoped type variables
 * `deriving`
 * finite arithmetic sequences
 * records
@@ -850,6 +851,132 @@ The following constructs are partially supported:
 
 See the following sections for more details.
 
+### Scoped type variables
+
+`singletons-th` makes an effort to track scoped type variables during promotion
+so that they "just work". For instance, this function:
+
+```hs
+f :: forall a. a -> a
+f x = (x :: a)
+```
+
+Will be promoted to the following type family:
+
+```hs
+type F :: forall a. a -> a
+type family F x where
+  F @a x = (x :: a)
+```
+
+Note the use of `@a` on the left-hand side of the type family equation, which
+ensures that `a` is in scope on the right-hand side. This also works for local
+definitions, so this:
+
+```hs
+f :: forall a. a -> a
+f x = g
+  where
+    g = (x :: a)
+```
+
+Will promote to the following type families:
+
+```hs
+type F :: forall a. a -> a
+type family F x where
+  F @a x = LetG a x
+
+type family LetG a x where
+  LetG a x = (x :: a)
+```
+
+Note that `LetG` includes both `a` and `x` as arguments to ensure that they are
+in scope on the right-hand side.
+
+Besides `forall`s in type signatures, scoped type variables can also come
+from pattern signatures. For example, this will also work:
+
+```hs
+f (x :: a) = g
+  where
+    g = (x :: a)
+```
+
+Not all forms of scoped type variables are currently supported:
+
+* If a type signature brings a type variable into scope over the body of a
+  function with a `forall`, then any pattern signatures must consistently use
+  the same type variable in argument types that mention it. For example, while
+  this will work:
+
+  ```hs
+  f :: forall a. a -> a
+  f (x :: a) = a -- (x :: a) mentions the same type variable `a` from the type signature
+  ```
+
+  The following will _not_ work:
+
+  ```hs
+  f' :: forall a. a -> a
+  f' (x :: b) = b -- BAD: (x :: b) mentions `b` instead of `a`
+  ```
+
+  This is because `singletons-th` would attempt to promote `f'` to the
+  following:
+
+  ```hs
+  type F' :: forall a. a -> a
+  type family F' x where
+    F' @a (x :: b) = b
+  ```
+
+  And GHC will not infer that `b` should stand for `a`.
+
+* There is limited support for local variables that themselves bring type
+  variables into scope with `forall`s in their type signatures. For example,
+  this example works:
+
+  ```hs
+  f local = g
+    where
+      g :: forall a. a -> a
+      g x = const (x :: a) local
+  ```
+
+  This is because `f` and `g` will be promoted like so:
+
+  ```hs
+  type family F local where
+    F local = G local
+
+  type family G local x where
+    G local (x :: a) = Const (x :: a) local
+  ```
+
+  It is not straightforward to give `G` a standalone kind signature, and
+  without a standalone kind signature, GHC will not allow writing `@a` on the
+  left-hand side of `G`'s type family equation. On the other hand, we can still
+  ensure that `a` is brought into scope by writing `(x :: a)` instead of `x` on
+  the left-hand side.  While the `:: a` signature was not present in the
+  original definition, we include it anyway during promotion to ensure that
+  definitions like `G` kind-check.
+
+  This trick only works if the scoped type variable is mentioned in one of the
+  local definition's arguments, however. If the scoped type variable is only
+  mentioned in the return type, then the promoted definition will not
+  kind-check. This means that examples like this one will not work:
+
+  ```hs
+  konst :: a -> Maybe Bool -> a
+  konst x _ = x
+
+  f x = konst x y
+    where
+      y :: forall b. Maybe b
+      y = Nothing :: Maybe b
+  ```
+
 ### `deriving`
 
 `singletons-th` is slightly more conservative with respect to `deriving` than
@@ -1304,7 +1431,6 @@ underyling pattern instead.
 
 The following constructs are either unsupported or almost never work:
 
-* scoped type variables
 * datatypes that store arrows or `Symbol`
 * rank-n types
 * promoting `TypeRep`s
@@ -1315,46 +1441,6 @@ The following constructs are either unsupported or almost never work:
 
 See the following sections for more details.
 
-### Scoped type variables
-
-Promoting functions that rely on the behavior of `ScopedTypeVariables` is very
-tricky—see
-[this GitHub issue](https://github.com/goldfirere/singletons/issues/433) for an
-extended discussion on the topic. This is not to say that promoting functions
-that rely on `ScopedTypeVariables` is guaranteed to fail, but it is rather
-fragile. To demonstrate how fragile this is, note that the following function
-will promote successfully:
-
-```hs
-f :: forall a. a -> a
-f x = id x :: a
-```
-
-But this one will not:
-
-```hs
-g :: forall a. a -> a
-g x = id (x :: a)
-```
-
-There are usually workarounds one can use instead of `ScopedTypeVariables`:
-
-1. Use pattern signatures:
-
-   ```hs
-   g :: forall a. a -> a
-   g (x :: a) = id (x :: a)
-   ```
-2. Use local definitions:
-
-   ```hs
-   g :: forall a. a -> a
-   g x = id' a
-     where
-       id' :: a -> a
-       id' x = x
-   ```
-
 ### Arrows, `Symbol`, and literals
 
 As described in the promotion paper, automatic promotion of datatypes that

singletons-base/tests/SingletonsBaseTestSuite.hs

@@ -132,6 +132,7 @@ tests =
     , compileAndDumpStdTest "T410"
     , compileAndDumpStdTest "T412"
     , compileAndDumpStdTest "T414"
+    , compileAndDumpStdTest "T433"
     , compileAndDumpStdTest "T443"
     , afterSingletonsNat .
       compileAndDumpStdTest "T445"

singletons-base/tests/compile-and-dump/Singletons/CaseExpressions.golden

@@ -69,28 +69,36 @@ Singletons/CaseExpressions.hs:(0,0)-(0,0): Splicing declarations
       Lambda_0123456789876543210Sym3 y0123456789876543210 x0123456789876543210 arg_01234567898765432100123456789876543210 = Lambda_0123456789876543210 y0123456789876543210 x0123456789876543210 arg_01234567898765432100123456789876543210
     type family Case_0123456789876543210 x0123456789876543210 t where
       Case_0123456789876543210 x y = Apply (Apply (Apply Lambda_0123456789876543210Sym0 y) x) y
-    data Let0123456789876543210ZSym0 y0123456789876543210
+    data Let0123456789876543210ZSym0 a0123456789876543210
       where
         Let0123456789876543210ZSym0KindInference :: SameKind (Apply Let0123456789876543210ZSym0 arg) (Let0123456789876543210ZSym1 arg) =>
-                                                    Let0123456789876543210ZSym0 y0123456789876543210
-    type instance Apply Let0123456789876543210ZSym0 y0123456789876543210 = Let0123456789876543210ZSym1 y0123456789876543210
+                                                    Let0123456789876543210ZSym0 a0123456789876543210
+    type instance Apply Let0123456789876543210ZSym0 a0123456789876543210 = Let0123456789876543210ZSym1 a0123456789876543210
     instance SuppressUnusedWarnings Let0123456789876543210ZSym0 where
       suppressUnusedWarnings
         = snd ((,) Let0123456789876543210ZSym0KindInference ())
-    data Let0123456789876543210ZSym1 y0123456789876543210 x0123456789876543210
+    data Let0123456789876543210ZSym1 a0123456789876543210 y0123456789876543210
       where
-        Let0123456789876543210ZSym1KindInference :: SameKind (Apply (Let0123456789876543210ZSym1 y0123456789876543210) arg) (Let0123456789876543210ZSym2 y0123456789876543210 arg) =>
-                                                    Let0123456789876543210ZSym1 y0123456789876543210 x0123456789876543210
-    type instance Apply (Let0123456789876543210ZSym1 y0123456789876543210) x0123456789876543210 = Let0123456789876543210Z y0123456789876543210 x0123456789876543210
-    instance SuppressUnusedWarnings (Let0123456789876543210ZSym1 y0123456789876543210) where
+        Let0123456789876543210ZSym1KindInference :: SameKind (Apply (Let0123456789876543210ZSym1 a0123456789876543210) arg) (Let0123456789876543210ZSym2 a0123456789876543210 arg) =>
+                                                    Let0123456789876543210ZSym1 a0123456789876543210 y0123456789876543210
+    type instance Apply (Let0123456789876543210ZSym1 a0123456789876543210) y0123456789876543210 = Let0123456789876543210ZSym2 a0123456789876543210 y0123456789876543210
+    instance SuppressUnusedWarnings (Let0123456789876543210ZSym1 a0123456789876543210) where
       suppressUnusedWarnings
         = snd ((,) Let0123456789876543210ZSym1KindInference ())
-    type family Let0123456789876543210ZSym2 y0123456789876543210 x0123456789876543210 :: a0123456789876543210 where
-      Let0123456789876543210ZSym2 y0123456789876543210 x0123456789876543210 = Let0123456789876543210Z y0123456789876543210 x0123456789876543210
-    type family Let0123456789876543210Z y0123456789876543210 x0123456789876543210 :: a where
-      Let0123456789876543210Z y x = y
-    type family Case_0123456789876543210 x0123456789876543210 t where
-      Case_0123456789876543210 x y = Let0123456789876543210ZSym2 y x
+    data Let0123456789876543210ZSym2 a0123456789876543210 y0123456789876543210 x0123456789876543210
+      where
+        Let0123456789876543210ZSym2KindInference :: SameKind (Apply (Let0123456789876543210ZSym2 a0123456789876543210 y0123456789876543210) arg) (Let0123456789876543210ZSym3 a0123456789876543210 y0123456789876543210 arg) =>
+                                                    Let0123456789876543210ZSym2 a0123456789876543210 y0123456789876543210 x0123456789876543210
+    type instance Apply (Let0123456789876543210ZSym2 a0123456789876543210 y0123456789876543210) x0123456789876543210 = Let0123456789876543210Z a0123456789876543210 y0123456789876543210 x0123456789876543210
+    instance SuppressUnusedWarnings (Let0123456789876543210ZSym2 a0123456789876543210 y0123456789876543210) where
+      suppressUnusedWarnings
+        = snd ((,) Let0123456789876543210ZSym2KindInference ())
+    type family Let0123456789876543210ZSym3 a0123456789876543210 y0123456789876543210 x0123456789876543210 :: a0123456789876543210 where
+      Let0123456789876543210ZSym3 a0123456789876543210 y0123456789876543210 x0123456789876543210 = Let0123456789876543210Z a0123456789876543210 y0123456789876543210 x0123456789876543210
+    type family Let0123456789876543210Z a0123456789876543210 y0123456789876543210 x0123456789876543210 :: a0123456789876543210 where
+      Let0123456789876543210Z a y x = y
+    type family Case_0123456789876543210 a0123456789876543210 x0123456789876543210 t where
+      Case_0123456789876543210 a x y = Let0123456789876543210ZSym3 a y x
     data Let0123456789876543210Scrutinee_0123456789876543210Sym0 a0123456789876543210
       where
         Let0123456789876543210Scrutinee_0123456789876543210Sym0KindInference :: SameKind (Apply Let0123456789876543210Scrutinee_0123456789876543210Sym0 arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym1 arg) =>
@@ -223,7 +231,7 @@ Singletons/CaseExpressions.hs:(0,0)-(0,0): Splicing declarations
       Foo5 x = Case_0123456789876543210 x x
     type Foo4 :: forall a. a -> a
     type family Foo4 (a :: a) :: a where
-      Foo4 x = Case_0123456789876543210 x x
+      Foo4 @a (x :: a) = Case_0123456789876543210 a x x
     type Foo3 :: a -> b -> a
     type family Foo3 (a :: a) (a :: b) :: a where
       Foo3 a b = Case_0123456789876543210 a b (Let0123456789876543210Scrutinee_0123456789876543210Sym2 a b)
@@ -262,11 +270,11 @@ Singletons/CaseExpressions.hs:(0,0)-(0,0): Splicing declarations
                     sY)
     sFoo4 (sX :: Sing x)
       = id
-          @(Sing (Case_0123456789876543210 x x))
+          @(Sing (Case_0123456789876543210 a x x))
           (case sX of
              (sY :: Sing y)
                -> let
-                    sZ :: (Sing (Let0123456789876543210ZSym2 y x :: a) :: Type)
+                    sZ :: (Sing (Let0123456789876543210ZSym3 a y x :: a) :: Type)
                     sZ = sY
                   in sZ)
     sFoo3 (sA :: Sing a) (sB :: Sing b)

singletons-base/tests/compile-and-dump/Singletons/LetStatements.golden

@@ -233,18 +233,26 @@ Singletons/LetStatements.hs:(0,0)-(0,0): Splicing declarations
       Let0123456789876543210Y x = Case_0123456789876543210 x (Let0123456789876543210X_0123456789876543210Sym1 x)
     type family Let0123456789876543210X_0123456789876543210 x0123456789876543210 where
       Let0123456789876543210X_0123456789876543210 x = Apply (Apply Tuple2Sym0 (Apply SuccSym0 x)) x
-    data Let0123456789876543210BarSym0 x0123456789876543210
+    data Let0123456789876543210BarSym0 a0123456789876543210
       where
         Let0123456789876543210BarSym0KindInference :: SameKind (Apply Let0123456789876543210BarSym0 arg) (Let0123456789876543210BarSym1 arg) =>
-                                                      Let0123456789876543210BarSym0 x0123456789876543210
-    type instance Apply Let0123456789876543210BarSym0 x0123456789876543210 = Let0123456789876543210Bar x0123456789876543210
+                                                      Let0123456789876543210BarSym0 a0123456789876543210
+    type instance Apply Let0123456789876543210BarSym0 a0123456789876543210 = Let0123456789876543210BarSym1 a0123456789876543210
     instance SuppressUnusedWarnings Let0123456789876543210BarSym0 where
       suppressUnusedWarnings
         = snd ((,) Let0123456789876543210BarSym0KindInference ())
-    type family Let0123456789876543210BarSym1 x0123456789876543210 :: a0123456789876543210 where
-      Let0123456789876543210BarSym1 x0123456789876543210 = Let0123456789876543210Bar x0123456789876543210
-    type family Let0123456789876543210Bar x0123456789876543210 :: a where
-      Let0123456789876543210Bar x = x
+    data Let0123456789876543210BarSym1 a0123456789876543210 x0123456789876543210
+      where
+        Let0123456789876543210BarSym1KindInference :: SameKind (Apply (Let0123456789876543210BarSym1 a0123456789876543210) arg) (Let0123456789876543210BarSym2 a0123456789876543210 arg) =>
+                                                      Let0123456789876543210BarSym1 a0123456789876543210 x0123456789876543210
+    type instance Apply (Let0123456789876543210BarSym1 a0123456789876543210) x0123456789876543210 = Let0123456789876543210Bar a0123456789876543210 x0123456789876543210
+    instance SuppressUnusedWarnings (Let0123456789876543210BarSym1 a0123456789876543210) where
+      suppressUnusedWarnings
+        = snd ((,) Let0123456789876543210BarSym1KindInference ())
+    type family Let0123456789876543210BarSym2 a0123456789876543210 x0123456789876543210 :: a0123456789876543210 where
+      Let0123456789876543210BarSym2 a0123456789876543210 x0123456789876543210 = Let0123456789876543210Bar a0123456789876543210 x0123456789876543210
+    type family Let0123456789876543210Bar a0123456789876543210 x0123456789876543210 :: a0123456789876543210 where
+      Let0123456789876543210Bar a x = x
     data (<<<%%%%%%%%%%%%%%%%%%%%@#@$) x0123456789876543210
       where
         (:<<<%%%%%%%%%%%%%%%%%%%%@#@$###) :: SameKind (Apply (<<<%%%%%%%%%%%%%%%%%%%%@#@$) arg) ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$) arg) =>
@@ -726,7 +734,7 @@ Singletons/LetStatements.hs:(0,0)-(0,0): Splicing declarations
       Foo13_ y = y
     type Foo13 :: forall a. a -> a
     type family Foo13 (a :: a) :: a where
-      Foo13 x = Apply Foo13_Sym0 (Let0123456789876543210BarSym1 x)
+      Foo13 @a (x :: a) = Apply Foo13_Sym0 (Let0123456789876543210BarSym2 a x)
     type Foo12 :: Nat -> Nat
     type family Foo12 (a :: Nat) :: Nat where
       Foo12 x = Apply (Apply ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x) x) (Apply SuccSym0 (Apply SuccSym0 ZeroSym0))
@@ -832,7 +840,7 @@ Singletons/LetStatements.hs:(0,0)-(0,0): Splicing declarations
     sFoo13_ (sY :: Sing y) = sY
     sFoo13 (sX :: Sing x)
       = let
-          sBar :: (Sing (Let0123456789876543210BarSym1 x :: a) :: Type)
+          sBar :: (Sing (Let0123456789876543210BarSym2 a x :: a) :: Type)
           sBar = sX
         in applySing (singFun1 @Foo13_Sym0 sFoo13_) sBar
     sFoo12 (sX :: Sing x)

singletons-base/tests/compile-and-dump/Singletons/Records.golden

@@ -46,10 +46,10 @@ Singletons/Records.hs:(0,0)-(0,0): Splicing declarations
       Field1Sym1 a0123456789876543210 = Field1 a0123456789876543210
     type Field2 :: forall a. Record a -> Bool
     type family Field2 (a :: Record a) :: Bool where
-      Field2 (MkRecord _ field) = field
+      Field2 @a (MkRecord _ field :: Record a) = field
     type Field1 :: forall a. Record a -> a
     type family Field1 (a :: Record a) :: a where
-      Field1 (MkRecord field _) = field
+      Field1 @a (MkRecord field _ :: Record a) = field
     sField2 ::
       forall a (t :: Record a). Sing t
                                 -> Sing (Apply Field2Sym0 t :: Bool)