-- 2010-10-15
-- 2018-06-09

{-# OPTIONS --irrelevant-projections #-}

module DoNotEtaExpandMVarsWhenComparingAgainstRecord where

open import Common.Irrelevance

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

record IR : Set1 where
  constructor mkIR
  field
    .fromIR : Set

open IR

reflIR2 : (r : IR) -> _ == mkIR (fromIR r)
reflIR2 r = refl {a = _}
-- this would fail if
-- ? = mkIR (fromIR r)
-- would be solved by
-- mkIR ?1 = mkIR (fromIR r)
-- because then no constraint is generated for ?1 due to triviality
