Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add instances for SNat, SSymbol, and SChar #57

Merged
merged 1 commit into from
Oct 24, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions some.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -72,6 +72,10 @@ library
base >=4.12 && <4.20
, deepseq >=1.4.4.0 && <1.6

if !impl(ghc >= 9.8)
build-depends:
base-orphans >= 0.9.1 && <0.10

if impl(ghc >=9.0)
-- these flags may abort compilation with GHC-8.10
-- https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3295
Expand Down
17 changes: 17 additions & 0 deletions src/Data/EqP.hs
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,12 @@ import System.Mem.StableName (StableName, eqStableName)
#if MIN_VERSION_base(4,18,0)
import Data.Functor.Product (Product (..))
import Data.Functor.Sum (Sum (..))
import qualified GHC.TypeLits as TL
import qualified GHC.TypeNats as TN
#endif

#if !MIN_VERSION_base(4,19,0)
import Data.Orphans ()
#endif

import qualified Type.Reflection as TR
Expand Down Expand Up @@ -88,6 +94,17 @@ instance (EqP a, EqP b) => EqP (a :*: b) where
instance EqP TR.TypeRep where
eqp x y = TR.SomeTypeRep x == TR.SomeTypeRep y

#if MIN_VERSION_base(4,18,0)
instance EqP TL.SChar where
eqp x y = TL.fromSChar x == TL.fromSChar y

instance EqP TL.SSymbol where
eqp x y = TL.fromSSymbol x == TL.fromSSymbol y

instance EqP TN.SNat where
eqp x y = TN.fromSNat x == TN.fromSNat y
#endif

instance EqP Proxy where
eqp _ _ = True

Expand Down
69 changes: 59 additions & 10 deletions src/Data/GADT/Internal.hs
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,11 @@ import qualified Type.Reflection as TR
import Data.Kind (Constraint)
#endif

#if MIN_VERSION_base(4,18,0)
import qualified GHC.TypeLits as TL
import qualified GHC.TypeNats as TN
#endif

-- $setup
-- >>> :set -XKindSignatures -XGADTs -XTypeOperators -XStandaloneDeriving -XQuantifiedConstraints
-- >>> import Data.Type.Equality
Expand Down Expand Up @@ -68,6 +73,17 @@ instance GShow ((:~~:) a) where
instance GShow TR.TypeRep where
gshowsPrec = showsPrec

#if MIN_VERSION_base(4,18,0)
instance GShow TL.SChar where
gshowsPrec = showsPrec

instance GShow TL.SSymbol where
gshowsPrec = showsPrec

instance GShow TN.SNat where
gshowsPrec = showsPrec
#endif

--
-- | >>> gshow (InL Refl :: Sum ((:~:) Int) ((:~:) Bool) Int)
-- "InL Refl"
Expand Down Expand Up @@ -339,6 +355,17 @@ instance (GEq a, GEq b) => GEq (a :*: b) where
instance GEq TR.TypeRep where
geq = testEquality

#if MIN_VERSION_base(4,18,0)
instance GEq TL.SChar where
geq = testEquality

instance GEq TL.SSymbol where
geq = testEquality

instance GEq TN.SNat where
geq = testEquality
#endif

-------------------------------------------------------------------------------
-- GCompare
-------------------------------------------------------------------------------
Expand Down Expand Up @@ -426,20 +453,42 @@ instance GCompare ((:~~:) a) where
gcompare HRefl HRefl = GEQ

instance GCompare TR.TypeRep where
gcompare t1 t2 =
case testEquality t1 t2 of
Just Refl -> GEQ
Nothing ->
case compare (TR.SomeTypeRep t1) (TR.SomeTypeRep t2) of
LT -> GLT
GT -> GGT
EQ -> error "impossible: 'testEquality' and 'compare' \
\are inconsistent for TypeRep; report this \
\as a GHC bug"
gcompare = gcompareSing "TypeRep" TR.SomeTypeRep

#if MIN_VERSION_base(4,18,0)
instance GCompare TL.SChar where
gcompare = gcompareSing "SChar" TL.fromSChar

instance GCompare TL.SSymbol where
gcompare = gcompareSing "SSymbol" TL.fromSSymbol

instance GCompare TN.SNat where
gcompare = gcompareSing "SNat" TN.fromSNat
#endif

defaultCompare :: GCompare f => f a -> f b -> Ordering
defaultCompare x y = weakenOrdering (gcompare x y)

-- | An implementation of 'gcompare' for a singleton type.
gcompareSing :: (TestEquality f, Ord c)
=> String
-- ^ The name of the singleton type.
-- (Only used for error message purposes.)
-> (forall x. f x -> c)
-- ^ How to turn the singleton type into a value that can be
-- compared with 'Ord'.
-> f a -> f b -> GOrdering a b
gcompareSing singName toOrd t1 t2 =
case testEquality t1 t2 of
Just Refl -> GEQ
Nothing ->
case compare (toOrd t1) (toOrd t2) of
LT -> GLT
GT -> GGT
EQ -> error $ "impossible: 'testEquality' and 'compare' are inconsistent for "
++ singName
++ "; report this as a GHC bug"

instance (GCompare a, GCompare b) => GCompare (Sum a b) where
gcompare (InL x) (InL y) = gcompare x y
gcompare (InL _) (InR _) = GLT
Expand Down
17 changes: 17 additions & 0 deletions src/Data/OrdP.hs
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,12 @@ import GHC.Generics ((:*:) (..), (:+:) (..))
#if MIN_VERSION_base(4,18,0)
import Data.Functor.Product (Product (..))
import Data.Functor.Sum (Sum (..))
import qualified GHC.TypeLits as TL
import qualified GHC.TypeNats as TN
#endif

#if !MIN_VERSION_base(4,19,0)
import Data.Orphans ()
#endif

import qualified Type.Reflection as TR
Expand Down Expand Up @@ -75,6 +81,17 @@ instance (OrdP a, OrdP b) => OrdP (a :*: b) where
instance OrdP TR.TypeRep where
comparep x y = compare (TR.SomeTypeRep x) (TR.SomeTypeRep y)

#if MIN_VERSION_base(4,18,0)
instance OrdP TL.SChar where
comparep x y = compare (TL.fromSChar x) (TL.fromSChar y)

instance OrdP TL.SSymbol where
comparep x y = compare (TL.fromSSymbol x) (TL.fromSSymbol y)

instance OrdP TN.SNat where
comparep x y = compare (TN.fromSNat x) (TN.fromSNat y)
#endif

instance OrdP Proxy where
comparep _ _ = EQ

Expand Down