FStarLang/FStar

Shadowed binding results in confusing type mismatch error

Open

#1082 aperta il 14 giu 2017

Vedi su GitHub
 (1 commento) (0 reazioni) (0 assegnatari)F* (258 fork)auto 404
area/error-messagesarea/usabilitycomponent/printergood first issue

Metriche repository

Star
 (3068 star)
Metriche merge PR
 (Metriche PR in attesa)

Descrizione

I ran into a type mismatch that was confusing because the reported expected and actual types were identical. The difference turned out to be that I had (intentionally) shadowed a variable with a formal parameter in a let binding, and my types differed in which binding was referenced. Here's a reduced example of the error message:

module Shadowed_type_mismatch

open FStar.Seq

val index' : ns:seq nat -> i:nat{i < length ns} -> nat
let index' ns i =
  let f (ns:seq nat) : nat =
      index ns i in
  f ns
$ fstar.exe shadowed_type_mismatch.fst
./shadowed_type_mismatch.fst(8,15-8,16): (Error) Subtyping check failed; expected type (i:Prims.nat{ Prims.b2t (i < FStar.Seq.Base.length u#0 ns) }); got type (i:Prims.nat{ Prims.b2t (i < FStar.Seq.Base.length u#0 ns) }) (see also /usr/local/Cellar/fstar/HEAD-cf96c5a_1/ulib/FStar.Seq.Base.fst(30,49-30,61))
Verified module: Shadowed_type_mismatch (583 milliseconds)
1 error was reported (see above)

It would be great if these two bindings were disambiguated somehow.

Guida contributor