[Agda] meta vars regression from version 2.3.2
Christian Sattler
sattler.christian at gmail.com
Sun Sep 15 02:04:56 CEST 2013
Dear all,
Below is a self-contained code sample that initially loads successfully
in interactive mode of the latest development version, highlighting the
single hole in the last line (along with several instances of yellow).
However, attempting to fill the hole with h results in the following
message:
An internal error has occurred. Please report this as a bug.
Location of the error: src/full/Agda/TypeChecking/MetaVars.hs:654
The hole-filling appears to work just fine under Agda 2.3.2.
Cheers,
Christian
-------------- next part --------------
{-# OPTIONS --without-K #-}
module Bug-2-3-3 where
record T : Set where
constructor tt
postulate
Id : {A : Set} → A → Set
e : {B : Set} {f : T → B} → Id (f tt) → Id f
k : {P : Set → Set} {u : P T} → Id u → T
q : Id tt → T
q h = k (e {!h!})
More information about the Agda
mailing list