From 5c6467878cac6c806b9b6331aad6c65f5b2a0b3d Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Thu, 2 May 2024 06:44:20 -0400 Subject: [PATCH] singletons-th: Adapt to GHC 9.10's lack of arity inference MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 | 67 +++++++++++++++++++ .../src/Control/Applicative/Singletons.hs | 1 + .../src/Control/Monad/Fail/Singletons.hs | 1 + .../src/Control/Monad/Singletons.hs | 1 + .../src/Control/Monad/Singletons/Internal.hs | 1 + .../src/Control/Monad/Zip/Singletons.hs | 1 + singletons-base/src/Data/Bool/Singletons.hs | 1 + singletons-base/src/Data/Either/Singletons.hs | 1 + singletons-base/src/Data/Eq/Singletons.hs | 1 + .../src/Data/Foldable/Singletons.hs | 1 + .../src/Data/Function/Singletons.hs | 1 + .../src/Data/Functor/Compose/Singletons.hs | 1 + .../src/Data/Functor/Const/Singletons.hs | 1 + .../src/Data/Functor/Identity/Singletons.hs | 1 + .../src/Data/Functor/Product/Singletons.hs | 1 + .../src/Data/Functor/Singletons.hs | 1 + .../src/Data/Functor/Sum/Singletons.hs | 1 + .../src/Data/List/NonEmpty/Singletons.hs | 1 + .../src/Data/List/Singletons/Internal.hs | 1 + .../Singletons/Internal/Disambiguation.hs | 1 + singletons-base/src/Data/Maybe/Singletons.hs | 1 + singletons-base/src/Data/Monoid/Singletons.hs | 1 + singletons-base/src/Data/Ord/Singletons.hs | 1 + .../src/Data/Ord/Singletons/Disambiguation.hs | 1 + singletons-base/src/Data/Proxy/Singletons.hs | 1 + .../src/Data/Semigroup/Singletons.hs | 1 + .../Semigroup/Singletons/Internal/Classes.hs | 1 + .../Singletons/Internal/Disambiguation.hs | 1 + .../Semigroup/Singletons/Internal/Wrappers.hs | 1 + .../src/Data/Singletons/Base/Enum.hs | 1 + .../src/Data/Singletons/Base/Instances.hs | 1 + .../src/Data/Singletons/Base/PolyError.hs | 1 + .../src/Data/Singletons/Base/TypeError.hs | 1 + singletons-base/src/Data/String/Singletons.hs | 1 + .../src/Data/Traversable/Singletons.hs | 1 + singletons-base/src/Data/Tuple/Singletons.hs | 1 + singletons-base/src/Data/Void/Singletons.hs | 1 + singletons-base/src/GHC/Base/Singletons.hs | 1 + singletons-base/src/GHC/Num/Singletons.hs | 1 + .../src/GHC/TypeLits/Singletons/Internal.hs | 1 + singletons-base/src/Text/Show/Singletons.hs | 1 + singletons-th/CHANGES.md | 8 +++ .../src/Data/Singletons/TH/Promote.hs | 61 ++++++++++++++++- .../src/Data/Singletons/TH/Promote/Defun.hs | 36 ++++++++-- 44 files changed, 204 insertions(+), 8 deletions(-) diff --git a/README.md b/README.md index f9bc9d13..58534791 100644 --- a/README.md +++ b/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: diff --git a/singletons-base/src/Control/Applicative/Singletons.hs b/singletons-base/src/Control/Applicative/Singletons.hs index 1da89347..5b77fdec 100644 --- a/singletons-base/src/Control/Applicative/Singletons.hs +++ b/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 #-} diff --git a/singletons-base/src/Control/Monad/Fail/Singletons.hs b/singletons-base/src/Control/Monad/Fail/Singletons.hs index 956e67a5..f2b99b03 100644 --- a/singletons-base/src/Control/Monad/Fail/Singletons.hs +++ b/singletons-base/src/Control/Monad/Fail/Singletons.hs @@ -1,5 +1,6 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeAbstractions #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} diff --git a/singletons-base/src/Control/Monad/Singletons.hs b/singletons-base/src/Control/Monad/Singletons.hs index 97a15d03..53281fab 100644 --- a/singletons-base/src/Control/Monad/Singletons.hs +++ b/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 #-} diff --git a/singletons-base/src/Control/Monad/Singletons/Internal.hs b/singletons-base/src/Control/Monad/Singletons/Internal.hs index 133e50c6..67508006 100644 --- a/singletons-base/src/Control/Monad/Singletons/Internal.hs +++ b/singletons-base/src/Control/Monad/Singletons/Internal.hs @@ -2,6 +2,7 @@ {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE NoNamedWildCards #-} {-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeAbstractions #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} diff --git a/singletons-base/src/Control/Monad/Zip/Singletons.hs b/singletons-base/src/Control/Monad/Zip/Singletons.hs index 21d286d3..c60f53f8 100644 --- a/singletons-base/src/Control/Monad/Zip/Singletons.hs +++ b/singletons-base/src/Control/Monad/Zip/Singletons.hs @@ -1,6 +1,7 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeAbstractions #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} diff --git a/singletons-base/src/Data/Bool/Singletons.hs b/singletons-base/src/Data/Bool/Singletons.hs index 3583fc8a..da94a751 100644 --- a/singletons-base/src/Data/Bool/Singletons.hs +++ b/singletons-base/src/Data/Bool/Singletons.hs @@ -1,6 +1,7 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE NoNamedWildCards #-} {-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeAbstractions #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} diff --git a/singletons-base/src/Data/Either/Singletons.hs b/singletons-base/src/Data/Either/Singletons.hs index 55edf347..c7e63881 100644 --- a/singletons-base/src/Data/Either/Singletons.hs +++ b/singletons-base/src/Data/Either/Singletons.hs @@ -1,5 +1,6 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeAbstractions #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} diff --git a/singletons-base/src/Data/Eq/Singletons.hs b/singletons-base/src/Data/Eq/Singletons.hs index 1e4887e8..5fa0b297 100644 --- a/singletons-base/src/Data/Eq/Singletons.hs +++ b/singletons-base/src/Data/Eq/Singletons.hs @@ -1,6 +1,7 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeAbstractions #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} diff --git a/singletons-base/src/Data/Foldable/Singletons.hs b/singletons-base/src/Data/Foldable/Singletons.hs index 854205a2..9b56db26 100644 --- a/singletons-base/src/Data/Foldable/Singletons.hs +++ b/singletons-base/src/Data/Foldable/Singletons.hs @@ -2,6 +2,7 @@ {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE NoNamedWildCards #-} {-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeAbstractions #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} diff --git a/singletons-base/src/Data/Function/Singletons.hs b/singletons-base/src/Data/Function/Singletons.hs index f73e89bb..e781ae43 100644 --- a/singletons-base/src/Data/Function/Singletons.hs +++ b/singletons-base/src/Data/Function/Singletons.hs @@ -1,5 +1,6 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeAbstractions #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} diff --git a/singletons-base/src/Data/Functor/Compose/Singletons.hs b/singletons-base/src/Data/Functor/Compose/Singletons.hs index a3e49cb8..056971fc 100644 --- a/singletons-base/src/Data/Functor/Compose/Singletons.hs +++ b/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 #-} diff --git a/singletons-base/src/Data/Functor/Const/Singletons.hs b/singletons-base/src/Data/Functor/Const/Singletons.hs index 990415dc..c0ee9d0f 100644 --- a/singletons-base/src/Data/Functor/Const/Singletons.hs +++ b/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 #-} diff --git a/singletons-base/src/Data/Functor/Identity/Singletons.hs b/singletons-base/src/Data/Functor/Identity/Singletons.hs index 1ab2008d..2d189f54 100644 --- a/singletons-base/src/Data/Functor/Identity/Singletons.hs +++ b/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 #-} diff --git a/singletons-base/src/Data/Functor/Product/Singletons.hs b/singletons-base/src/Data/Functor/Product/Singletons.hs index 9c57de73..b31e1125 100644 --- a/singletons-base/src/Data/Functor/Product/Singletons.hs +++ b/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 #-} diff --git a/singletons-base/src/Data/Functor/Singletons.hs b/singletons-base/src/Data/Functor/Singletons.hs index d26cc98d..5ebdde94 100644 --- a/singletons-base/src/Data/Functor/Singletons.hs +++ b/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 #-} diff --git a/singletons-base/src/Data/Functor/Sum/Singletons.hs b/singletons-base/src/Data/Functor/Sum/Singletons.hs index b852c962..d216dd32 100644 --- a/singletons-base/src/Data/Functor/Sum/Singletons.hs +++ b/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 #-} diff --git a/singletons-base/src/Data/List/NonEmpty/Singletons.hs b/singletons-base/src/Data/List/NonEmpty/Singletons.hs index 49996d96..0f0c0b16 100644 --- a/singletons-base/src/Data/List/NonEmpty/Singletons.hs +++ b/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 #-} diff --git a/singletons-base/src/Data/List/Singletons/Internal.hs b/singletons-base/src/Data/List/Singletons/Internal.hs index b030954f..4d93b051 100644 --- a/singletons-base/src/Data/List/Singletons/Internal.hs +++ b/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 #-} diff --git a/singletons-base/src/Data/List/Singletons/Internal/Disambiguation.hs b/singletons-base/src/Data/List/Singletons/Internal/Disambiguation.hs index 3409daed..ea49f46b 100644 --- a/singletons-base/src/Data/List/Singletons/Internal/Disambiguation.hs +++ b/singletons-base/src/Data/List/Singletons/Internal/Disambiguation.hs @@ -1,5 +1,6 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeAbstractions #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} diff --git a/singletons-base/src/Data/Maybe/Singletons.hs b/singletons-base/src/Data/Maybe/Singletons.hs index 0047894b..2045f3e2 100644 --- a/singletons-base/src/Data/Maybe/Singletons.hs +++ b/singletons-base/src/Data/Maybe/Singletons.hs @@ -1,5 +1,6 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeAbstractions #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} diff --git a/singletons-base/src/Data/Monoid/Singletons.hs b/singletons-base/src/Data/Monoid/Singletons.hs index b5996437..1c72d069 100644 --- a/singletons-base/src/Data/Monoid/Singletons.hs +++ b/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 #-} diff --git a/singletons-base/src/Data/Ord/Singletons.hs b/singletons-base/src/Data/Ord/Singletons.hs index af830175..633ae6d5 100644 --- a/singletons-base/src/Data/Ord/Singletons.hs +++ b/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 #-} diff --git a/singletons-base/src/Data/Ord/Singletons/Disambiguation.hs b/singletons-base/src/Data/Ord/Singletons/Disambiguation.hs index 4abf5519..fb6a8643 100644 --- a/singletons-base/src/Data/Ord/Singletons/Disambiguation.hs +++ b/singletons-base/src/Data/Ord/Singletons/Disambiguation.hs @@ -1,5 +1,6 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeAbstractions #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} diff --git a/singletons-base/src/Data/Proxy/Singletons.hs b/singletons-base/src/Data/Proxy/Singletons.hs index 13f654d8..2a07ff9c 100644 --- a/singletons-base/src/Data/Proxy/Singletons.hs +++ b/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 #-} diff --git a/singletons-base/src/Data/Semigroup/Singletons.hs b/singletons-base/src/Data/Semigroup/Singletons.hs index 96754239..0edae4ce 100644 --- a/singletons-base/src/Data/Semigroup/Singletons.hs +++ b/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 #-} diff --git a/singletons-base/src/Data/Semigroup/Singletons/Internal/Classes.hs b/singletons-base/src/Data/Semigroup/Singletons/Internal/Classes.hs index e1db75cf..f5c9dd02 100644 --- a/singletons-base/src/Data/Semigroup/Singletons/Internal/Classes.hs +++ b/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 #-} diff --git a/singletons-base/src/Data/Semigroup/Singletons/Internal/Disambiguation.hs b/singletons-base/src/Data/Semigroup/Singletons/Internal/Disambiguation.hs index f76c1703..d4f016b4 100644 --- a/singletons-base/src/Data/Semigroup/Singletons/Internal/Disambiguation.hs +++ b/singletons-base/src/Data/Semigroup/Singletons/Internal/Disambiguation.hs @@ -1,5 +1,6 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeAbstractions #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} diff --git a/singletons-base/src/Data/Semigroup/Singletons/Internal/Wrappers.hs b/singletons-base/src/Data/Semigroup/Singletons/Internal/Wrappers.hs index 2dc84727..91130408 100644 --- a/singletons-base/src/Data/Semigroup/Singletons/Internal/Wrappers.hs +++ b/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 #-} diff --git a/singletons-base/src/Data/Singletons/Base/Enum.hs b/singletons-base/src/Data/Singletons/Base/Enum.hs index b2fcd0d4..9e32f8fb 100644 --- a/singletons-base/src/Data/Singletons/Base/Enum.hs +++ b/singletons-base/src/Data/Singletons/Base/Enum.hs @@ -1,6 +1,7 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeAbstractions #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} diff --git a/singletons-base/src/Data/Singletons/Base/Instances.hs b/singletons-base/src/Data/Singletons/Base/Instances.hs index 7b25fe58..46158f4f 100644 --- a/singletons-base/src/Data/Singletons/Base/Instances.hs +++ b/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 #-} diff --git a/singletons-base/src/Data/Singletons/Base/PolyError.hs b/singletons-base/src/Data/Singletons/Base/PolyError.hs index 00c80410..e504a832 100644 --- a/singletons-base/src/Data/Singletons/Base/PolyError.hs +++ b/singletons-base/src/Data/Singletons/Base/PolyError.hs @@ -1,5 +1,6 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeAbstractions #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} diff --git a/singletons-base/src/Data/Singletons/Base/TypeError.hs b/singletons-base/src/Data/Singletons/Base/TypeError.hs index a38fb860..cd9a7af1 100644 --- a/singletons-base/src/Data/Singletons/Base/TypeError.hs +++ b/singletons-base/src/Data/Singletons/Base/TypeError.hs @@ -1,5 +1,6 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeAbstractions #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} diff --git a/singletons-base/src/Data/String/Singletons.hs b/singletons-base/src/Data/String/Singletons.hs index cdeab97d..6fee4438 100644 --- a/singletons-base/src/Data/String/Singletons.hs +++ b/singletons-base/src/Data/String/Singletons.hs @@ -1,5 +1,6 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeAbstractions #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} diff --git a/singletons-base/src/Data/Traversable/Singletons.hs b/singletons-base/src/Data/Traversable/Singletons.hs index 65e226ed..49e829f7 100644 --- a/singletons-base/src/Data/Traversable/Singletons.hs +++ b/singletons-base/src/Data/Traversable/Singletons.hs @@ -2,6 +2,7 @@ {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE NoNamedWildCards #-} {-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeAbstractions #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} diff --git a/singletons-base/src/Data/Tuple/Singletons.hs b/singletons-base/src/Data/Tuple/Singletons.hs index 1cd1036c..1c8b0e48 100644 --- a/singletons-base/src/Data/Tuple/Singletons.hs +++ b/singletons-base/src/Data/Tuple/Singletons.hs @@ -1,5 +1,6 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeAbstractions #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} diff --git a/singletons-base/src/Data/Void/Singletons.hs b/singletons-base/src/Data/Void/Singletons.hs index 474c38b2..a7609520 100644 --- a/singletons-base/src/Data/Void/Singletons.hs +++ b/singletons-base/src/Data/Void/Singletons.hs @@ -1,5 +1,6 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeAbstractions #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} diff --git a/singletons-base/src/GHC/Base/Singletons.hs b/singletons-base/src/GHC/Base/Singletons.hs index 2cc6d523..8c5a4c1f 100644 --- a/singletons-base/src/GHC/Base/Singletons.hs +++ b/singletons-base/src/GHC/Base/Singletons.hs @@ -1,5 +1,6 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeAbstractions #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} diff --git a/singletons-base/src/GHC/Num/Singletons.hs b/singletons-base/src/GHC/Num/Singletons.hs index c49f44cc..f511e52a 100644 --- a/singletons-base/src/GHC/Num/Singletons.hs +++ b/singletons-base/src/GHC/Num/Singletons.hs @@ -2,6 +2,7 @@ {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE NoStarIsType #-} {-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeAbstractions #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} diff --git a/singletons-base/src/GHC/TypeLits/Singletons/Internal.hs b/singletons-base/src/GHC/TypeLits/Singletons/Internal.hs index 2bf6efc2..d9ae4480 100644 --- a/singletons-base/src/GHC/TypeLits/Singletons/Internal.hs +++ b/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 #-} diff --git a/singletons-base/src/Text/Show/Singletons.hs b/singletons-base/src/Text/Show/Singletons.hs index bc05411a..5c405721 100644 --- a/singletons-base/src/Text/Show/Singletons.hs +++ b/singletons-base/src/Text/Show/Singletons.hs @@ -1,6 +1,7 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeAbstractions #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} diff --git a/singletons-th/CHANGES.md b/singletons-th/CHANGES.md index a727a9dd..41f669bf 100644 --- a/singletons-th/CHANGES.md +++ b/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. diff --git a/singletons-th/src/Data/Singletons/TH/Promote.hs b/singletons-th/src/Data/Singletons/TH/Promote.hs index 5d5a8db3..5878cce0 100644 --- a/singletons-th/src/Data/Singletons/TH/Promote.hs +++ b/singletons-th/src/Data/Singletons/TH/Promote.hs @@ -786,6 +786,15 @@ promoteLetDecRHS rhs_sort type_env fix_env mb_let_uniq name let_dec_rhs = do ) -- 2(b). We have a standalone kind signature. Just sak -> + -- Compute the type variable binders needed to give the type + -- family the correct arity. + -- See Note [Generating type families with the correct arity]. + let tvbs' | null tvbs + = changeDTVFlags SpecifiedSpec $ + toposortTyVarsOf (argKs ++ [resK]) + | otherwise + = tvbs + arg_tvbs' = tvbSpecsToBndrVis tvbs' ++ arg_tvbs in ( lde_kvs_to_bind' , Just $ DKiSigD proName sak , DefunSAK sak @@ -793,7 +802,7 @@ promoteLetDecRHS rhs_sort type_env fix_env mb_let_uniq name let_dec_rhs = do -- the body of the type family declaration even if it is -- given a standalone kind signature. -- See Note [Keep redundant kind information for Haddocks]. - , mk_tf_head arg_tvbs (DKindSig resK) + , mk_tf_head arg_tvbs' (DKindSig resK) ) defun_decs <- defunctionalize proName m_fixity defun_ki @@ -957,6 +966,56 @@ information whatsoever. Until the aformentioned Haddock issue is resolved, we work around this limitation by generating the redundant argument and kind information anyway. Thankfully, this is simple to accomplish, as we already compute this information to begin with. + +Note [Generating type families with the correct arity] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +As of GHC 9.10, GHC no longer performs arity inference when kind-checking type +family declarations with standalone kind signatures. This is an important +consideration when promoting functions with top-level type signatures. For +example, we would not want to take this definition: + + f :: Maybe a + f = Nothing + +And promote it to this type family: + + type F :: Either a Bool + type family F where + F = Right True + +GHC would reject this type family because it would expect F to have arity 0, +but its definition requires arity 1. This is because the definition of F is +tantamount to writing: + + F @a = Right @a @Bool True -- This takes 1 argument, hence arity 1 + +In order to make F kind-check, we need to generate a type family header that +explicitly declares it to have arity 1, not arity 0: + + type F :: Either a Bool + type family F @a where + F = Right True + +Note the @a binder after F in the type family header. + +If the standalone kind signature lacks an outermost forall, then we simply bind +the type variables in left-to-right order, preserving dependencies (using +`toposortTyVarsOf`). If the standalone kind signature does have an outermost +`forall`, then we bind the type variables according to the order in which it +appears in the `forall`, making sure to filter out any inferred type variable +binders. For example, we would want to take this definition (from #585): + + konst :: forall a {b}. a -> b -> a + konst x _ = x + +And promote it to this type family: + + type Konst :: forall a {b}. a -> b -> a + type family Konst @a x y where + Konst @a (x :: a) (_ :: b) = x + +Note that we do not bind @b here. The `tvbSpecsToBndrVis` function is +responsible for filtering out inferred type variable binders. -} promoteClause :: Maybe Uniq diff --git a/singletons-th/src/Data/Singletons/TH/Promote/Defun.hs b/singletons-th/src/Data/Singletons/TH/Promote/Defun.hs index 7026c759..421869c9 100644 --- a/singletons-th/src/Data/Singletons/TH/Promote/Defun.hs +++ b/singletons-th/src/Data/Singletons/TH/Promote/Defun.hs @@ -263,7 +263,16 @@ defunctionalize name m_fixity defun_ki = do case res_nkss of [] -> let sat_sak_dec = mk_sak_dec sak_res_ki - sat_decs = mk_sat_decs opts n arg_tvbs (Just sak_res_ki) + -- Compute the type variable binders needed to give the type + -- family the correct arity. + -- See Note [Generating type families with the correct arity] + -- in D.S.TH.Promote. + sak_tvbs' | null sak_tvbs + = changeDTVFlags SpecifiedSpec $ + toposortTyVarsOf (sak_arg_kis ++ [sak_res_ki]) + | otherwise + = sak_tvbs + sat_decs = mk_sat_decs opts n sak_tvbs' arg_tvbs (Just sak_res_ki) in (sak_res_ki, sat_sak_dec:sat_decs) res_nk:res_nks -> let (res_ki, decs) = go (n+1) (arg_nks ++ [res_nk]) res_nks @@ -316,7 +325,7 @@ defunctionalize name m_fixity defun_ki = do go n arg_tvbs res_tvbss = case res_tvbss of [] -> - let sat_decs = mk_sat_decs opts n arg_tvbs m_res + let sat_decs = mk_sat_decs opts n [] arg_tvbs m_res in (m_res, sat_decs) res_tvb:res_tvbs -> let (m_res_ki, decs) = go (n+1) (arg_tvbs ++ [res_tvb]) res_tvbs @@ -380,15 +389,28 @@ defunctionalize name m_fixity defun_ki = do -- Generate a "fully saturated" defunction symbol, along with a fixity -- declaration (if needed). -- See Note [Fully saturated defunctionalization symbols]. - mk_sat_decs :: Options -> Int -> [DTyVarBndrVis] -> Maybe DKind -> [DDec] - mk_sat_decs opts n sat_tvbs m_sat_res = + mk_sat_decs :: + Options + -> Int + -> [DTyVarBndrSpec] + -- ^ The invisible type variable binders to put in the type family + -- head in order to give it the correct arity. + -- See Note [Generating type families with the correct arity] in + -- D.S.TH.Promote. + -> [DTyVarBndrVis] + -- ^ The visible kind arguments. + -> Maybe DKind + -- ^ The result kind (if known). + -> [DDec] + mk_sat_decs opts n sat_tvbs sat_args m_sat_res = let sat_name = defunctionalizedName opts name n sat_dec = DClosedTypeFamilyD - (DTypeFamilyHead sat_name sat_tvbs + (DTypeFamilyHead sat_name + (tvbSpecsToBndrVis sat_tvbs ++ sat_args) (maybeKindToResultSig m_sat_res) Nothing) [DTySynEqn Nothing - (foldTypeTvbs (DConT sat_name) sat_tvbs) - (foldTypeTvbs (DConT name) sat_tvbs)] + (foldTypeTvbs (DConT sat_name) sat_args) + (foldTypeTvbs (DConT name) sat_args)] sat_fixity_dec = maybeToList $ fmap (mk_fix_decl sat_name) m_fixity in sat_dec : sat_fixity_dec