agda / agda

Agda is a dependently typed programming language / interactive theorem prover.
https://wiki.portal.chalmers.se/agda/pmwiki.php
Other
2.41k stars 339 forks source link

New error warning `ConstructorDoesNotFitInData` instead of hard error. #7292

Closed andreasabel closed 4 weeks ago

andreasabel commented 1 month ago

When we check that the sort of the constructor (resp. constructor argument) fits into the sort of the data type, we now catch the error and wrap it into the ConstructorDoesNotFitData warning.

This warning is not benign and cannot be turned off, but one can continue coding interactively now as this is no longer a hard error.