🐛 Fix build on older compilers

src/Grisette/Unified/Internal/EvalMode.hs

@@ -58,14 +58,14 @@ import Grisette.Unified.Internal.UnifiedFun
 import Grisette.Unified.Internal.UnifiedInteger (UnifiedInteger)
 import Language.Haskell.TH
   ( DecsQ,
-    Quote (newName),
     Type (AppT, ArrowT, ConT, StarT, VarT),
     appT,
     classD,
     conT,
     instanceD,
     kindedTV,
     mkName,
+    newName,
     promotedT,
     tySynD,
     varT,
@@ -227,14 +227,33 @@ type MonadEvalModeAll mode m =
 -- The function will also provide the constraint @MonadMyEvalModeUF@, which
 -- includes the constraints for the monad and the unified branching, similar to
 -- 'MonadEvalModeAll'.
+--
+-- For compilers older than GHC 9.2.1, see the notes for 'EvalModeAll'. This
+-- function will also generate constraints like @MyEvalModeUFFunUWordNUIntN@,
+-- which can be used to resolve the constraints for older compilers.
+--
+-- The naming conversion is the concatenation of the three parts:
+--
+-- * The base name provided by the user (i.e., @MyEvalModeUF@),
+-- * @Fun@,
+-- * The concatenation of all the types in the uninterpreted function (i.e.,
+--   @UWordNUIntN@).
+--
+-- The arguments to the type class is as follows:
+--
+-- * The first argument is the mode,
+-- * The second to the end arguments are the natural number arguments for all
+--   the types. Here the second argument is the bitwidth of the unsigned
+--   bit-vector argument, and the third argument is the bitwidth of the signed
+--   bit-vector result.
 genEvalMode :: String -> [TheoryToUnify] -> DecsQ
 genEvalMode nm theories = do
   modeName <- newName "mode"
   let modeType = VarT modeName
   baseConstraint <- [t|EvalModeBase $(return modeType)|]
   basicConstraints <- concat <$> traverse (nonFuncConstraint modeType) nonFuncs
   funcInstances <- concat <$> traverse (genUnifiedFunInstance nm) funcs
-  let instanceNames = unifiedFunInstanceName nm <$> funcs
+  let instanceNames = ("All" ++) . unifiedFunInstanceName nm <$> funcs
   funcConstraints <- traverse (genFunConstraint (return modeType)) instanceNames
   r <-
     classD

src/Grisette/Unified/Internal/UnifiedFun.hs

@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE FlexibleContexts #-}
@@ -83,15 +84,23 @@ import Language.Haskell.TH
     promotedT,
     varT,
   )
+import qualified Language.Haskell.TH
 import Language.Haskell.TH.Datatype.TyVarBndr
-  ( TyVarBndrVis,
-    kindedTV,
+  ( kindedTV,
     mapTVFlag,
     specifiedSpec,
     tvName,
   )
 import Language.Haskell.TH.Syntax (Lift)
 
+#if MIN_VERSION_template_haskell(2,21,0)
+type TyVarBndrVis = Language.Haskell.TH.TyVarBndrVis
+#elif MIN_VERSION_template_haskell(2,17,0)
+type TyVarBndrVis = Language.Haskell.TH.TyVarBndr ()
+#else
+type TyVarBndrVis = Language.Haskell.TH.TyVarBndr
+#endif
+
 -- | Provide unified function types.
 class UnifiedFun (mode :: EvalModeTag) where
   -- | Get a unified function type. Resolves to t'Grisette.SymPrim.=->' in 'Con'
@@ -257,7 +266,7 @@ genOuterUnifiedFunInstance nm innerName mode preds bndrs = do
 -- | Generate unified function instance names.
 unifiedFunInstanceName :: String -> [TheoryToUnify] -> String
 unifiedFunInstanceName prefix theories =
-  prefix ++ "UnifiedFunInstance" ++ (concatMap show theories)
+  prefix ++ "Fun" ++ (concatMap show theories)
 
 -- | Generate unified function instances.
 genUnifiedFunInstance :: String -> [TheoryToUnify] -> DecsQ
@@ -266,23 +275,20 @@ genUnifiedFunInstance prefix theories = do
   let modeType = VarT modeName
   allArgs <- traverse (genArgs modeType) theories
   let baseName = unifiedFunInstanceName prefix theories
-  let noBndr = all (\(bndr, _, _, _, _) -> null bndr) allArgs
-  let innerName = if noBndr then baseName else baseName ++ "Inner"
-
   rinner <-
     genInnerUnifiedFunInstance
-      innerName
+      baseName
       (kindedTV modeName (ConT ''EvalModeTag))
       (concatMap (\(_, p, _, _, _) -> p) allArgs)
       (concatMap (\(t, _, _, _, _) -> t) allArgs)
       ((\(_, _, u, c, s) -> (u, c, s)) <$> allArgs)
   router <-
-    if noBndr
+    if all (\(bndr, _, _, _, _) -> null bndr) allArgs
       then return []
       else
         genOuterUnifiedFunInstance
+          ("All" ++ baseName)
           baseName
-          innerName
           (kindedTV modeName (ConT ''EvalModeTag))
           (concatMap (\(_, p, _, _, _) -> p) allArgs)
           (concatMap (\(t, _, _, _, _) -> t) allArgs)

test/Grisette/Unified/EvalModeTest.hs

@@ -23,9 +23,7 @@
 
 module Grisette.Unified.EvalModeTest (evalModeTest) where
 
-#if MIN_VERSION_base(4,16,0)
-import GHC.TypeLits (KnownNat, type (<=))
-#else
+#if !MIN_VERSION_base(4,16,0)
 import Grisette.Unified
   ( SafeUnifiedBV,
     SafeUnifiedBVFPConversion,
@@ -43,6 +41,7 @@ import Control.Monad.Error.Class (MonadError)
 import Control.Monad.Except (ExceptT (ExceptT))
 import Control.Monad.Identity (Identity (Identity))
 import GHC.Generics (Generic)
+import GHC.TypeLits (KnownNat, type (<=))
 import Grisette
   ( BV (bv),
     BitCast (bitCast),
@@ -384,17 +383,36 @@ bvToBVFromIntegral = symFromIntegral @mode
 
 genEvalMode "EvalMode" [UFun [UIntN, UWordN]]
 
+#if MIN_VERSION_base(4,16,0)
+type EvalModeUFunConstraint mode n m =
+  ( EvalMode mode,
+    KnownNat n,
+    1 <= n,
+    KnownNat m,
+    1 <= m
+  )
+#else
+type EvalModeUFunConstraint mode n m =
+  ( EvalMode mode,
+    KnownNat n,
+    1 <= n,
+    KnownNat m,
+    1 <= m,
+    EvalModeFunUIntNUWordN mode n m
+  )
+#endif
+
 ufuncTest0 ::
   forall mode n m.
-  (EvalMode mode, KnownNat n, 1 <= n, KnownNat m, 1 <= m) =>
+  (EvalModeUFunConstraint mode n m) =>
   GetFun mode (GetIntN mode n) (GetWordN mode m) ->
   GetIntN mode n ->
   GetWordN mode m
 ufuncTest0 f = (f #)
 
 ufunc0 ::
   forall mode n m.
-  (EvalMode mode, KnownNat n, 1 <= n, KnownNat m, 1 <= m) =>
+  (EvalModeUFunConstraint mode n m) =>
   GetFun mode (GetIntN mode n) (GetWordN mode m)
 ufunc0 = toSym (TabularFun [(1, 0)] 2 :: IntN n =-> WordN m)