Aseem Rastogi

Thanks for the minimization of the releases @hacklex, much appreciated. I have a hunch that it has something to do with normalizing return type annotations in the auto generated projectors....

The fix is a little tricky, in the meantime you could apply the following patch temporarily while we fix the issue: ``` aseem@MSRI-5166880:~/CuteCAS$ git diff diff --git a/AlgebraTypes.fst b/AlgebraTypes.fst index...

See https://github.com/FStarLang/FStar/pull/2256 for dependent pattern matching

Here is a minimal repro without any typeclasses etc.: ``` let compile_option : (option int -> option int) = fun x -> match x with | None -> None |...

Please see #2654.

Restricting reify means that it is no longer an unsoundness, but keeping the issue open, we can use it to track support for indexed effects reification.

We are looking at upgrading to the latest 4.8.15 release. It is a bit involved because it requires accommodating other projects that are part of our CI. Will keep posting...

It is a parser issue, negative int literals are not supported as patterns in the parser. As a workaround, you could also use `if then else`: ``` let example_1 (s:sign)...

Related to #2635.

The issue was automatically closed but #2760 fixes it only partially, we still need to implement the check for degenerate effects.