Issue331.agda

-- 2010-10-15

module Issue331 where

record ⊤ : Set where
  constructor tt

data Wrap (I : Set) : Set where
  wrap : I → Wrap I

data B (I : Set) : Wrap I → Set₁ where
  b₁ : ∀ i → B I (wrap i)
  b₂ : {w : Wrap I} → B I w → B I w
  b₃ : (X : Set){w : Wrap I}(f : X → B I w) → B I w

ok : B ⊤ (wrap tt)
ok = b₂ (b₁ _)

-- Issue 331 was: Unsolved meta: _45 : ⊤
bad : Set → B ⊤ (wrap tt)
bad X = b₃ X λ x → b₁ _