Agda-2.3.2.2: test/fail/SortDependingOnIndex.err
SortDependingOnIndex.agda:6,6-9 The sort of Bad cannot depend on its indices in the type (l : Level) → Set l when checking the definition of Bad
SortDependingOnIndex.agda:6,6-9 The sort of Bad cannot depend on its indices in the type (l : Level) → Set l when checking the definition of Bad