polarity-lang / polarity

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

Panic in normalizer when checking pathological example #321

Open timsueberkrueb opened 23 hours ago

timsueberkrueb commented 23 hours ago

Consider the following example (note the missing case for C in type:

data Foo {
    A,
    B(y: C(A).type),
    C(x: B(A).type)
}

def Foo.type: Type {
    A => Foo,
    B(_) => Foo,
}

Typechecking fails with the following panic:

Error:   × Main thread panicked.
  ├─▶ at lang/elaborator/src/normalizer/eval.rs:160:91
  ╰─▶ called `Option::unwrap()` on a `None` value
  help: set the `RUST_BACKTRACE=1` environment variable to display a
        backtrace.