search

UlfNorell / agda-test

Agda test
0 stars 0 forks source link

Impossible when inlining with call during termination checking #970

Closed UlfNorell closed 10 years ago

UlfNorell commented 10 years ago

From Fredriks...@gmail.com on November 19, 2013 17:06:55

Consider the following code (using the latest darcs version of the standard library):

begin{code} open import Data.Unit hiding (≟) open import Relation.Nullary open import Relation.Binary.PropositionalEquality

module Bug (≟ : (n n' : ⊤) → Dec (n ≡ n')) where

open import Data.Product open import Data.Maybe

data Blah (a : Maybe ⊤ × ⊤) : Set where blah : {b : Maybe ⊤ × ⊤} → Blah b → Blah a

update : {A : Set} → ⊤ → A → A update n m with n ≟ n update n m | yes p = m update n m | no ¬p = m

bug : {x : Maybe ⊤ × ⊤} → proj₁ x ≡ nothing → Blah x bug ia = blah (bug (subst (λ _ → proj₁ (update tt (nothing , tt)) ≡ nothing) refl refl)) \end{code}

(This is nonsensical since it's a boiled down version of something less nonsensical.)

Trying to load this using the latest darcs version of Agda, I get:

"An internal error has occurred. Please report this as a bug. Location of the error: src/full/Agda/Termination/Inlining.hs:236"

On the other hand, it loads (with lots of yellow, etc) if I rollback the following recent patch:

"Wed Nov 13 19:07:23 GMT 2013 ulfn@chalmers.se

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

UlfNorell commented 10 years ago

From Fredriks...@gmail.com on November 19, 2013 08:17:29

Status: New
Owner: ---

UlfNorell commented 10 years ago

From ulf.nor...@gmail.com on November 19, 2013 08:18:57

Summary: Impossible when inlining with call during termination checking (was: Previously working code yields an internal error)
Status: Accepted
Owner: ulf.nor...@gmail.com
Labels: Type-Defect Priority-High Milestone-2.3.4 Termination With

UlfNorell commented 10 years ago

From ulf.nor...@gmail.com on November 20, 2013 02:37:55

Status: Fixed