Bad typing for range values

[mtzguido]

open FStar.Range

assume val p : range -> prop

assume val lem : r:range -> Lemma (p r)

let test () : range =
  let r = normalize_term (mk_range "asd" 1 2 3 4) in
  Classical.forall_intro lem;
  assert (p r);
  r

This fails to prove the property since the encoded range value is just a Range_const 0 without any useful axiom for its typing. We seem to add an axiom for the typing of range constants, but it's broken as it is specialized to a particular one:

;;;;;;;;;;;;;;;;Range_const typing
;;; Fact-ids: Name FStar.Range.range; Namespace FStar.Range
(assert (! (HasTypeZ (Range_const 1)
FStar.Range.range)
:named typing_range_const))