CompareLevel.agda

{-# OPTIONS --universe-polymorphism #-}
module CompareLevel where

open import Common.Level

postulate
  X : Set
  Foo : (a b : Level) → Set (a ⊔ b) → Set
  Bar : Foo _ _ X  -- solve _1 ⊔ _2 = 0

postulate
  id    : ∀ {a}{A : Set a} → A → A
  apply : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) → A → B
  a b   : Level
  Any   : (ℓ : Level) → Set ℓ
  any   : ∀ {ℓ} → Any ℓ

-- Too aggressive level solving can cause a problem here.
foo : Any (a ⊔ b)
foo =
  apply {_}{_} id any