Agda-2.3.2.2: test/fail/SortDependingOnIndex.agda
{-# OPTIONS --universe-polymorphism #-}
module SortDependingOnIndex where
open import Imports.Level
data Bad : (l : Level) → Set l where
{-# OPTIONS --universe-polymorphism #-}
module SortDependingOnIndex where
open import Imports.Level
data Bad : (l : Level) → Set l where