module BadIdent

open FStar.Reflection
open FStar.Tactics

// The qualifier `Projector` and `univ_name` both contains `ident`
// to illustrate the embedding bug, let's try to extract `ident`s:

// dummy type so that we can grab a projector
type typ = | Foo: v:unit -> typ
// dummy top-level with univ variable
let foo (_: Type u#a) = ()

[@@expect_failure
// (Error 228) user tactic failed: `exact: Cannot type [Visible_default; Projector ["BadIdent"; "Foo"] ("v", <input>(8,18-8,19))] in context (). Error = (Expected type "name * ident"; but "["BadIdent"; "Foo"]" has type "list string")
]
let proj: list qualifier =  _ by (
    let t = lookup_typ (top_env ()) (explode_qn (`%Foo?.v)) in
    guard (Some? t);
    let quals: list qualifier = sigelt_quals (Some?.v t) in
    exact (quote quals)
  )

[@@expect_failure
// (Error 228) user tactic failed: `exact: "a", <input>(21,19-21,20) : string * range does not exactly solve the goal range * string (witness = (*?u161*) _)`
]
let se1: range * string (* aka FStar.Reflection.Types.ident *) =  _ by (
    let t = lookup_typ (top_env ()) (explode_qn (`%foo)) in
    guard (Some?   t); let t = inspect_sigelt (Some?.v t) in
    guard (Sg_Let? t); let Sg_Let _ t = t in
    guard (Cons?   t); let t::_ = t in
                       let t = (inspect_lb t).lb_us in
    guard (Cons? t);   let t::_ = t in
                       exact (quote t)
  )

// FStar.Reflection.Types defines ident as `range * string`, not ad `string * range`:
let _ = assert (FStar.Reflection.Types.ident == range * string)

// this works
let se3: string*range =  _ by (
    let t = lookup_typ (top_env ()) (explode_qn (`%foo)) in
    guard (Some?   t); let t = inspect_sigelt (Some?.v t) in
    guard (Sg_Let? t); let Sg_Let _ t = t in
    guard (Cons?   t); let t::_ = t in
                       let t = (inspect_lb t).lb_us in
    guard (Cons? t);   let t::_ = t in
                       exact (quote t)
  )