FStarLang/FStar

Stack overflow with --print_universes

Closed this issue · 0 comments

This just threw me off

type test1 (a:Type0) : Type u#0 =
$ ./bin/fstar.exe Type.fst --debug Tac --print_universes  --debug Extreme 
Will try to load cmxs files: []
Opening file Type.fst
Chosen Z3 executable: z3-4.8.5
+++++++++++Encoding externals from cache for module Prims ... 919 decls
Done encoding externals from cache for module Prims
+++++++++++Encoding externals from cache for module FStar.Pervasives.Native ... 1278 decls
Done encoding externals from cache for module FStar.Pervasives.Native
+++++++++++Encoding externals from cache for interface FStar.Pervasives ... 2100 decls
Done encoding externals from cache for interface FStar.Pervasives
Opening file Type.fst
Checking module: Type
Now verifying implementation of Type
>>>>>>>>>>>>>>Checking top-level Sig_bundle decl type test1 (a: Type0) =
Processing type Type.test1
>>>>>>>>>>>>>>tc_decl type test1 (a: Type0) =
>>>>>>>>>>>>>>tc_inductive []
Checking binders (a: Type0)
Checking binder a#2:Type0 at type Type u#_
Typechecking Type.fst(3,14-3,19) (Tm_type): Type0
Unexpected error; please file a bug report, ideally with a minimized version of the source program that triggered the error.
Stack overflow