[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