✨ Add deriving for void types for builtin type classes

CHANGELOG.md

@@ -19,6 +19,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Added `mrgIfPropagatedStrategy`. ([#184](https://github.com/lsrcz/grisette/pull/184))
 - Added `freshString`. ([#188](https://github.com/lsrcz/grisette/pull/188))
 - Added `localFreshIdent`. ([#190](https://github.com/lsrcz/grisette/pull/190))
+- Added deriving for void types for builtin type classes. ([#191](https://github.com/lsrcz/grisette/pull/191))
 
 ### Fixed
 

src/Grisette/Core/Data/Class/EvaluateSym.hs

@@ -46,6 +46,7 @@ import Generics.Deriving
     K1 (K1),
     M1 (M1),
     U1,
+    V1,
     type (:*:) ((:*:)),
     type (:+:) (L1, R1),
   )
@@ -254,23 +255,34 @@ deriving via (Default AssertionError) instance EvaluateSym AssertionError
 deriving via (Default VerificationConditions) instance EvaluateSym VerificationConditions
 
 instance (Generic a, EvaluateSym' (Rep a)) => EvaluateSym (Default a) where
-  evaluateSym fillDefault model = Default . to . evaluateSym' fillDefault model . from . unDefault
+  evaluateSym fillDefault model =
+    Default . to . evaluateSym' fillDefault model . from . unDefault
 
 class EvaluateSym' a where
   evaluateSym' :: Bool -> Model -> a c -> a c
 
 instance EvaluateSym' U1 where
   evaluateSym' _ _ = id
+  {-# INLINE evaluateSym' #-}
+
+instance EvaluateSym' V1 where
+  evaluateSym' _ _ = id
+  {-# INLINE evaluateSym' #-}
 
 instance (EvaluateSym c) => EvaluateSym' (K1 i c) where
   evaluateSym' fillDefault model (K1 v) = K1 $ evaluateSym fillDefault model v
+  {-# INLINE evaluateSym' #-}
 
 instance (EvaluateSym' a) => EvaluateSym' (M1 i c a) where
   evaluateSym' fillDefault model (M1 v) = M1 $ evaluateSym' fillDefault model v
+  {-# INLINE evaluateSym' #-}
 
 instance (EvaluateSym' a, EvaluateSym' b) => EvaluateSym' (a :+: b) where
   evaluateSym' fillDefault model (L1 l) = L1 $ evaluateSym' fillDefault model l
   evaluateSym' fillDefault model (R1 r) = R1 $ evaluateSym' fillDefault model r
+  {-# INLINE evaluateSym' #-}
 
 instance (EvaluateSym' a, EvaluateSym' b) => EvaluateSym' (a :*: b) where
-  evaluateSym' fillDefault model (a :*: b) = evaluateSym' fillDefault model a :*: evaluateSym' fillDefault model b
+  evaluateSym' fillDefault model (a :*: b) =
+    evaluateSym' fillDefault model a :*: evaluateSym' fillDefault model b
+  {-# INLINE evaluateSym' #-}

src/Grisette/Core/Data/Class/ExtractSymbolics.hs

@@ -44,6 +44,7 @@ import Generics.Deriving
     K1 (unK1),
     M1 (unM1),
     U1,
+    V1,
     type (:*:) ((:*:)),
     type (:+:) (L1, R1),
   )
@@ -293,6 +294,9 @@ class ExtractSymbolics' a where
 instance ExtractSymbolics' U1 where
   extractSymbolics' _ = mempty
 
+instance ExtractSymbolics' V1 where
+  extractSymbolics' _ = mempty
+
 instance (ExtractSymbolics c) => ExtractSymbolics' (K1 i c) where
   extractSymbolics' = extractSymbolics . unK1
 

src/Grisette/Core/Data/Class/SubstituteSym.hs

@@ -45,6 +45,7 @@ import Generics.Deriving
     K1 (K1),
     M1 (M1),
     U1,
+    V1,
     type (:*:) ((:*:)),
     type (:+:) (L1, R1),
   )
@@ -294,6 +295,9 @@ instance
 instance SubstituteSym' U1 where
   substituteSym' _ _ = id
 
+instance SubstituteSym' V1 where
+  substituteSym' _ _ = id
+
 instance (SubstituteSym c) => SubstituteSym' (K1 i c) where
   substituteSym' sym val (K1 v) = K1 $ substituteSym sym val v
 

src/Grisette/Core/Data/Class/ToCon.hs

@@ -40,14 +40,7 @@ import Data.Functor.Sum (Sum)
 import Data.Int (Int16, Int32, Int64, Int8)
 import qualified Data.Text as T
 import Data.Word (Word16, Word32, Word64, Word8)
-import GHC.Generics
-  ( Generic (Rep, from, to),
-    K1 (K1),
-    M1 (M1),
-    U1,
-    type (:*:) ((:*:)),
-    type (:+:) (L1, R1),
-  )
+import GHC.Generics (Generic (Rep, from, to), K1 (K1), M1 (M1), U1, V1, type (:*:) ((:*:)), type (:+:) (L1, R1))
 import GHC.TypeNats (KnownNat, type (<=))
 import Generics.Deriving (Default (Default))
 import Generics.Deriving.Instances ()
@@ -312,6 +305,9 @@ class ToCon' a b where
 instance ToCon' U1 U1 where
   toCon' = Just
 
+instance ToCon' V1 V1 where
+  toCon' = Just
+
 instance (ToCon a b) => ToCon' (K1 i a) (K1 i b) where
   toCon' (K1 a) = K1 <$> toCon a
 

src/Grisette/Core/Data/Class/ToSym.hs

@@ -48,6 +48,7 @@ import Generics.Deriving
     K1 (K1),
     M1 (M1),
     U1,
+    V1,
     type (:*:) ((:*:)),
     type (:+:) (L1, R1),
   )
@@ -297,6 +298,9 @@ class ToSym' a b where
 instance ToSym' U1 U1 where
   toSym' = id
 
+instance ToSym' V1 V1 where
+  toSym' = id
+
 instance (ToSym a b) => ToSym' (K1 i a) (K1 i b) where
   toSym' (K1 a) = K1 $ toSym a