polarity-lang / polarity

A Language with Dependent Data and Codata Types
https://polarity-lang.github.io
Apache License 2.0
57 stars 2 forks source link

Cannot typecheck file which wants to normalize definition from imported module. #345

Closed BinderDavid closed 1 week ago

BinderDavid commented 2 weeks ago

Counterexample:

If we change the boolrep.pol example to the following example:

use "../std/data/bool.pol"

data BoolRep(x: Bool) {
    TrueRep: BoolRep(T),
    FalseRep: BoolRep(F),
}

def BoolRep(x).extract(x: Bool): Bool {
    TrueRep => T,
    FalseRep => F,
}

data Top { Unit }

def Top.flipRep(x: Bool, rep: BoolRep(x)): BoolRep(x.neg) {
    Unit => rep.match {
        TrueRep => FalseRep,
        FalseRep => TrueRep,
    }
}

def Top.example: Bool {
    Unit => Unit.flipRep(T, TrueRep).extract(F)
}

then we cannot normalize the occurrance of x.neg in the definition of flipRep.

BinderDavid commented 2 weeks ago

Depends on #334