search

FStarLang / FStar

A Proof-oriented Programming Language
https://fstar-lang.org
Apache License 2.0
2.7k stars 234 forks source link

Bad refinement triggers crash: tc_maybee_toplevel_term #3600

Closed briangmilnes closed 2 weeks ago

briangmilnes commented 2 weeks ago

[F error] Raised at FStarC_Compiler_Effect.raise in file "fstar-lib/FStarC_Compiler_Effect.ml" (inlined), line 7, characters 12-17 [F error] Called from FStarC_Errors.raise_error in file "fstar-lib/generated/FStarC_Errors.ml", line 956, characters 14-49 [F error] Called from FStarC_TypeChecker_TcTerm.tc_maybe_toplevel_term in file "fstar-lib/generated/FStarC_TypeChecker_TcTerm.ml", line 3795, characters 28-118 [F error] Called from FStarC_Compiler_Util.record_time_ns in file "fstar-lib/FStarC_Compiler_Util.ml", line 24, characters 14-18 [F* error] Called from FStarC_Compiler_Util.record_time_ms in file "fstar-lib/FStarC_Compiler_Util.ml", line 28, characters 18-34

The type checker does not like my accidental really bad refinement. F* 2024.09.05~dev platform=Linux_x86_64 compiler=OCaml 4.14.2 date=2024-10-24 17:40:26 -0700 commit=8b6fce63ca91b16386d8f76e82ea87a3c109a208

module ListSet type listset (e: eqtype) = (e': listset' e) let empty (#e: eqtype) : listset e = [] val isempty' (#e: eqtype) (ls : listset e) : Tot (b:bool{b <==> empty ls})

briangmilnes commented 2 weeks ago

This is purely in the language server. I'm going to have to get a better test case for this before you look at it.

briangmilnes commented 2 weeks ago

Shockingly this does not repeat after a boot but repeated multiple times for me. I suspect an out of memory or other system error. On the command line it ran, I had 8MB free. I can generate a stack exception but can't catch it. It would be good to test both and have an example of how to catch them. I'll close this.