diff --git a/lib/check.ml b/lib/check.ml index 679d21d..be3594d 100644 --- a/lib/check.ml +++ b/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 \ - emitted here — they are chosen from the concrete type, which does not \ - exist until this generic is instantiated. The key pair is emitted per \ - copy, so this operation belongs in a body the checker has substituted" v + "a map keyed by the type variable %s cannot be operated on here: the \ + hash and the equality are emitted as concrete symbols chosen from the \ + concrete key type, and there is no concrete key type until this \ + 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" diff --git a/lib/prelude.ml b/lib/prelude.ml index 553014f..d5f1ee6 100644 --- a/lib/prelude.ml +++ b/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 -;; hold an element in a local say [copyable?] and the ones that only move -;; elements between slots do not. +;; and the checker cannot tell which until it substitutes. +;; +;; **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 diff --git a/test/test_flan.ml b/test/test_flan.ml index a2239b7..264355c 100644 --- a/test/test_flan.ml +++ b/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"