Failure("Not an imp") when defining mutually recursive types with refinement and `List.Tot.map`

[tahina-pro]

Consider the following F* file:

module Te
type typ = | TStruct: (l: struct_typ) ->  typ
and struct_typ = (l: list (unit * typ) {
  Cons? (List.Tot.map fst l)
} )

This file successfully checks in command line with the latest F* master. But in interactive mode, here is what happens, when verifying, or even when lax-type-checking, or even just when verifying the first line and jumping to line 4.

[F* error] Unexpected error; please file a bug report, ideally with a minimized version of the source program that triggered the error.
[F* error] Failure("Not an imp")
F*: subprocess exited.

Changing the refinement to not using List.Tot.map makes the problem disappear.

[cpitclaudel]

Thanks. Bugs in interactive mode are better reported on the FStar tracker, though (unless you want me to do something about this in ELisp ^^).

To make the bug easily reproducible, you can use M-x fstar-toggle-debug before running through your example, and then M-x fstar-write-transcript to save a copy of a transcript file that can be fed to fstar.exe --ide. With that it should be easy to replay the error and fix it (and even add a test for it :)

I tried to do this for your example, but surprisingly I couldn't reproduce it, so the above process will be even more useful :)

[tahina-pro]

Thank you for the tips @cpitclaudel ! You are right, I cannot reproduce this issue on my other machine... I'll file it again on F* if it ever happens again.