Bug in lifting

[timsueberkrueb]

-- Embedding of classical logic into intuitionistic logic using double negation

data False {}

codata Not(a: Type) {
    Not(a).ret(a: Type, x: a): False,
}

data DN(a: Type) {
    C1(a: Type): DN(Or(a, Not(a)))
}

def (self: DN(a)).given(a: Type, x: Not(a)): False {
    C1(a') =>
        Unit.contra(Or(a', Not(a')),
                    Right(a',
                          Not(a'),
                          comatch C2 {
                              ret(x', x'') =>
                                  Unit.contra(Or(a', Not(a')), Left(a', Not(a'), x''), x)
                          }),
                    x)
}

data Or(a b: Type) {
    Left(a: Type, b: Type, x: a) : Or(a, b),
    Right(a: Type, b: Type, x: b) : Or(a, b),
}

data Top {
    Unit,
}

def Top.contra(a: Type, prf: a, ref: Not(a)) : False {
    Unit => ref.ret(a, prf)
}

def (self: Top).lem(a: Type): DN(Or(a, Not(a))) {
    Unit => C1(a)
}

cargo run -- lift Not examples/classical_logic.xfn

Error: 
  × Main thread panicked.
  ├─▶ at /home/tim/Dev/MSc/impl/lang/renaming/src/ctx.rs:45:18
  ╰─▶ attempt to subtract with overflow
  help: set the `RUST_BACKTRACE=1` environment variable to display
        a backtrace.

[timsueberkrueb]

Simplified example:

data Bar(a: Type) { }

codata Baz { unit: Top }

data Foo(a: Type) {
    MkFoo(a: Type): Foo(Bar(a)),
}

data Top { Unit }

def Top.ignore(a: Type, x: a): Top {
    Unit => Unit
}

def Top.foo(a: Type, foo: Foo(a)): Baz {
    Unit => foo.match {
        MkFoo(a') => comatch {
            unit => Unit.ignore(Foo(Bar(a')), foo)
        }
    }
}

cargo run -- lift Baz examples/foo.xfn