record R : Set₁ where
field f1 : ∀ {A : Set} → A
bla = f1 -- creates an unsolved meta _A
field f2 : Set
-- Field f1 is highlighted yellow.
-- Yellow should not be there at least not at definition of f1.
-- Maybe it could be at definition of bla (but should also not).
From andreas....@gmail.com on November 17, 2013 00:59:28
record R : Set₁ where field f1 : ∀ {A : Set} → A bla = f1 -- creates an unsolved meta _A field f2 : Set
-- Field f1 is highlighted yellow. -- Yellow should not be there at least not at definition of f1. -- Maybe it could be at definition of bla (but should also not).
-- Yellow disappears if bla or f2 is removed.
See also issue 783 and issue 655 .
Original issue: http://code.google.com/p/agda/issues/detail?id=966