why the following clojure core.logic expression returns no solutions? `(run* [a b] (== {:a b} {a :b}))`

Question

Why the first expression (involving maps) doesn't yield any solutions, whereas the second one (involving vectors) does?

(run* [a b] (== {:a b} {a :b}))

;> ()

but

(run* [a b] (== [:a b] [a :b]))

;> ([:a :b])

To narrow down the problem to map unifications, here are examples illustrating different treatments of map keys and values.

(u/unify ['{:a ?b}
          '{:a :b}])  ;=> {:a :b}

(u/unify ['{?a :b}
          '{:a :b}])  ;=> nil

Answer 1

I am not an expert in the core.logic implementation, but I found what looks like the unification algorithm for maps:

(defn unify-with-map* [u v s]
  (when (clojure.core/== (count u) (count v))
    (loop [ks (keys u) s s]
      (if (seq ks)
        (let [kf (first ks)
              vf (get v kf ::not-found)]
          (when-not (identical? vf ::not-found)
            (if-let [s (unify s (get u kf) vf)]
              (recur (next ks) s)
              nil)))
        s))))

It makes no effort to unify map keys. It requires the two maps be the same size, with the same keys. If that is so, it unifies the corresponding values for each key.

Answer 2

The described behavior is deliberate and not a bug. It looks like the map unification doesn't try to substitute the keys by design as a given map's value might not necessarily be related to the same key in the other map.