hashable? gates the type and not the operations, and say so where it bites

A map keyed by a type variable cannot be put into inside a generic body:
the hash and the equality are concrete symbols chosen from the concrete
key type, and there is none until the copy exists. The refusal now says
that, and says what hashable? does buy - taking and returning a
(Map $t V) - rather than leaving the reader to infer it.

Closing the hole means adding the map operations to the list of forms
the abstract pass defers to instantiation. That list is print and
println and nothing else, and every member is a place where a refusal
moves from the definition to a call site, which is what the abstract
pass exists to prevent. Two is short enough to hold in your head.

Also written down: four of the prelude's copyable? declarations are
convention rather than checker-enforced. The move analysis tracks
locals, not reads out of a slice, so swap! and friends check without it
- and would still duplicate a header at [(Vec i32)].

lib/check.ml

@@ -1227,13 +1227,27 @@ let rec key_pair env loc (k : Types.t) : Tast.fnref * Tast.fnref =
      than assumed — falling through to [bytewise_key] would hash whatever
      bytes the variable turned out to have, which is the wrong answer for a
      [string] and for any struct with padding. Inside an instantiation this
-     arm is unreachable: [env.subst] has already made [k] concrete. *)
+     arm is unreachable: [env.subst] has already made [k] concrete.
+
+     **This is a known hole and it is deliberate.** It means [hashable?] gates
+     the *type* and not the operations: a generic may take or return a
+     [(Map $t V)] under it, and may not [put], [get] or [has?] into one. The
+     alternative is to add the map operations to the list of forms the
+     abstract pass defers to instantiation — the list [print] and [println]
+     are the only members of — and every member of that list is a place where
+     a refusal moves from the definition to a call site, which is the thing
+     the abstract pass exists to prevent. Two members is a short list worth
+     keeping short; six is a rule nobody can hold in their head. If a generic
+     over maps is ever wanted, this is the decision to revisit, and it is one
+     line here plus one in [key_fns]. *)
   | Types.Var v ->
     Loc.failk "check/generic-map-key" loc
-      "a map keyed by the type variable %s cannot have its hash and equality \
+      "a map keyed by the type variable %s cannot be operated on here: the \
-       emitted here — they are chosen from the concrete type, which does not \
+       hash and the equality are emitted as concrete symbols chosen from the \
-       exist until this generic is instantiated. The key pair is emitted per \
+       concrete key type, and there is no concrete key type until this \
-       copy, so this operation belongs in a body the checker has substituted" v
+       generic is instantiated. {:where (hashable? $%s)} says the map may be \
+       taken and returned, not that its keys can be hashed here — write the \
+       operation in a function over the concrete key type and call that" v v
   | Types.String -> Tast.Rtfn "flan_hash_str", Tast.Rtfn "flan_eq_str"
   | t when bytewise_key t ->
     Tast.Rtfn "flan_hash_flat", Tast.Rtfn "flan_eq_flat"

lib/prelude.ml

@@ -166,9 +166,21 @@ let source = {flan|
 ;; stricter rule and assuming it can only refuse a valid program rather than
 ;; admit a broken one: [reduce]'s accumulator is read into [f] and then
 ;; assigned again, which is correct at [i32] and a double move at [(Vec i32)],
-;; and the checker cannot tell which until it substitutes. So the ones that
+;; and the checker cannot tell which until it substitutes.
-;; hold an element in a local say [copyable?] and the ones that only move
+;;
-;; elements between slots do not.
+;; **Two of these ten are forced and the rest are convention, and the
+;; difference is worth knowing.** [filter] and [reduce] do not check without
+;; [copyable?]: the first returns a [(Vec $t)], and a Vec of an owning element
+;; is refused, and the second holds its accumulator in a local and reads it
+;; twice. [swap!], [reverse!], [map!] and [sort-by!] check *without* it,
+;; because the move analysis tracks locals and parameters and does not track a
+;; read out of a slice — so [(let [t (at s i)] ... (set (at s j) t))] is not
+;; seen as a move even when the element owns storage. They declare it anyway,
+;; and should: at [[(Vec i32)]] those bodies would duplicate a header. It is
+;; the one place move-by-default is not conservative, and until element-level
+;; moves are tracked, a [copyable?] on a body that moves elements between
+;; slots is a convention the reader has to keep rather than a fact the checker
+;; enforces.
 ;;
 ;; **What did not collapse, and why it should not.** [sum-i32] and [sum-f32]
 ;; widen their element into [i64] and [f64]; "the wider type $t accumulates

test/test_flan.ml

@@ -2194,12 +2194,20 @@ let () =
     "(defn outer [s [$t]] () {:where (ordered? $t)} (sort! s))";
 
   (* A map key that is a type variable has no hash and no equality to emit:
-     they are chosen from the concrete type, which does not exist yet. *)
+     they are chosen from the concrete type, which does not exist yet. So
+     hashable? gates the *type* and not the operations — a generic may take
+     and return a (Map $t V) and may not put into one. Pinned because it is a
+     deliberate hole and not an oversight: closing it means adding the map
+     operations to the list of forms the abstract pass defers to
+     instantiation, which is print and println and should stay that short. *)
   rejects_check "a map keyed by a type variable that is not hashable?"
     ~needle:"is not a map key"
     "(defn f [m (Map $t i32)] i32 {:where (copyable? $t)} (len m))";
   accepts "and hashable? is what says it is"
     "(defn f [m (Map $t i32)] i32 {:where (hashable? $t)} (len m))";
+  rejects_check "but hashable? does not make the key hashable here"
+    ~needle:"not that its keys can be hashed here"
+    "(defn f [m (Map $t i32)  k $t] () {:where (hashable? $t)} (put m k 1))";
 
   (* ── The acceptance program checks end to end ──────────────────── *)
   accepts "calc-me.flan type checks"