Squash warnings; improve HashMap construction

* Get rid of a bunch of redundant constraint warnings, record field
  ambiguity warnings, etc.

* Use `Data.HashMap.fromListWith` instead of building from a list with
  `insertWith`. The built-in version does basically the same thing, but
  with a bunch of unsafe array freeze/thaw operations to reduce
  allocation and copying.

Author: treeowl

kore/kore.cabal

@@ -156,9 +156,9 @@ common library
   build-depends: gitrev >=1.3
   build-depends: graphviz >=2999.20
   -- Pin hashable to make sure cabal build uses the one Nix & Stack builds do
-  build-depends: hashable ==1.3.0.0
+  build-depends: hashable ==1.4.2.0
   build-depends: haskeline ==0.8.*
-  build-depends: integer-gmp >=1.0
+  build-depends: ghc-bignum >=1.2
   build-depends: json-rpc >=1.0
   build-depends: lens >=4.17
   build-depends: lifted-async
@@ -196,7 +196,7 @@ common library
   build-depends: unliftio >= 0.2
   build-depends: unordered-containers >=0.2
   build-depends: vector >=0.12
-  build-depends: witherable ==0.3.*
+  build-depends: witherable ==0.4.*
   build-depends: yaml >=0.11.5.0
   build-depends: zlib >=0.6
   build-tool-depends: happy:happy

kore/src/Kore/Attribute/PredicatePattern.hs

@@ -69,8 +69,7 @@ instance Debug variable => Debug (PredicatePattern variable) where
 instance (Debug variable, Diff variable) => Diff (PredicatePattern variable)
 
 instance
-    ( Functor base
-    , Synthetic (FreeVariables variable) base
+    ( Synthetic (FreeVariables variable) base
     , Synthetic Simplified base
     ) =>
     Synthetic (PredicatePattern variable) base

kore/src/Kore/Builtin/AssociativeCommutative.hs

@@ -805,8 +805,8 @@ matchUnifyEqualsNormalizedAc
         matchUnifyOpaqueVariable' =
             matchUnifyOpaqueVariable tools
 
-        listToMap :: Hashable a => Ord a => [a] -> HashMap a Int
-        listToMap = List.foldl' (\m k -> HashMap.insertWith (+) k 1 m) HashMap.empty
+        listToMap :: Hashable a => [a] -> HashMap a Int
+        listToMap keys = HashMap.fromListWith (+) [(k, 1) | k <- keys]
         mapToList :: HashMap a Int -> [a]
         mapToList =
             HashMap.foldrWithKey
@@ -872,7 +872,6 @@ matchUnifyEqualsNormalizedAc
 
         withoutKeys ::
             Hashable k =>
-            Eq k =>
             HashMap k v ->
             HashSet k ->
             HashMap k v
@@ -969,8 +968,8 @@ unifyEqualsNormalizedAc
                     , commonVariablesCondition
                     ]
       where
-        listToMap :: Hashable a => Ord a => [a] -> HashMap a Int
-        listToMap = List.foldl' (\m k -> HashMap.insertWith (+) k 1 m) HashMap.empty
+        listToMap :: Hashable a => [a] -> HashMap a Int
+        listToMap keys = HashMap.fromListWith (+) [(k, 1) | k <- keys]
         mapToList :: HashMap a Int -> [a]
         mapToList =
             HashMap.foldrWithKey

kore/src/Kore/Builtin/Int.hs

