Issue203.agda

{-# OPTIONS --universe-polymorphism #-}

module Issue203 where

open import Imports.Level

-- shouldn't work
data Bad {a b} (A : Set a) : Set b where
  [_] : (x : A) → Bad A