Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Showing content from https://github.com/agda/agda/issues/7382 below:

Agda 2.7.0-rc1 crashes when run twice, probably serialization issue · Issue #7382 · agda/agda · GitHub

With the test case from #7380:

open import Agda.Builtin.IO
open import Agda.Builtin.Unit
open import Agda.Builtin.Nat
open import Agda.Builtin.Sigma

record R : Set where
  field x : Nat

variable r : R

data D : R → Nat → Set where
  c : let open R r in D r x

f : R → Nat
f x = fst g
  where
    g : Σ Nat (D x)
    g = (_ , c)

postulate print : Nat → IO ⊤
{-# COMPILE GHC print = print #-}

main = print (f (record { x = 3 }))

I get a crash if I run 2.7.0-rc1 twice on this file:

$ agda-2.7.0-rc1 Issue7380.agda && agda-2.7.0-rc1 -c Issue7380.agda
An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE_VERBOSE__, called at src/full/Agda/TypeChecking/Reduce.hs:224:18

The internal error goes away with

.

Also, it cannot be triggered in 2.6.4.3 with

, so it must be a fresh regression in the

feature.

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4