singletons-th: Adapt to GHC 9.10's lack of arity inference

GHC 9.10 no longer performs arity inference in type-level declarations (see
https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0425-decl-invis-binders.rst),
and as it turns out, many of the promoted type families that `singletons-th`
generates would have the wrong arity. For instance, `singletons-th` would
promote this definition:

```hs
f :: Either a Bool
f = Right True
```

To this type family:

```hs
type F :: Either a Bool
type family F where
  F = Right True
```

With GHC 9.10 or later, however, GHC would conclude that `F` has arity 0, which
means that it should not bind any arguments (visible or invisible). The type
family equation for `F`, however, only works if `F` has arity 1! This is
because the type family equation needs to bind an invisible `@a` argument:

```hs
  F @A = Right @A @Bool True
```

To ensure that type families like `F` have the expected arity, `singletons-th`
now uses `TypeAbstractions` in more places to ensure that type family headers
bind an appropriate number of type variables, which makes the type families'
arities explicit. For instance, `singletons-th` now generates the following
code for `F`:

```hs
type F :: Either a Bool
type family F @A where -- Note the @A here, which gives it arity 1
  F = Right True
```

For more details on how this is implemented, see the new `Note [Generating type
families with the correct arity]` in `Data.Singletons.TH.Promote`.

A consequence of this change is that the average piece of
`singletons-th`–generated code is much more likely to require
`TypeAbstractions` than it did before. This explains why we now enable
`TypeAbstractions` in almost every module in `singletons-base`.

Fixes #566.

README.md

@@ -850,6 +850,7 @@ The following constructs are partially supported:
 * type families
 * `TypeApplications`
 * wildcard types
+* inferred type variable binders
 
 See the following sections for more details.
 
@@ -1229,6 +1230,72 @@ any other context. Ultimately, this is due to a GHC restriction, as GHC itself
 will forbid using wildcards in most kind-level contexts. For example, GHC will
 permit `f :: _` but reject `type F :: _`.
 
