[feat] some more things for existential SBools

dependent-if.cabal

@@ -1,47 +1,54 @@
-cabal-version:      3.4
-name:               dependent-if
-version:            0.1.0.0
+cabal-version:   3.4
+name:            dependent-if
+version:         0.1.0.0
+
 -- synopsis:
 -- description:
-homepage:           https://sr.ht/~mangoiv/dependent-if
-license:            MIT
-license-file:       LICENSE
-author:             mangoiv
-maintainer:         contact@mangoiv.com
+homepage:        https://sr.ht/~mangoiv/dependent-if
+license:         MIT
+license-file:    LICENSE
+author:          mangoiv
+maintainer:      contact@mangoiv.com
+
 -- copyright:
-category:           Data
-build-type:         Simple
-extra-doc-files:    CHANGELOG.md
+category:        Data
+build-type:      Simple
+extra-doc-files: CHANGELOG.md
+
 -- extra-source-files:
 
 common warnings
-    ghc-options: -Wall
+  ghc-options: -Wall
 
-common extensions 
-    default-extensions: 
-      DataKinds
-      DerivingStrategies
-      GADTs
-      TypeFamilies 
+common extensions
+  default-extensions:
+    BlockArguments
+    DataKinds
+    DerivingStrategies
+    GADTs
+    LambdaCase
+    TypeFamilies
 
 library
-    import:           
-      , warnings
-      , extensions
-    exposed-modules:  Data.Bool.IfThenElse
-    build-depends:    base ^>=4.16.3.0
-    hs-source-dirs:   src
-    default-language: GHC2021
+  import:
+    , warnings
+    , extensions
+
+  exposed-modules:  Data.Bool.IfThenElse
+  build-depends:    base ^>=4.16.3.0
+  hs-source-dirs:   src
+  default-language: GHC2021
 
 test-suite dependent-if-test
-    import:           
-      , warnings
-      , extensions
-    default-language: GHC2021
-    type:             exitcode-stdio-1.0
-    hs-source-dirs:   test
-    main-is:          Main.hs
-    build-depends:
-      , base ^>=4.16.3.0
-      , dependent-if
-      , HUnit
+  import:
+    , warnings
+    , extensions
+
+  default-language: GHC2021
+  type:             exitcode-stdio-1.0
+  hs-source-dirs:   test
+  main-is:          Main.hs
+  build-depends:
+    , base          ^>=4.16.3.0
+    , dependent-if
+    , HUnit

fourmolu.yaml

@@ -0,0 +1,11 @@
+indentation: 2
+function-arrows: leading
+comma-style: leading
+import-export-style: leading
+indent-wheres: false
+record-brace-space: true
+newlines-between-decls: 1
+haddock-style: single-line
+let-style: inline
+in-style: right-align
+respectful: false

src/Data/Bool/IfThenElse.hs

