Agda-2.3.2.2: test/fail/Issue87.agda

module Issue87 where

data I : Set where

data D : I -> Set where
  d : forall {i} (x : D i) -> D i

bar : forall {i} -> D i -> D i -> D i
bar (d x) (d     y) with y
bar (d x) (d {i} y) | z = d {i} y

-- Panic: unbound variable i
-- when checking that the expression i has type I