search

UlfNorell / agda-test

Agda test
0 stars 0 forks source link

An internal error #971

Closed UlfNorell closed 10 years ago

UlfNorell commented 10 years ago

From mech...@botik.ru on November 20, 2013 15:13:42

When type-checking (under emacs) the module AlgClasses01.agda of my project, the report is

An internal error has occurred. Please report this as a bug. Location of the error:

src/full/Agda/Syntax/Translation/AbstractToConcrete.hs:362

It looks like the responsible place is in the end:

record EuclideanRing : Set (α ⊔ α=) where ... b∣x--rem-x-b : (b x : C) → let r = eucRem x b in b ∣ (x - r) b∣x--rem-x-b b x with b ≟ 0# ... | yes _ = (0# , *0 b)

This is for Agda version 2.3.2.2, MAlonzo, lib-0.7, Debian Linux.

This is 5 modules, with many code parts replaced with `postulate' -- in order to simplify the report code. I think, the example can be simplified much further.

Unzip it,
take AlgClasses01.agda into emacs and apply Control-C Control-l.

Attachment: repNov18-2013.zip

Original issue: http://code.google.com/p/agda/issues/detail?id=971

UlfNorell commented 10 years ago

From ulf.nor...@gmail.com on November 20, 2013 07:10:05

Looks like this has been fixed. I can't reproduce the problem in the development version.

Status: Fixed