Skip to content

Instantly share code, notes, and snippets.

@JoeyEremondi

JoeyEremondi/Tarski.idr

Last active September 18, 2020 19:35
Show Gist options
  • Save JoeyEremondi/05d25de1df480ff91619868e0784d5da to your computer and use it in GitHub Desktop.
Save JoeyEremondi/05d25de1df480ff91619868e0784d5da to your computer and use it in GitHub Desktop.
Download ZIP
Raw
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
@JoeyEremondi
Copy link
Author

JoeyEremondi commented Sep 18, 2020 •
edited
Loading

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?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment