Consider only variable identifier for equality

kore/src/Kore/Internal/Substitution.hs

@@ -314,24 +314,25 @@ wrap xs = Substitution xs
 -- | Wrap the list of substitutions to a normalized substitution. Do not use
 -- this unless you are sure you need it.
 unsafeWrap
-    :: Ord variable
+    :: HasCallStack
+    => Ord variable
     => [(UnifiedVariable variable, TermLike variable)]
     -> Substitution variable
 unsafeWrap =
     NormalizedSubstitution . List.foldl' insertNormalized Map.empty
   where
     insertNormalized subst (var, termLike) =
+        Map.insert var termLike subst
         -- The variable must not occur in the substitution
-        assert (Map.notMember var subst)
+        & assert (Map.notMember var subst)
         -- or in the right-hand side of this or any other substitution,
-        $ assert (not $ occurs termLike)
-        $ assert (not $ any occurs subst)
+        & assert (not $ occurs termLike)
+        & assert (not $ any occurs subst)
         -- this substitution must not depend on any substitution variable,
-        $ assert (not $ any depends $ Map.keys subst)
+        & assert (not $ any depends $ Map.keys subst)
         -- and if this is an element variable substitution, the substitution
         -- must be defined.
-        $ assert (not $ isElemVar var && isBottom termLike)
-        $ Map.insert var termLike subst
+        & assert (not $ isElemVar var && isBottom termLike)
       where
         occurs = TermLike.hasFreeVariable var
         depends var' = TermLike.hasFreeVariable var' termLike

kore/src/Kore/Syntax/Variable.hs

@@ -56,9 +56,33 @@ data Variable = Variable
     , variableCounter :: !(Maybe (Sup Natural))
     , variableSort :: !Sort
     }
-    deriving (Eq, GHC.Generic, Ord, Show)
+    deriving (GHC.Generic, Show)
 
-instance Hashable Variable
+-- TODO (thomas.tuegel): Move variableSort out of Variable entirely, so that
+-- only the identifiers remain.
+
+instance Eq Variable where
+    (==) a b =
+            on (==) variableName a b
+        &&  on (==) variableCounter a b
+    {-# INLINE (==) #-}
+
+{- | 'Variable' is uniquely identified by 'variableName' and 'variableCounter'.
+
+Two 'Variable's with the same 'variableName' and 'variableCounter' but different
+'variableSort's are not different so much as they are /inconsistent/.
+
+ -}
+instance Ord Variable where
+    compare a b =
+            on compare variableName a b
+        <>  on compare variableCounter a b
+    {-# INLINE compare #-}
+
+instance Hashable Variable where
+    hashWithSalt salt Variable { variableName, variableCounter } =
+        salt `hashWithSalt` variableName `hashWithSalt` variableCounter
+    {-# INLINE hashWithSalt #-}
 
 instance NFData Variable
 

kore/test/Test/Kore/Step/Axiom/Matcher.hs

@@ -384,7 +384,7 @@ test_matcherVariableFunction =
     ]
   where
     aSubSub = Mock.functional00SubSubSort
-    xSub = ElementVariable $ Variable (testId "x") mempty Mock.subSort
+    xSub = ElementVariable $ Variable (testId "xSub") mempty Mock.subSort
 
 test_matcherNonVarToPattern :: [TestTree]
 test_matcherNonVarToPattern =