Issue348.agda

module Issue348 where

import Common.Irrelevance  

data _==_ {A : Set1}(a : A) : A -> Set where
  refl : a == a

record R : Set1 where
  constructor mkR
  field
    .fromR : Set

reflR : (r : R) -> r == r
reflR r = refl {a = _}
-- issue: unsolved metavars resolved 2010-10-15 by making eta-expansion
-- more lazy (do not eta expand all meta variable listeners, see MetaVars.hs