@@ -1,20 +1,27 @@
-{-# LANGUAGE TypeFamilyDependencies #-}
 -- | Dependent If in Haskell, use this with `-XRebindableSyntax`
-module Data.Bool.IfThenElse (
-    SBool (..),
-    SomeBool (..),
-    ifThenElse,
-    IfThenElse,
-    IfThenElse',
-) where
+module Data.Bool.IfThenElse
+  ( -- * SBool
+    SBool (..)
+  , SomeBool (..)
+  , withSomeBool
 
-import Data.Kind (Type, Constraint)
+    -- * IfThenElse
+  , IfThenElse
+  , IfThenElse'
+  , ifThenElse
+
+    -- * helpers
+  , SomeIfThenElse (..)
+  )
+where
+
+import Data.Kind (Constraint, Type)
 
 -- | Singleton for Bool
 type SBool :: Bool -> Type
 data SBool b where
-    STrue :: SBool 'True
-    SFalse :: SBool 'False
+  STrue :: SBool 'True
+  SFalse :: SBool 'False
 
 deriving stock instance (Show (SBool b))
 
@@ -22,13 +29,17 @@ deriving stock instance (Show (SBool b))
 type SomeBool :: Type
 data SomeBool = forall b. SomeBool (SBool b)
 
+withSomeBool :: SomeBool -> (forall b. SBool b -> r) -> r
+withSomeBool (SomeBool b) f = f b
+
 deriving stock instance (Show SomeBool)
 
--- | ifThenElse as type family, total
+-- | IfThenElse but as a class
 type IsIfThenElse :: Type -> Type -> Type -> Constraint
-class IsIfThenElse b x y where 
+class IsIfThenElse b x y where
   type IfThenElse b x y :: Type
-  -- | dependent if to be used with `-XRebindableSyntax`, also works 
+
+  -- | dependent if to be used with `-XRebindableSyntax`, also works
   --   for non-singled Bools
   --
   -- /Examples/
@@ -43,12 +54,22 @@ instance (x ~ y) => IsIfThenElse Bool x y where
   ifThenElse True x _ = x
   ifThenElse False _ y = y
 
-type IfThenElse' :: Bool -> Type -> Type -> Type
-type family IfThenElse' b x y where
-    IfThenElse' 'True x _ = x
-    IfThenElse' 'False _ y = y
+-- | We need this because specifying a polymorphic type as a result for a type family is
+--   not allowed
+data SomeIfThenElse x y = forall b. SomeIfThenElse (SBool b) (IfThenElse' b x y)
+
+instance IsIfThenElse SomeBool x y where
+  type IfThenElse SomeBool x y = SomeIfThenElse x y
+  ifThenElse b x y = withSomeBool b \b' ->
+    SomeIfThenElse b' $ ifThenElse b' x y
 
 instance IsIfThenElse (SBool b) x y where
   type IfThenElse (SBool b) x y = IfThenElse' b x y
   ifThenElse STrue x _ = x
   ifThenElse SFalse _ y = y
+
+-- | ifThenElse as type family, total
+type IfThenElse' :: Bool -> Type -> Type -> Type
+type family IfThenElse' b x y where
+  IfThenElse' 'True x _ = x
+  IfThenElse' 'False _ y = y

test/Main.hs

@@ -3,9 +3,16 @@
 module Main (main) where
 
 import Control.Monad ((<=<))
-import Data.Bool.IfThenElse (SBool (SFalse, STrue), ifThenElse, IfThenElse')
+import Data.Bool.IfThenElse
+  ( IfThenElse'
+  , SBool (SFalse, STrue)
+  , SomeBool (SomeBool)
+  , SomeIfThenElse (SomeIfThenElse)
+  , ifThenElse
+  )
+import Data.Function ((&))
 import Test.HUnit (Test (TestList), runTestTT, (~:), (~=?))
-import Prelude (IO, Integer, String, fromInteger, print, ($), Bool (True, False))
+import Prelude (Bool (False, True), Either (Left, Right), IO, Integer, String, fromInteger, print, ($))
 
 example :: SBool b -> IfThenElse' b Integer String
 example b = if b then (1 :: Integer) else "False"
@@ -13,12 +20,20 @@ example b = if b then (1 :: Integer) else "False"
 example2 :: Bool -> Integer
 example2 b = if b then 1 else 5
 
+example3 :: SomeBool -> Either Integer String
+example3 b =
+  (if b then 42 :: Integer else "bar" :: String) & \case
+    SomeIfThenElse STrue ite -> Left ite
+    SomeIfThenElse SFalse ite -> Right ite
+
 main :: IO ()
 main =
-    print <=< runTestTT $
-        TestList
-            [ "test true" ~: 1 ~=? example STrue
-            , "test false" ~: "False" ~=? example SFalse
-            , "test true" ~: 1 ~=? example2 True
-            , "test false" ~: 5 ~=? example2 False
-            ]
+  print <=< runTestTT $
+    TestList
+      [ "test SBool true" ~: 1 ~=? example STrue
+      , "test SBool false" ~: "False" ~=? example SFalse
+      , "test Bool true" ~: 1 ~=? example2 True
+      , "test Bool false" ~: 5 ~=? example2 False
+      , "test SomeBool true" ~: Left 42 ~=? example3 (SomeBool STrue)
+      , "test SomeBool false" ~: Right "foo" ~=? example3 (SomeBool SFalse)
+      ]