Closed UlfNorell closed 10 years ago
UlfNorell
commented
10 years ago From nils.anders.danielsson on October 18, 2013 09:14:11
Status: Accepted
Owner: andreas....@gmail.com
Labels: Type-Defect Priority-High Milestone-2.3.4 Termination Conversion
UlfNorell
commented
10 years ago From andreas....@gmail.com on October 20, 2013 09:59:48
This issue is actually not caused by the termination check itself, but by the disabling of reductions in case of a failed termination check. These disabled reductions make the final constraint solving pass go berserk. E.g., suddenly a constructor has a type that does not reduce to a data type [it did reduce previously, since during initial termination checking, all functions are believed to be terminating, and reductions are enabled].
I fixed this issue on my machine, yet it depends on other patches, and I do not want to backport now.
Summary: Internal error (Conversion.hs:501) triggered non-reducing definitions (was: Internal error (Conversion.hs:501) triggered by termination check)
Labels: Constraints
UlfNorell
commented
10 years ago
From sattler....@gmail.com on October 16, 2013 16:50:16
Yet another internal error encountered when trying to internalize type theory. This time I couldn't minimize the code example beyond the attached file.
The current development version (after applying the patch fixing http://code.google.com/p/agda/issues/detail?id=918 ) reports:
An internal error has occurred. Please report this as a bug. Location of the error: src/full/Agda/TypeChecking/Conversion.hs:501
Giving --no-termination-check eliminates the error. Swapping the two indicated lines of code eliminates the error.
Attachment: Bug2.agda
Original issue: http://code.google.com/p/agda/issues/detail?id=921