Issue689.agda

-- Andreas, 2012-10-02
-- {-# OPTIONS -v tc.conv.level:100 -v tc.constr.add:40 -v tc.meta:50 -v tc.inj.use:30 -v 80 #-}
module Issue689 where

open import Common.Level

data Bad : Set₁ where
  c : Set₁ → Bad

-- this should not leave unsolvable constraints, but report an error