[Agda] Question regarding a simple "dependently typed IF-THEN-ELSE"

[Konstantin Tretjakov]

Hello,

suppose I would like to be able to use if-then-else in something like the following:

   f t = if t then true else zero

My current attempt at doing it (Agda 2.3.0.1, Windows) is this:

--------------------------------
module Test1 where

postulate
   Level  : Set
   lze    : Level
   lsu    : Level -> Level
   lmax   : Level -> Level -> Level

{-# BUILTIN LEVEL         Level  #-}
{-# BUILTIN LEVELZERO     lze    #-}
{-# BUILTIN LEVELSUC      lsu    #-}
{-# BUILTIN LEVELMAX      lmax   #-}


data Bool : Set where
   true false : Bool

data ℕ : Set  where
   zero : ℕ
   suc : ℕ → ℕ

{- Set level of the return type of the if-then-else operator -}
if[Level]_then_else_ : Bool → Level → Level → Level
if[Level] true then x else y = x
if[Level] false then x else y = y

{- Return type of the if-then-else operator -}
if[Set*]_then_else_ : ∀ {i j} (t : Bool) → Set i → Set j → Set (if[Level] t then i else j)
if[Set*] true then A else B = A
if[Set*] false then A else B = B

{- Define the actual if-then-else operator -}
if_then_else_ : ∀ {i j}{A : Set i}{B : Set j}(t : Bool) → A → B → (if[Set*] t then A else B)
if true then x else y = x
if false then x else y = y


{- The test -}
f : (t : Bool) → if[Set*] t then Bool else ℕ
f t = if t then true else zero
--------------------------------

This seems to work fine. However, the version, where I use the "most general" 
if_then_else_ in the type declaration, i.e.:

   f : (t : Bool) → if t then Bool else ℕ
   f t = if t then true else zero

would not go through, reporting that:

   if[Set*] t then Set else Set !=< Set (_53 t) of type
   Set (if[Level] t then lsu lze else lsu lze)
   when checking that the expression if t then Bool else ℕ has type
   Set (_53 t)

I do not understand the reason for this behaviour. Is it a bug of the version I am using, 
or am I misunderstanding something here? After all, simply writing

g1 : Set
g1 = if[Set*] true then Bool else ℕ
g2 : Set
g2 = if true then Bool else ℕ

seems to work totally fine.


Thank you,
K.


PS: A couple of optional noob questions, once I'm at it:
* Is it possible to somehow verify that g1 == g2 in the last code snippet above?
* Is there a possibility to do pattern-matching on type expressions in Agda?
(e.g.
  f: (t = true) → ...
  f: (t = false) → ...)