Seems like a rather arbitrary restriction, no?

Global inference is a whole other world, I think if you're trying to nail down the fields of a record and their types using global analysis it might be a necessary restriction. But take it with a grain of salt, haven't thought about this in 5 years.

The basic model for type inference is sets, right?

Yeah sets of constraints. It's a delicate balance of expressivity to make them solvable.

Can't maps be inferred then by treating them as a union of constraints regarding the occurrence of their entries?

Maybe that just breaks everything, I'm no expert

I think you're right in terms of inference, but if you have 2 different records with the same field name, the type system won't know which record you're referring to.

(defn foo [m1] (inc (:a m1))
(defn bar [m2] (name (:a m2))
(foo {:a 1})
(bar {:a 'a})

You still need (inc (:a m1)) to type check. So you need to choose. And IIRC it's simply forbidden so the choice is made implicitly.

Why can't they be different sets? Their Union succeeds and their intersection fails. Their inference is tracked just like any set propagating through the calculation. What I'm missing is the need to have a global state associated with it

Good point, I went back to the papers to stop guessing. You're right, the functions are inferred separately with polymorphic rows. See sections 2.1, 2.2 in https://caml.inria.fr/pub/papers/garrigue-structural_poly-fool02.pdf

I misremembered, the fields on an object are inferred on its definition, not its usages. see first example in https://caml.inria.fr/pub/papers/remy_vouillon-objective_ml-tapos98.pdf

I'm thinking not even doing anything with the types really, so lets assumes keys and values are just of type ANY. The question would be more:

(defn bazz [m] (get m :name))

And could you ask the type checker to list out all cases of the set of keys m could have from all the callsite to `bazz?

(bazz {:name 10 :age 10})
(bazz {:age 23})
(bazz (if wtv? {:hello true} {})

bazz is called with:
a :name key AND an :age key
or
a :age key
or
a :hello key
or
with no keys

So similarly, you could tell the type checker to assert that bazz is called with both a :name and :age key, and it could tell you if that's not the case. And maybe it could help you find where in the code woulds it get called without those keys.

And finally, I know some places would be undecidable, like say:

(bazz (hash-map (keyword (slurp "foo.txt")) "John"))

And possibly it could let you add a runtime assertion and maybe the type checker could understand that or be told about it, for example:

(bazz (assert-key (hash-map (keyword (slurp "foo.txt")) "John") :name))

So now even though its dynamic, the checker would know that this should make it so the map contains the :name key as well.

Maybe calling it a type checker would be wrong, it be more like a static key checker.