Issue402.agda

module Issue402 where

record Unit : Set where
  constructor inn
  field
    out : Unit

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

test : (x y : Unit) -> x == y
test x y = refl

-- this used to cause an infinite loop in the conversion checker
-- now it fails, because no eta-laws are generated for the
-- unguarded recursive record Unit