Tarski.idr

module Main

%default total


mutual
  data Code : Nat -> Type where
    N : Code n
    Fn : (c : Code n) -> (el c -> Code n) -> Code n
    Ty : (n : Nat) -> Code (S n) 

  el : Code n -> Type
  el N = Nat
  el (Fn a b) = (x : el a) -> (el (b x))
  el {n = S n} Ty = Type 

test : (n : Nat) -> el (Ty n)
test n = Code n

I'm trying to figure out why this compiles in Idris 1. As I see it, we write Type 3 times, so we have 3 level variables i, j, k:

• Code n : Type i on line 7
• el n : Type j on line 12
• el (Ty n) = Type k on line 15

We know that:

• el (Ty n) : Type j, so k < j
• test n = Code n : el (Ty n) = Type k : Type j, so i < j and i <= k
• In the Fn constructor, (c : Code n) -> (el c -> Code n) -> Code n : Type i, so el c : Type i. But then el (Ty n) = Type k : Type i, so k < i

So for constraints, we have k < j, i < j, i <= k and k < i, the latter two of which are contradictory.

What am I misunderstanding? Is a different level variable created for each n in Code, el and test? Or am I wrong that Code n : Type k implies that i <= k?