UlfNorell
commented
10 years ago From andreas....@gmail.com on September 17, 2013 03:28:41
Owner: andreas....@gmail.com
Closed UlfNorell closed 10 years ago
UlfNorell
commented
10 years ago From andreas....@gmail.com on September 17, 2013 03:28:41
Owner: andreas....@gmail.com
UlfNorell
commented
10 years ago From andreas....@gmail.com on September 17, 2013 03:44:15
The problem is that Agda thinks it is impossible that a meta variable's type provides less domain types than the number of arguments it is applied to. This is apparently not always the case, maybe due to my change to Agda's blocking strategy (see issue 856 ).
I guess this bug surfaced because of my patch
Wed May 15 11:12:41 CEST 2013 Andreas Abel andreas.abel@ifi.lmu.de
UlfNorell
commented
10 years ago From andreas....@gmail.com on September 17, 2013 04:31:00
Status: Fixed
Labels: Meta
From nils.anders.danielsson on September 17, 2013 10:18:03
-- This bug was reported by Christian Sattler. (I modified his example -- slightly.)
module Bug where
record T : Set where constructor tt
postulate Id : (A : Set) → A → Set e : (B : Set) (f : T → B) → Id B (f tt) → Id (T → B) f k : (P : Set → Set) (u : P T) → Id (P T) u → T h : Id T tt
q : T q = k {!!} {!!} (e {!!} _ {!h!})
-- If one tries to give h:
-- An internal error has occurred. Please report this as a bug. -- Location of the error: src/full/Agda/TypeChecking/MetaVars.hs:654
Original issue: http://code.google.com/p/agda/issues/detail?id=903