+## Inferred type variable binders
+
+`singletons-th` supports promoting inferred type variable binders in most
+circumstances. For example, `singletons-th` can promote this definition:
+
+```hs
+konst :: forall a {b}. a -> b -> a
+konst x _ = x
+```
+
+To this type family:
+
+```hs
+type Konst :: forall a {b}. a -> b -> a
+type family Konst @a x y where
+  Konst @a (x :: a) (_ :: b) = x
+```
+
+There is one (somewhat obscure) corner case that `singletons-th` cannot handle,
+which requires both of the following criteria to be met:
+
+* A definition must not have any visible arguments.
+* A definition must have an inferred type variable binder as the last type
+  variable in an outermost `forall`.
+
+For instance, `singletons-th` cannot promote this definition:
+
+```hs
+bad :: forall {a}. Either a Bool
+bad = Right True
+```
+
+This is because `singletons-th` will attempt to generate this type family:
+
+```hs
+type Bad :: forall {a}. Either a Bool
+type family Bad where
+  Bad = Right True
+```
+
+GHC will not kind-check `Bad`, however. GHC will kind-check the standalone kind
+signature and conclude that `Bad` has arity 0, i.e., that it does not bind any
+arguments (visible or invisible). However, the definition of `Bad` requires an
+arity of 1, as it implicitly binds an argument:
+
+```hs
+Bad @{a} = Right @{a} @Bool True
+```
+
+In order to make this kind-check, we would need to be able to generate something
+like this:
+
+```hs
+type Bad :: forall {a}. Either a Bool
+type family Bad @{a} where
+  Bad = Right True
+```
+
+However, GHC does not allow users to things like `@{a}`, and this is by design.
+(See [this
+part](https://github.com/ghc-proposals/ghc-proposals/blob/10290a668608d608c3f6c6010be265cf7a02e1fc/proposals/0425-decl-invis-binders.rst#alternatives)
+of the relevant GHC proposal about invisible binders in type declarations.) As
+such, there is no way for `singletons-th` to promote this definition exactly as
+written. As a workaround, you can change the `forall {a}` to `forall a`, or you
+can remove the standalone kind signature.
+
 ## Support for promotion, but not singling
 
 The following constructs are supported for promotion but not singleton generation:

singletons-base/src/Control/Applicative/Singletons.hs

@@ -1,5 +1,6 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeAbstractions #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -Wno-orphans #-}

singletons-base/src/Control/Monad/Fail/Singletons.hs

@@ -1,5 +1,6 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeAbstractions #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 

singletons-base/src/Control/Monad/Singletons.hs

@@ -1,5 +1,6 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeAbstractions #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -Wno-orphans #-}

singletons-base/src/Control/Monad/Singletons/Internal.hs

@@ -2,6 +2,7 @@
 {-# LANGUAGE DefaultSignatures #-}
 {-# LANGUAGE NoNamedWildCards #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeAbstractions #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 

singletons-base/src/Control/Monad/Zip/Singletons.hs

@@ -1,6 +1,7 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE DefaultSignatures #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeAbstractions #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 

singletons-base/src/Data/Bool/Singletons.hs

@@ -1,6 +1,7 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE NoNamedWildCards #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeAbstractions #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 

singletons-base/src/Data/Either/Singletons.hs

@@ -1,5 +1,6 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeAbstractions #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 

singletons-base/src/Data/Eq/Singletons.hs

@@ -1,6 +1,7 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE DefaultSignatures #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeAbstractions #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 

singletons-base/src/Data/Foldable/Singletons.hs

@@ -2,6 +2,7 @@
 {-# LANGUAGE DefaultSignatures #-}
 {-# LANGUAGE NoNamedWildCards #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeAbstractions #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 

singletons-base/src/Data/Function/Singletons.hs

@@ -1,5 +1,6 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeAbstractions #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 

singletons-base/src/Data/Functor/Compose/Singletons.hs

@@ -1,5 +1,6 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeAbstractions #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -Wno-orphans #-}

singletons-base/src/Data/Functor/Const/Singletons.hs

@@ -1,6 +1,7 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE NoNamedWildCards #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeAbstractions #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -Wno-orphans #-}

singletons-base/src/Data/Functor/Identity/Singletons.hs

@@ -1,6 +1,7 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE NoNamedWildCards #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeAbstractions #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -Wno-orphans #-}

singletons-base/src/Data/Functor/Product/Singletons.hs

@@ -1,5 +1,6 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeAbstractions #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -Wno-orphans #-}

singletons-base/src/Data/Functor/Singletons.hs

@@ -1,6 +1,7 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE NoNamedWildCards #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeAbstractions #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -Wno-orphans #-}

singletons-base/src/Data/Functor/Sum/Singletons.hs

@@ -1,5 +1,6 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeAbstractions #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -Wno-orphans #-}

singletons-base/src/Data/List/NonEmpty/Singletons.hs

@@ -1,5 +1,6 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeAbstractions #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -Wno-orphans #-}

singletons-base/src/Data/List/Singletons/Internal.hs

@@ -1,6 +1,7 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE NoNamedWildCards #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeAbstractions #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -O0 #-}

singletons-base/src/Data/List/Singletons/Internal/Disambiguation.hs

@@ -1,5 +1,6 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeAbstractions #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 

singletons-base/src/Data/Maybe/Singletons.hs

@@ -1,5 +1,6 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeAbstractions #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 

singletons-base/src/Data/Monoid/Singletons.hs

@@ -2,6 +2,7 @@
 {-# LANGUAGE DefaultSignatures #-}
 {-# LANGUAGE NoNamedWildCards #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeAbstractions #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -Wno-orphans #-}

singletons-base/src/Data/Ord/Singletons.hs

@@ -1,6 +1,7 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE DefaultSignatures #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeAbstractions #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -Wno-orphans #-}

singletons-base/src/Data/Ord/Singletons/Disambiguation.hs

@@ -1,5 +1,6 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeAbstractions #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 

singletons-base/src/Data/Proxy/Singletons.hs

@@ -1,5 +1,6 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeAbstractions #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -Wno-orphans #-}

singletons-base/src/Data/Semigroup/Singletons.hs

@@ -1,6 +1,7 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE NoNamedWildCards #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeAbstractions #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -Wno-orphans #-}

singletons-base/src/Data/Semigroup/Singletons/Internal/Classes.hs

@@ -1,6 +1,7 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE DefaultSignatures #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeAbstractions #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 

singletons-base/src/Data/Semigroup/Singletons/Internal/Disambiguation.hs

@@ -1,5 +1,6 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeAbstractions #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 

singletons-base/src/Data/Semigroup/Singletons/Internal/Wrappers.hs

@@ -1,6 +1,7 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE NoNamedWildCards #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeAbstractions #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -Wno-orphans #-}

singletons-base/src/Data/Singletons/Base/Enum.hs

@@ -1,6 +1,7 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE DefaultSignatures #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeAbstractions #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 

singletons-base/src/Data/Singletons/Base/Instances.hs

@@ -1,5 +1,6 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeAbstractions #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -Wno-orphans #-}

singletons-base/src/Data/Singletons/Base/PolyError.hs

@@ -1,5 +1,6 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeAbstractions #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 

singletons-base/src/Data/Singletons/Base/TypeError.hs

@@ -1,5 +1,6 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeAbstractions #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 

singletons-base/src/Data/String/Singletons.hs

@@ -1,5 +1,6 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeAbstractions #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 

singletons-base/src/Data/Traversable/Singletons.hs

@@ -2,6 +2,7 @@
 {-# LANGUAGE DefaultSignatures #-}
 {-# LANGUAGE NoNamedWildCards #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeAbstractions #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 

singletons-base/src/Data/Tuple/Singletons.hs

@@ -1,5 +1,6 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeAbstractions #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 

singletons-base/src/Data/Void/Singletons.hs

@@ -1,5 +1,6 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeAbstractions #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 

singletons-base/src/GHC/Base/Singletons.hs

@@ -1,5 +1,6 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeAbstractions #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 

singletons-base/src/GHC/Num/Singletons.hs

@@ -2,6 +2,7 @@
 {-# LANGUAGE DefaultSignatures #-}
 {-# LANGUAGE NoStarIsType #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeAbstractions #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 

singletons-base/src/GHC/TypeLits/Singletons/Internal.hs

@@ -1,6 +1,7 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeAbstractions #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -Wno-orphans #-}

singletons-base/src/Text/Show/Singletons.hs

@@ -1,6 +1,7 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE DefaultSignatures #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeAbstractions #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 

singletons-th/CHANGES.md

@@ -4,6 +4,14 @@ Changelog for the `singletons-th` project
 next [????.??.??]
 -----------------
 * Require building with GHC 9.10.
+* GHC 9.10 removes arity inference when kind-checking type families with
+  standalone kind signatures, persuant to [this GHC
+  proposal](https://github.com/ghc-proposals/ghc-proposals/blob/10290a668608d608c3f6c6010be265cf7a02e1fc/proposals/0425-decl-invis-binders.rst#breakage-2-arity-inference).
+  In order to promote functions to type families with correct arities,
+  `singletons-th` uses `TypeAbstractions` to bind type variable binders in the
+  headers of promoted type families. As such, it is quite likely that you will
+  need to enable `TypeAbstractions` in order to make GHC accept code that
+  `singletons-th` generates.
 * Fix a bug causing definitions with type signatures using inferred type
   variable binders (e.g., `forall a {b}. a -> b -> a`) to fail to promote.