Use meta-programming in F* for a syntactic check on a function argument

Question

I would like to write a function that enforces that its argument is, syntactically, a constant string. Here's what I tried:

module Test

module R = FStar.Reflection

let is_literal (t: R.term) =
  match R.inspect_ln t with
  | R.Tv_Const (R.C_String _) -> true
  | _ -> false

let check_literal (s: string { normalize (is_literal (`s)) }) =
  ()

let test () =
  check_literal ""; // should work
  let s = "" in
  check_literal s // should not work

However, I'm pretty sure static quotations (with `) are not what I want, but instead dynamic quotations with quote. But this would put my precondition into the Tac effect. Is there any way to do what I want in the current state of things?

Answer 1

I don't know if you finally found a solution, but what about implicit meta arguments?

They somehow allow running Tac code at function invocation time, making quote usable.

Changing your code a bit doing so seems to work:

module Is_lit

open FStar.Tactics

let is_literal (t: term) =
  match inspect_ln t with
  | Tv_Const (C_String _) -> true
  | _ -> false

let check_literal (s: string)
                  (#[(if (normalize_term (is_literal (quote s)))
                      then exact (`())
                      else fail "not a litteral")
                    ] witness: unit)
                  : unit =
  ()

// success
let _ = check_literal "hey" 

// failure
[@expect_failure]
let _ = let s = "hey" in check_literal s