FStarLang/FStar

Shadowed binding results in confusing type mismatch error

Open

#1,082 opened on Jun 14, 2017

View on GitHub
 (1 comment) (0 reactions) (0 assignees)F* (258 forks)auto 404
area/error-messagesarea/usabilitycomponent/printergood first issue

Repository metrics

Stars
 (3,068 stars)
PR merge metrics
 (PR metrics pending)

Description

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.

Contributor guide