@@ -1,4 +1,5 @@
 {-# LANGUAGE MagicHash #-}
+{-# LANGUAGE UnboxedSums #-}
 
 {- |
 Module      : Kore.Builtin.Int
@@ -89,9 +90,11 @@ import Data.Text (
 import GHC.Integer (
     smallInteger,
  )
-import GHC.Integer.GMP.Internals (
-    powModInteger,
-    recipModInteger,
+import GHC.Num.Integer (
+    integerFromNatural,
+    integerPowMod#,
+    integerRecipMod#,
+    integerToNatural,
  )
 import GHC.Integer.Logarithms (
     integerLog2#,
@@ -364,6 +367,18 @@ powmod b e m
     | m == 0 = Nothing
     | e < 0 && recipModInteger b m == 0 = Nothing
     | otherwise = Just (powModInteger b e m)
+  where
+    -- These functions are deprecated in integer-gmp. I'm not sure how to
+    -- adapt best to the new ghc-bignum regime.
+    recipModInteger :: Integer -> Integer -> Integer
+    recipModInteger x m' = case integerRecipMod# x (integerToNatural m') of
+       (# y |    #) -> integerFromNatural y
+       (#   | () #) -> 0
+
+    powModInteger :: Integer -> Integer -> Integer -> Integer
+    powModInteger b' e' m' = case integerPowMod# b' e' (integerToNatural m') of
+       (# r  | #) -> integerFromNatural r
+       (# | () #) -> 0
 
 evalEq :: Builtin.Function
 evalEq sideCondition resultSort arguments@[_intLeft, _intRight] =

kore/src/Kore/Internal/Key.hs

@@ -2,6 +2,8 @@
 Copyright   : (c) Runtime Verification, 2018-2021
 License     : BSD-3-Clause
 -}
+-- The Synthetic KeyAttributes base instance needs this.
+{-# OPTIONS_GHC -Wno-redundant-constraints #-}
 module Kore.Internal.Key (
     Key (..),
     KeyF (..),
@@ -63,6 +65,8 @@ newtype KeyAttributes = KeyAttributes
     deriving anyclass (SOP.Generic, SOP.HasDatatypeInfo)
     deriving anyclass (Debug, Diff)
 
+-- GHC claims the Functor constraint is redundant, but it gives an error
+-- without it. See https://gitlab.haskell.org/ghc/ghc/-/issues/22838
 instance (Synthetic Sort base, Functor base) => Synthetic KeyAttributes base where
     synthetic base =
         KeyAttributes

kore/src/Kore/Internal/SideCondition.hs

@@ -443,7 +443,6 @@ mapVariables adj condition@(SideCondition _ _ _ _ _) =
 
 -- | Utility function for mapping on the keys and values of a 'HashMap'.
 mapKeysAndValues ::
-    Eq b =>
     Hashable b =>
     (a -> b) ->
     HashMap a a ->

kore/src/Kore/Internal/TermLike/TermLike.hs

@@ -1,4 +1,3 @@
-{-# LANGUAGE CPP #-}
 {-# LANGUAGE UndecidableInstances #-}
 
 {- |
@@ -55,7 +54,6 @@ import Data.Functor.Identity (
 import Data.Generics.Product
 import Data.Generics.Product qualified as Lens.Product
 import Data.HashMap.Strict qualified as HashMap
-import Data.Kind (Constraint)
 import Data.Map.Strict (
     Map,
  )
@@ -694,13 +692,7 @@ instance Ord variable => Ord (TermLike variable) where
         (Recursive.project -> _ :< pat2) =
             compare pat1 pat2
 
-#if MIN_VERSION_hashable(1,4,0)
-type HashableConstraint variable = Eq variable
-#else
-type HashableConstraint variable = () :: Constraint
-#endif
-
-instance HashableConstraint variable => Hashable (TermLike variable) where
+instance Eq variable => Hashable (TermLike variable) where
     hashWithSalt salt (TermLike__ _ hsh _) =
         salt `hashWithSalt` hsh -- HACK
     {-# INLINE hashWithSalt #-}

kore/src/Kore/Log/ErrorOutOfDate.hs

@@ -15,7 +15,7 @@ import Control.Monad.Catch (
     MonadThrow,
     throwM,
  )
-import Log
+import Log hiding (message)
 import Prelude.Kore
 import Pretty
 

kore/src/Kore/Log/ErrorParse.hs

@@ -15,7 +15,7 @@ import Control.Monad.Catch (
     MonadThrow,
     throwM,
  )
-import Log
+import Log hiding (message)
 import Prelude.Kore
 import Pretty
 

kore/src/Kore/Log/WarnNotAPredicate.hs

@@ -16,7 +16,7 @@ import Kore.Internal.Conditional qualified as Conditional
 import Kore.Internal.Pattern (Pattern)
 import Kore.Internal.Predicate (Predicate)
 import Kore.Rewrite.RewritingVariable
-import Log
+import Log hiding (severity)
 import Prelude.Kore
 import Pretty (Pretty)
 import Pretty qualified

kore/src/Kore/Simplify/Simplify.hs

@@ -311,7 +311,7 @@ instance MonadSimplify Simplifier where
     {-# INLINE askMemo #-}
 
 instance
-    (WithLog LogMessage m, MonadSimplify m, Monoid w) =>
+    (MonadSimplify m, Monoid w) =>
     MonadSimplify (AccumT w m)
     where
     localAxiomEquations locally =

kore/src/Log.hs

@@ -264,7 +264,7 @@ runLoggerT LoggerT{getLoggerT} logAction =
     runReaderT getLoggerT LoggerEnv{logAction}
 {-# INLINE runLoggerT #-}
 
-instance (MonadCatch m, MonadThrow m) => MonadLog (LoggerT m) where
+instance MonadCatch m => MonadLog (LoggerT m) where
     logEntry entry = do
         someLogAction <- askLogAction
         lift $ someLogAction <& toEntry entry

kore/test/Test/Kore/Builtin/Map.hs

@@ -1582,7 +1582,6 @@ distinctVariables variables =
 -- | Utility function for mapping over the keys of a 'HashMap'.
 mapKeys ::
     Hashable k2 =>
-    Eq k2 =>
     (k1 -> k2) ->
     HashMap k1 v ->
     HashMap k2 v

kore/test/Test/Kore/Builtin/Set.hs

@@ -1917,7 +1917,7 @@ normalizedSet elements opaque =
 mkIntVar :: Id -> TermLike VariableName
 mkIntVar variableName = mkElemVar $ mkElementVariable variableName intSort
 
-setIntersectionsAreEmpty :: Hashable a => Eq a => [HashSet a] -> Bool
+setIntersectionsAreEmpty :: Hashable a => [HashSet a] -> Bool
 setIntersectionsAreEmpty [] = True
 setIntersectionsAreEmpty (set : sets) =
     setIntersectionsAreEmpty sets

kore/test/Test/Kore/Equation/Common.hs

@@ -20,7 +20,7 @@ import Data.Sup (
     Sup (..),
  )
 import GHC.Natural (
-    intToNatural,
+    wordToNatural,
  )
 import Kore.Attribute.Axiom (Simplification (..))
 import Kore.Attribute.Axiom.Concrete (
@@ -84,7 +84,7 @@ functionAxiomUnification symbol args right requires =
   where
     ~left = mkApplySymbol symbol variables
     sorts = fmap termLikeSort args
-    ~variables = generateVariables (intToNatural (length args)) sorts
+    ~variables = generateVariables (wordToNatural (fromIntegral (length args))) sorts
     generateVariables ~n sorts' =
         -- lazy argument to prevent arithmetic underflow
         fmap makeElementVariable (zip [0 .. n - 1] sorts')

kore/test/Test/Kore/Rewrite/MockSymbols.hs

@@ -46,6 +46,7 @@ import Kore.Attribute.Pattern.ConstructorLike (
     isConstructorLike,
  )
 import Kore.Attribute.Sort qualified as Attribute
+import Kore.Attribute.Sort qualified as AttributeSort
 import Kore.Attribute.Sort.Concat qualified as Attribute
 import Kore.Attribute.Sort.Constructors qualified as Attribute (
     Constructors,
@@ -1793,7 +1794,7 @@ sortAttributesMapping =
     ,
         ( mapSort
         , Default.def
-            { Attribute.hook = Hook (Just "MAP.Map")
+            { AttributeSort.hook = Hook (Just "MAP.Map")
             , Attribute.unit =
                 Attribute.Unit (Just $ toSymbolOrAlias unitMapSymbol)
             , Attribute.element =
@@ -1805,7 +1806,7 @@ sortAttributesMapping =
     ,
         ( listSort
         , Default.def
-            { Attribute.hook = Hook (Just "LIST.List")
+            { AttributeSort.hook = Hook (Just "LIST.List")
             , Attribute.unit =
                 Attribute.Unit (Just $ toSymbolOrAlias unitListSymbol)
             , Attribute.element =
@@ -1817,7 +1818,7 @@ sortAttributesMapping =
     ,
         ( setSort
         , Default.def
-            { Attribute.hook = Hook (Just "SET.Set")
+            { AttributeSort.hook = Hook (Just "SET.Set")
             , Attribute.unit =
                 Attribute.Unit (Just $ toSymbolOrAlias unitSetSymbol)
             , Attribute.element =
@@ -1828,20 +1829,20 @@ sortAttributesMapping =
         )
     ,
         ( intSort
-        , Default.def{Attribute.hook = Hook (Just "INT.Int")}
+        , Default.def{AttributeSort.hook = Hook (Just "INT.Int")}
         )
     ,
         ( boolSort
-        , Default.def{Attribute.hook = Hook (Just "BOOL.Bool")}
+        , Default.def{AttributeSort.hook = Hook (Just "BOOL.Bool")}
         )
     ,
         ( stringSort
-        , Default.def{Attribute.hook = Hook (Just "STRING.String")}
+        , Default.def{AttributeSort.hook = Hook (Just "STRING.String")}
         )
     , -- Also add attributes for the implicitly defined sorts.
 
         ( stringMetaSort
-        , Default.def{Attribute.hook = Hook (Just "STRING.String")}
+        , Default.def{AttributeSort.hook = Hook (Just "STRING.String")}
         )
     ]
 

kore/test/Test/Kore/Variables/V.hs

@@ -13,9 +13,9 @@ import Data.Sup
 import Debug
 import GHC.Generics qualified as GHC
 import Generics.SOP qualified as SOP
-import Kore.Internal.TermLike
+import Kore.Internal.TermLike hiding (counter)
 import Kore.Unparser
-import Kore.Variables.Fresh
+import Kore.Variables.Fresh hiding (counter)
 import Numeric.Natural
 import Prelude.Kore
 import Pretty

kore/test/Test/Kore/Variables/W.hs

@@ -14,13 +14,13 @@ import Data.Sup
 import Debug
 import GHC.Generics qualified as GHC
 import Generics.SOP qualified as SOP
-import Kore.Internal.TermLike
+import Kore.Internal.TermLike hiding (counter)
 import Kore.Unparser
-import Kore.Variables.Fresh
+import Kore.Variables.Fresh hiding (counter)
 import Numeric.Natural
 import Prelude.Kore
 import Pretty
-import Test.Kore.Variables.V
+import Test.Kore.Variables.V hiding (counter)
 
 data W = W {value :: String, counter :: Maybe (Sup Natural)}
     deriving stock (Show, Eq, Ord)

kore/test/Test/Kore/With.hs

@@ -354,7 +354,7 @@ instance
 newtype VariableElement child = VariableElement {getVariableElement :: child}
 
 instance
-    (Hashable child, Ord child) =>
+    Hashable child =>
     With
         (NormalizedAc NormalizedSet Key child)
         (VariableElement child)
@@ -379,15 +379,15 @@ instance
                 internalSet
 
 instance
-    (Hashable child, Ord child) =>
+    Hashable child =>
     With
         (NormalizedAc NormalizedSet Key child)
         [VariableElement child]
     where
     with = foldl' with
 
 instance
-    (Hashable child, Ord child) =>
+    Hashable child =>
     With
         (NormalizedSet Key child)
         (VariableElement child)
@@ -398,7 +398,7 @@ instance
             NormalizedSet (ac `with` value)
 
 instance
-    (Hashable child, Ord child) =>
+    Hashable child =>
     With
         (NormalizedSet Key child)
         [VariableElement child]