More precise error on positivity violation
Open
area/error-messages
area/usability
kind/enhancement
- Dominant language
- F*
- Stars
- 3.1k
- Forks
- 266
- Avg merge
- 21h 1m
- Merged PRs (30d)
- 54
Description
When an inductive violates the positivity restriction the error message (`./debug.fst(11,0-26,18): (Error) Inductive type Debug.def_eq does not satisfy the positivity condition
`) is not really informative and it may be hard to find where it comes from (in particular when working with big inductives like AST or typing derivations).
Any idea on how to achieve that @aseemr ? (also it would be nice to be able to assume polarities when using `assume type`)
Contributor guide
Assessment
This issue has not been assessed yet.