Issue292-23.agda

-- Andreas, 2011-09-21, reported by Nisse
-- {-# OPTIONS -v tc.lhs.unify:25 #-}
module Issue292-23 where

data ⊤ : Set where
  tt : ⊤

data D : (A : Set) → A → Set₁ where
  d : (A : Set) (x : A) → D A x

data P : (x : ⊤) → D ⊤ x → Set₁ where
  p : (x : ⊤) → P x (d ⊤ x)

Foo : P tt (d ⊤ tt) → Set₁
Foo (p .tt) = Set
-- should work
-- bug was caused by a use of ureduce instead of reduce