Issue133.agda

module Issue133 where

data Nat : Set where
  zz : Nat
  ss : Nat → Nat

data _==_ {X : Set}(x : X) : X → Set where
  refl : x == x

data Zero : Set where

data Eq? (x : Nat) : Nat → Set where
  same : Eq? x x
  diff : {y : Nat} → (x == y → Zero) → Eq? x y

-- This failed before due to absurd lambda checking not getting
-- postponed.
ioo : {y : Nat} → Eq? zz (ss y)
ioo {y} = diff λ ()

foo : {y : Nat} → zz == ss y → Zero
foo ()

goo : {y : Nat} → zz == ss y → Zero
goo = λ ()

hoo : {y : Nat}{X : Set} → ((zz == ss y → Zero) → X) → X
hoo boo = boo λ ()