Issue396.agda

module Issue396 where

record ⊤ : Set where
  constructor tt

foo : (P : ⊤ → Set) →
      ((x : ⊤) → P x → P x) →
      (x y : ⊤) → P x → P y
foo P hyp x y = hyp x

-- Error was:
-- x != y of type ⊤
-- when checking that the expression hyp x has type P x → P y