[Agda] how to set level

[Sergei Meshveliani]

Please, what is wrong in the below program?

I define Expression over a Semiring, and the relations _=e_ and _<e_ on
Expression.
But Agda 2.5.3 does not solve the level values.
First it forces the level  α=  for Expression.
And then, I cannot satisfy it with the level values for _<e_ and for the
Lift calls.
If I replace the last line RHS with `anything', then I can satisfy it.

I wonder what level expressions to set, where to set Lift, and with what
levels.

Thanks,
-------

Sergei


--**********************************************************************
open import Level    using (_⊔_; Lift)
open import Algebra  using (Semiring)
open import Algebra.FunctionProperties as FuncProp using (Op₂)
open import Relation.Binary using (Rel; IsStrictTotalOrder) 
                            renaming (Decidable to Decidable₂)
open import Relation.Binary.PropositionalEquality using (_≡_)
open import Data.Empty   using (⊥) 
open import Data.Unit    using (⊤) 
open import Data.Sum     using (_⊎_)
open import Data.Product using (_×_; _,_)
open import Data.Nat     using (ℕ) renaming (_≟_ to _≟n_; _<_ to _<n_) 

-------------------------------------------------------------------------
postulate anything : ∀ {a} {A : Set a} → A      -- for debug    


module Foo {α α= β} (R : Semiring α α=) 
                 (open Semiring R using (_≈_) renaming (Carrier to C))
                 (_≟_   : Decidable₂ _≈_)  
                 (_<_   : Rel C β)  
                 (isDTO : IsStrictTotalOrder _≈_ _<_)
  where  
  open Semiring R using (_+_) 

  data Expression : Set α where cf   : C → Expression
                                var  : ℕ → Expression  
                                _:+_ : Op₂ Expression 
  infixl 6 _:+_

  data _=e_ : Expression → Expression → Set α=
    where
    cfEq  :  ∀ {a b} → a ≈ b → cf a =e cf b 
    varEq :  ∀ {i j} → i ≡ j → var i =e var j
    +eq   :  ∀ {x x' y y'} → x =e x' → y =e y' → (x :+ y) =e (x' :+ y')


  _<e_ :  Rel Expression β        -- inverse lexicographic ordering
                         -- (α= ⊔ β) ?

  (cf a) <e (cf b)   =  (a < b)   -- Lift  will be forced if ...
  (cf _) <e (var _)  =  Lift ⊤ 
  (cf _) <e (_ :+ _) =  Lift ⊤ 

  (var i) <e (var j)  =  Lift (i <n j)
  (var _) <e (cf _)   =  Lift ⊥
  (var _) <e (_ :+ _) =  Lift ⊤

  (_ :+ _) <e (cf _)   =  Lift ⊥ 
  (_ :+ _) <e (var _)  =  Lift ⊥
  (x :+ y) <e (z :+ u) =  Lift (x <e z  ⊎  (x =e z × y <e u))
                          -- anything
--**************************************************************************