Skip to content

Commit

Permalink
Monomorphize kinds of Error{,WithoutStackTrace}, introduce PolyError
Browse files Browse the repository at this point in the history
Previously, we had generalized the argument kind to `Error` in commit
077aee5 to permit passing things to `Error`
besides `Symbol`s. Back then, there was no way to `show` things at the type
level, nor was there a way to manipulate `Symbol`s in any meaningful fashion,
so this seemed like a reasonable choice.

Nowadays, however, the story is different. There is a type-level `Show_`
function, and the API for manipulating `Symbol`s is nearly as expressive as the
API for manipulating `String`s.  What's more, making `Error`'s argument kind
more general introduces ambiguity-related issues when deriving `Enum` instances
with `OverloadedStrings` enabled, as observed in #89.

In light of this, I have changed the API such that:

* The kind of the argument to `Error` (as well as the related
  `ErrorWithoutStackTrace` function) is now `Symbol`.  In this sense, this patch
  reverts 077aee5.
* There is now a new `Data.Singletons.Base.PolyError` module that provides a
  `PolyError` function. `PolyError` provides a kind-polymorphic `Error`
  interface much like what the previous type of `Error` was, so any existing
  code that relied on the argument of `Error` being kind-polymorphic can be
  migrated over to use `PolyError`.

Resolves #89 (hopefully for good this time).
  • Loading branch information
RyanGlScott committed Feb 18, 2023
1 parent c27df34 commit e89070a
Show file tree
Hide file tree
Showing 7 changed files with 145 additions and 12 deletions.
14 changes: 12 additions & 2 deletions singletons-base/CHANGES.md
Original file line number Diff line number Diff line change
@@ -1,8 +1,18 @@
Changelog for the `singletons-base` project
===========================================

