Missing var signals expecting Type0

[briangmilnes]

Rewriting some stuff I bumped into a funny type checking error.

module MissingVar

open FStar.String

let streq_upto s1 s2 (pos: nat) =
  (pos <= strlen s1 /\ pos <= strlen s2 /\
   (forall (i: nat{i < pos}). index s1 i = index s2 i))

///  strlen is pointed to as nat when expecting Type0
let rec streq_upto'' (s1: string) (s2: string{strlen s1 = strlen s2}) 
    (from: nat{from < strlen s1})  (to: nat{to < strlen s1}) :
  Tot (b:bool{b <==> streq_upto s1 s2 to})
  (decreases strlen s1 - to)
=     
 if pos = strlen s1
 then 0
 else 0

on both the language server and the command line.

* Error 12 at src/MissingVar.fst(15,10-15,19):
  - Expected type Type0 but FStar.String.strlen s1 has type Prims.nat

this should be a very low priority.

[mtzguido]

pos is defined in prims, it's resolving to that.

(** The type of positive integers *)
type pos = i: int{i > 0}