WIP : Opt for Num and Fractional type, and more

.gitignore

@@ -21,3 +21,5 @@ cabal.project.local
 cabal.project.local~
 .HTF/
 .ghc.environment.*
+Makefile
+.vscode

package.yaml

@@ -16,6 +16,7 @@ dependencies:
 - data-default-class >= 0.1.2.0 && < 1
 - singletons >= 3.0.2 && < 3.1
 - singletons-base >= 3.1.1 && < 3.5
+- convertible >= 1.0 && < 1.2
 ghc-options:
 - -Wall
 - -Wcompat

singletons-default.cabal

@@ -1,6 +1,6 @@
 cabal-version: 2.2
 
--- This file has been generated from package.yaml by hpack version 0.36.0.
+-- This file has been generated from package.yaml by hpack version 0.38.1.
 --
 -- see: https://github.com/sol/hpack
 
@@ -37,6 +37,7 @@ library
   ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints
   build-depends:
       base >=4.7 && <5
+    , convertible >=1.0 && <1.2
     , data-default-class >=0.1.2.0 && <1
     , singletons >=3.0.2 && <3.1
     , singletons-base >=3.1.1 && <3.5

src/Data/Default/Singletons.hs

@@ -149,43 +149,44 @@ import GHC.TypeLits
 import Data.Singletons
 import Data.String
 import Prelude.Singletons ()
+import Data.Convertible
 
 {- |
 `Opt`ional type with
 either a `Def`ault promoted value @def@,
 or `Some` specific `Demote`d value.
 -}
-data Opt (def :: k) where
-  Def :: forall {k} def. SingDef def => Opt (def :: k)
-  Some :: forall {k} def. Demote k -> Opt (def :: k)
+data Opt (def :: k) a where
+  Def :: forall {k} def a. SingDef def a => Opt (def :: k) a
+  Some :: forall {k} def a. a -> Opt (def :: k) a
 
 {- | Constraint required to `demote` @@def@. -}
-type SingDef (def :: k) = (SingI def, SingKind k)
+type SingDef (def :: k) a = (SingI def, SingKind k, Convertible (Demote k) a)
 
-instance Semigroup (Opt (def :: k)) where
+instance Semigroup (Opt (def :: k) a) where
   Def <> opt = opt
   Some x <> _ = Some x
 
-instance SingDef def => Monoid (Opt def) where
+instance SingDef def a => Monoid (Opt def a) where
   mempty = Def
 
-deriving instance (SingDef def, Show (Demote k))
-  => Show (Opt (def :: k))
+deriving instance (SingDef def a, Show a)
+  => Show (Opt (def :: k) a)
 
-deriving instance (SingDef def, Read (Demote k))
-  => Read (Opt (def :: k))
+deriving instance (SingDef def a, Read a)
+  => Read (Opt (def :: k) a)
 
-deriving instance (SingDef def, Eq (Demote k))
-  => Eq (Opt (def :: k))
+deriving instance (SingDef def a, Eq a)
+  => Eq (Opt (def :: k) a)
 
-deriving instance (SingDef def, Ord (Demote k))
-  => Ord (Opt (def :: k))
+deriving instance (SingDef def a, Ord a)
+  => Ord (Opt (def :: k) a)
 
-instance SingDef def
-  => Default (Opt (def :: k)) where def = Def
+instance SingDef def a
+  => Default (Opt (def :: k) a) where def = Def
 
-instance Num (Demote k)
-  => Num (Opt (def :: k)) where
+instance Num a
+  => Num (Opt (def :: k) a) where
     x + y = Some $ definite x + definite y
     x * y = Some $ definite x * definite y
     abs x = Some $ abs (definite x)
@@ -194,19 +195,19 @@ instance Num (Demote k)
     negate x = Some $ negate (definite x)
     x - y = Some $ definite x - definite y
 
-instance Fractional (Demote k)
-  => Fractional (Opt (def :: k)) where
+instance Fractional a
+  => Fractional (Opt (def :: k) a) where
     recip x = Some $ recip (definite x)
     x / y = Some $ definite x / definite y
     fromRational x = Some $ fromRational x
 
-instance IsString (Demote k)
-  => IsString (Opt (def :: k)) where
+instance IsString a
+  => IsString (Opt (def :: k) a) where
     fromString x = Some $ fromString x
 
-instance IsList (Demote k)
-  => IsList (Opt (def :: k)) where
-    type Item (Opt (def :: k)) = Item (Demote k)
+instance IsList a
+  => IsList (Opt (def :: k) a) where
+    type Item (Opt (def :: k) a) = Item a
     fromList xs = Some $ fromList xs
     fromListN n xs = Some $ fromListN n xs
     toList x = toList $ definite x
@@ -222,19 +223,19 @@ and `Just` maps to `Some`.
 "bar"
 -}
 optionally
-  :: forall {k} def. SingDef def
-  => Maybe (Demote k)
-  -> Opt (def :: k)
+  :: forall {k} def a. SingDef def a
+  => Maybe a
+  -> Opt (def :: k) a
 optionally = maybe Def Some
 
 {- |
 Deconstructs an `Opt` to a `Demote`d value.
 `Def` maps to `demote` @@def@,
 and `Some` maps to its argument.
 -}
-definite :: forall {k} def. Opt (def :: k) -> Demote k
+definite :: forall {k} def a. Opt (def :: k) a -> a
 definite = \case
-  Def -> demote @def
+  Def -> convert $ demote @def
   Some a -> a
 
 {- |
@@ -244,8 +245,8 @@ and `Some` maps to `pure`,
 inverting `optionally`.
 -}
 perhaps
-  :: forall {k} def m. Alternative m
-  => Opt (def :: k) -> m (Demote k)
+  :: forall {k} def a m. Alternative m
+  => Opt (def :: k) a -> m a
 perhaps = \case
   Def -> empty
   Some a -> pure a
@@ -435,4 +436,4 @@ instance SingKind Q where
   toSing q = withSomeSing q SomeSing
 
 instance (SingI num, SingI denom) => SingI (num :% denom) where
-  sing = SRational sing sing
+  sing = SRational sing sing