3.1.2 [????.??.??]
------------------
3.2 [????.??.??]
----------------
* The kinds of the promoted `Error` and `ErrorWithoutStackTrace` functions have
been monomorphized to `Symbol`. A previous release generalized the kinds of
these arguments to allow passing arguments besides `Symbol`s, but this change
introduces ambiguity in derived code when `OverloadedString`s is enabled.
See [#89](https://github.com/goldfirere/singletons/issues/89) for the full
story.

If you were relying on the previous, kind-polymorphic behavior of `Error`, you
can instead use the new `Data.Singletons.Base.PolyError` module that provides
`PolyError`, a version of `Error` with a kind-polymorphic argument.
* Provide `TestEquality` and `TestCoercion` instances for `SNat, `SSymbol`, and
`SChar`.

Expand Down
3 changes: 2 additions & 1 deletion singletons-base/singletons-base.cabal
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
name: singletons-base
version: 3.1.2
version: 3.2
cabal-version: 1.24
synopsis: A promoted and singled version of the base library
homepage: http://www.github.com/goldfirere/singletons
Expand Down Expand Up @@ -84,6 +84,7 @@ library
exposed-modules: Data.Singletons.Base.CustomStar
Data.Singletons.Base.Enum
Data.Singletons.Base.TH
Data.Singletons.Base.PolyError
Data.Singletons.Base.SomeSing
Data.Singletons.Base.TypeError
Data.Singletons.Base.TypeRepTYPE
Expand Down
28 changes: 28 additions & 0 deletions singletons-base/src/Data/Singletons/Base/PolyError.hs
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

-----------------------------------------------------------------------------
-- |
-- Module : Data.Singletons.Base.TypeError
-- Copyright : (C) 2023 Ryan Scott
-- License : BSD-style (see LICENSE)
-- Maintainer : Ryan Scott
-- Stability : experimental
-- Portability : non-portable
--
-- Defines a replacement for the promoted @Error@ function whose argument is
-- kind-polymorphic.
--
----------------------------------------------------------------------------
module Data.Singletons.Base.PolyError (PolyError) where

import Data.Singletons.TH

-- | Like @Error@ from "GHC.TypeLits.Singletons", but with an argument that is
-- generalized to be kind-polymorphic. This allows passing additional
-- information to the error besides raw @Symbol@s.
type PolyError :: a -> b
type family PolyError (arg :: a) :: b where {}
$(genDefunSymbols [''PolyError])
27 changes: 18 additions & 9 deletions singletons-base/src/GHC/TypeLits/Singletons/Internal.hs
Original file line number Diff line number Diff line change
Expand Up @@ -244,22 +244,31 @@ withKnownSymbol SSym f = f
withKnownChar :: Sing n -> (KnownChar n => r) -> r
withKnownChar SChar f = f

-- | The promotion of 'error'. This version is more poly-kinded for
-- easier use.
type Error :: k0 -> a
type family Error (str :: k0) :: a where {}
-- | A promoted version of 'error'. This implements 'Error' as a stuck type
-- family with a 'Symbol' argument. Depending on your needs, you might also
-- consider the following alternatives:
--
-- * "Data.Singletons.Base.PolyError" provides @PolyError@, which generalizes
-- the argument to be kind-polymorphic. This allows passing additional
-- information to the error besides raw 'Symbol's.
--
-- * "Data.Singletons.Base.TypeError" provides @TypeError@, a slightly modified
-- version of the custom type error machinery found in "GHC.TypeLits". This
-- allows emitting error messages as compiler errors rather than as stuck type
-- families.
type Error :: Symbol -> a
type family Error (str :: Symbol) :: a where {}
$(genDefunSymbols [''Error])
instance SingI (ErrorSym0 :: Symbol ~> a) where
sing = singFun1 sError

-- | The singleton for 'error'
-- | The singleton for 'error'.
sError :: HasCallStack => Sing (str :: Symbol) -> a
sError sstr = error (T.unpack (fromSing sstr))

-- | The promotion of 'errorWithoutStackTrace'. This version is more
-- poly-kinded for easier use.
type ErrorWithoutStackTrace :: k0 -> a
type family ErrorWithoutStackTrace (str :: k0) :: a where {}
-- | The promotion of 'errorWithoutStackTrace'.
type ErrorWithoutStackTrace :: Symbol -> a
type family ErrorWithoutStackTrace (str :: Symbol) :: a where {}
$(genDefunSymbols [''ErrorWithoutStackTrace])
instance SingI (ErrorWithoutStackTraceSym0 :: Symbol ~> a) where
sing = singFun1 sErrorWithoutStackTrace
Expand Down
1 change: 1 addition & 0 deletions singletons-base/tests/SingletonsBaseTestSuite.hs
Original file line number Diff line number Diff line change
Expand Up @@ -58,6 +58,7 @@ tests =
compileAndDumpStdTest "Classes2"
, compileAndDumpStdTest "FunDeps"
, compileAndDumpStdTest "T78"
, compileAndDumpStdTest "T89"
, compileAndDumpStdTest "OrdDeriving"
, compileAndDumpStdTest "BoundedDeriving"
, compileAndDumpStdTest "BadBoundedDeriving"
Expand Down
78 changes: 78 additions & 0 deletions singletons-base/tests/compile-and-dump/Singletons/T89.golden
Original file line number Diff line number Diff line change
@@ -0,0 +1,78 @@
Singletons/T89.hs:0:0:: Splicing declarations
singletons
[d| data Foo
= Foo
deriving (Enum) |]
======>
data Foo
= Foo
deriving Enum
type FooSym0 :: Foo
type family FooSym0 :: Foo where
FooSym0 = Foo
type family Case_0123456789876543210 n t where
Case_0123456789876543210 n 'True = FooSym0
Case_0123456789876543210 n 'False = Apply ErrorSym0 (FromString "toEnum: bad argument")
type ToEnum_0123456789876543210 :: GHC.Num.Natural.Natural -> Foo
type family ToEnum_0123456789876543210 (a :: GHC.Num.Natural.Natural) :: Foo where
ToEnum_0123456789876543210 n = Case_0123456789876543210 n (Apply (Apply (==@#@$) n) (FromInteger 0))
type ToEnum_0123456789876543210Sym0 :: (~>) GHC.Num.Natural.Natural Foo
data ToEnum_0123456789876543210Sym0 :: (~>) GHC.Num.Natural.Natural Foo
where
ToEnum_0123456789876543210Sym0KindInference :: SameKind (Apply ToEnum_0123456789876543210Sym0 arg) (ToEnum_0123456789876543210Sym1 arg) =>
ToEnum_0123456789876543210Sym0 a0123456789876543210
type instance Apply ToEnum_0123456789876543210Sym0 a0123456789876543210 = ToEnum_0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings ToEnum_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd (((,) ToEnum_0123456789876543210Sym0KindInference) ())
type ToEnum_0123456789876543210Sym1 :: GHC.Num.Natural.Natural
-> Foo
type family ToEnum_0123456789876543210Sym1 (a0123456789876543210 :: GHC.Num.Natural.Natural) :: Foo where
ToEnum_0123456789876543210Sym1 a0123456789876543210 = ToEnum_0123456789876543210 a0123456789876543210
type FromEnum_0123456789876543210 :: Foo -> GHC.Num.Natural.Natural
type family FromEnum_0123456789876543210 (a :: Foo) :: GHC.Num.Natural.Natural where
FromEnum_0123456789876543210 Foo = FromInteger 0
type FromEnum_0123456789876543210Sym0 :: (~>) Foo GHC.Num.Natural.Natural
data FromEnum_0123456789876543210Sym0 :: (~>) Foo GHC.Num.Natural.Natural
where
FromEnum_0123456789876543210Sym0KindInference :: SameKind (Apply FromEnum_0123456789876543210Sym0 arg) (FromEnum_0123456789876543210Sym1 arg) =>
FromEnum_0123456789876543210Sym0 a0123456789876543210
type instance Apply FromEnum_0123456789876543210Sym0 a0123456789876543210 = FromEnum_0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings FromEnum_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd (((,) FromEnum_0123456789876543210Sym0KindInference) ())
type FromEnum_0123456789876543210Sym1 :: Foo
-> GHC.Num.Natural.Natural
type family FromEnum_0123456789876543210Sym1 (a0123456789876543210 :: Foo) :: GHC.Num.Natural.Natural where
FromEnum_0123456789876543210Sym1 a0123456789876543210 = FromEnum_0123456789876543210 a0123456789876543210
instance PEnum Foo where
type ToEnum a = Apply ToEnum_0123456789876543210Sym0 a
type FromEnum a = Apply FromEnum_0123456789876543210Sym0 a
data SFoo :: Foo -> Type where SFoo :: SFoo (Foo :: Foo)
type instance Sing @Foo = SFoo
instance SingKind Foo where
type Demote Foo = Foo
fromSing SFoo = Foo
toSing Foo = SomeSing SFoo
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)))))
(case
(applySing ((applySing ((singFun2 @(==@#@$)) (%==))) sN))
(sFromInteger (sing :: Sing 0))
of
STrue -> SFoo
SFalse
-> sError (sFromString (sing :: Sing "toEnum: bad argument")))
sFromEnum SFoo = sFromInteger (sing :: Sing 0)
instance SingI Foo where
sing = SFoo
6 changes: 6 additions & 0 deletions singletons-base/tests/compile-and-dump/Singletons/T89.hs
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
{-# LANGUAGE OverloadedStrings #-}
module T89 where

import Data.Singletons.Base.TH

$(singletons [d|data Foo = Foo deriving (Enum)|])

0 comments on commit e89070a

Please sign in to comment.