FStarLang/FStar
GitHub で見るShadowed binding results in confusing type mismatch error
Open
#1,082 opened on 2017年6月14日
area/error-messagesarea/usabilitycomponent/printergood first issue
Repository metrics
- Stars
- (3,068 stars)
- PR merge metrics
- (PR metrics pending)
説明
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.