Panic in elaborator

[timsueberkrueb]

The following example panics:

codata Fun(a b: Type) {
    Fun(a,b).ap(a b: Type, x: a) : b
}

let bar(f: Fun(?, ?)): f.ap(?, ?, ?) {
    ?
}

Rust backtrace:

Error:   × Main thread panicked.
  ├─▶ at lang/ast/src/ctx/def.rs:39:19
  ╰─▶ attempt to subtract with overflow
         0: 0x5e702840c427 - rust_begin_unwind
                      at /rustc/051478957371ee0084a7c0913941d2a8c4757bb9/library/std/src/panicking.rs:652
         1: 0x5e7027619c13 - core::panicking::panic_fmt::h319840fcbcd912ef
                      at /rustc/051478957371ee0084a7c0913941d2a8c4757bb9/library/core/src/panicking.rs:72
         2: 0x5e702761a4f7 - core::panicking::panic_const::panic_const_sub_overflow::h3ac2048727405c68
                      at /rustc/051478957371ee0084a7c0913941d2a8c4757bb9/library/core/src/
      panicking.rs:179
         3: 0x5e702820c46b - ast::ctx::def::GenericCtx<T>::idx_to_lvl::h04636bf7e40c2c49
                      at /home/tim/Dev/polarity-lang/polarity/lang/ast/src/ctx/def.rs:39
         4: 0x5e70281f9bb9 - <ast::exp::Variable as
      ast::traits::subst::Substitutable>::subst::h6e5ac777e5845879
                      at /home/tim/Dev/polarity-lang/polarity/lang/ast/src/exp.rs:391
         5: 0x5e70281f96e5 - <ast::exp::Exp as
      ast::traits::subst::Substitutable>::subst::h9d0d7c235f990b60
                      at /home/tim/Dev/polarity-lang/polarity/lang/ast/src/exp.rs:260
         6: 0x5e70281eea66 - <alloc::boxed::Box<T> as
      ast::traits::subst::Substitutable>::subst::h00a45fc3c5a2631a
                      at /home/tim/Dev/polarity-lang/polarity/lang/ast/src/traits/subst.rs:92
         7: 0x5e702822cbb6 - <alloc::vec::Vec<T> as ast::traits::subst::Substitutable>::subst::
      {{closure}}::h9f9f0b807e7aa34b
                      at /home/tim/Dev/polarity-lang/polarity/lang/ast/src/traits/subst.rs:85
         8: 0x5e702820b405 - core::iter::adapters::map::map_fold::{{closure}}::hc36bf52e0804e7fa
                      at /rustc/051478957371ee0084a7c0913941d2a8c4757bb9/library/core/src/iter/adapters/
      map.rs:89
         9: 0x5e70282258a9 - <core::slice::iter::Iter<T> as
      core::iter::traits::iterator::Iterator>::fold::h4ed46b5467bed57f
                      at /rustc/051478957371ee0084a7c0913941d2a8c4757bb9/library/core/src/slice/iter/
      macros.rs:230
        10: 0x5e7028209d72 - <core::iter::adapters::map::Map<I,F> as
      core::iter::traits::iterator::Iterator>::fold::h4f1aed2f53c149ff
                      at /rustc/051478957371ee0084a7c0913941d2a8c4757bb9/library/core/src/iter/adapters/
      map.rs:129
        11: 0x5e702820ac46 - core::iter::traits::iterator::Iterator::for_each::h5a8121631cdadb8d
                      at /rustc/051478957371ee0084a7c0913941d2a8c4757bb9/library/core/src/iter/traits/
      iterator.rs:818
        12: 0x5e70281e91af - alloc::vec::Vec<T,A>::extend_trusted::hcd353fa81762b703
                      at /rustc/051478957371ee0084a7c0913941d2a8c4757bb9/library/alloc/src/vec/
      mod.rs:3096
        13: 0x5e70281ece7b - <alloc::vec::Vec<T,A> as
      alloc::vec::spec_extend::SpecExtend<T,I>>::spec_extend::ha5143ffdac6f5b8f
                      at /rustc/051478957371ee0084a7c0913941d2a8c4757bb9/library/alloc/src/vec/
      spec_extend.rs:26
        14: 0x5e70281e5c94 - <alloc::vec::Vec<T> as
      alloc::vec::spec_from_iter_nested::SpecFromIterNested<T,I>>::from_iter::hc0f0baf465720f18
                      at /rustc/051478957371ee0084a7c0913941d2a8c4757bb9/library/alloc/src/vec/
      spec_from_iter_nested.rs:62
        15: 0x5e70281ecffe - <alloc::vec::Vec<T> as
      alloc::vec::spec_from_iter::SpecFromIter<T,I>>::from_iter::hd248b48396c848f2
                      at /rustc/051478957371ee0084a7c0913941d2a8c4757bb9/library/alloc/src/vec/
      spec_from_iter.rs:33
        16: 0x5e70281ecc59 - <alloc::vec::Vec<T> as
      core::iter::traits::collect::FromIterator<T>>::from_iter::h951deb0f369f737d
                      at /rustc/051478957371ee0084a7c0913941d2a8c4757bb9/library/alloc/src/vec/
      mod.rs:2970
        17: 0x5e702820aa6e - core::iter::traits::iterator::Iterator::collect::h56e68c0a6398872d
                      at /rustc/051478957371ee0084a7c0913941d2a8c4757bb9/library/core/src/iter/traits/
      iterator.rs:2005
        18: 0x5e70281ed6fe - <alloc::vec::Vec<T> as
      ast::traits::subst::Substitutable>::subst::h55a7fa3e1a8242ff
                      at /home/tim/Dev/polarity-lang/polarity/lang/ast/src/traits/subst.rs:85
        19: 0x5e702822cbf0 - <alloc::vec::Vec<T> as ast::traits::subst::Substitutable>::subst::
      {{closure}}::ha8b18a8912e649ce
                      at /home/tim/Dev/polarity-lang/polarity/lang/ast/src/traits/subst.rs:85
        20: 0x5e702820b380 - core::iter::adapters::map::map_fold::{{closure}}::h8f99a58fc37ab58e
                      at /rustc/051478957371ee0084a7c0913941d2a8c4757bb9/library/core/src/iter/adapters/
      map.rs:89
        21: 0x5e70282267ad - <core::slice::iter::Iter<T> as
      core::iter::traits::iterator::Iterator>::fold::hf85da0dd99da729f
                      at /rustc/051478957371ee0084a7c0913941d2a8c4757bb9/library/core/src/slice/iter/
      macros.rs:230
        22: 0x5e7028209fc2 - <core::iter::adapters::map::Map<I,F> as
      core::iter::traits::iterator::Iterator>::fold::hd8277e9aff9a0469
                      at /rustc/051478957371ee0084a7c0913941d2a8c4757bb9/library/core/src/iter/adapters/
      map.rs:129
        23: 0x5e702820acd6 - core::iter::traits::iterator::Iterator::for_each::heef308818d4a7065
                      at /rustc/051478957371ee0084a7c0913941d2a8c4757bb9/library/core/src/iter/traits/
      iterator.rs:818
        24: 0x5e70281e7bff - alloc::vec::Vec<T,A>::extend_trusted::h0017e2e2e3fe23bc
                      at /rustc/051478957371ee0084a7c0913941d2a8c4757bb9/library/alloc/src/vec/
      mod.rs:3096
        25: 0x5e70281eceab - <alloc::vec::Vec<T,A> as
      alloc::vec::spec_extend::SpecExtend<T,I>>::spec_extend::hbfef22b9d5bf8ce3
                      at /rustc/051478957371ee0084a7c0913941d2a8c4757bb9/library/alloc/src/vec/
      spec_extend.rs:26
        26: 0x5e70281e6274 - <alloc::vec::Vec<T> as
      alloc::vec::spec_from_iter_nested::SpecFromIterNested<T,I>>::from_iter::hcd58a4748342fed7
                      at /rustc/051478957371ee0084a7c0913941d2a8c4757bb9/library/alloc/src/vec/
      spec_from_iter_nested.rs:62
        27: 0x5e70281ecfbe - <alloc::vec::Vec<T> as
      alloc::vec::spec_from_iter::SpecFromIter<T,I>>::from_iter::h91a5f265b19845fc
                      at /rustc/051478957371ee0084a7c0913941d2a8c4757bb9/library/alloc/src/vec/
      spec_from_iter.rs:33
        28: 0x5e70281ecd29 - <alloc::vec::Vec<T> as
      core::iter::traits::collect::FromIterator<T>>::from_iter::hbddb99199fdd0c32
                      at /rustc/051478957371ee0084a7c0913941d2a8c4757bb9/library/alloc/src/vec/
      mod.rs:2970
        29: 0x5e702820a9fe - core::iter::traits::iterator::Iterator::collect::h26e77a07ec7bbb79
                      at /rustc/051478957371ee0084a7c0913941d2a8c4757bb9/library/core/src/iter/traits/
      iterator.rs:2005
        30: 0x5e70281ed77e - <alloc::vec::Vec<T> as
      ast::traits::subst::Substitutable>::subst::ha90877d35770cecc
                      at /home/tim/Dev/polarity-lang/polarity/lang/ast/src/traits/subst.rs:85
        31: 0x5e70281fc1fa - <ast::exp::Hole as
      ast::traits::subst::Substitutable>::subst::hd82ddb35a1d816d0
                      at /home/tim/Dev/polarity-lang/polarity/lang/ast/src/exp.rs:1343
        32: 0x5e70281f991e - <ast::exp::Exp as
      ast::traits::subst::Substitutable>::subst::h9d0d7c235f990b60
                      at /home/tim/Dev/polarity-lang/polarity/lang/ast/src/exp.rs:268
        33: 0x5e70281eea66 - <alloc::boxed::Box<T> as
      ast::traits::subst::Substitutable>::subst::h00a45fc3c5a2631a
                      at /home/tim/Dev/polarity-lang/polarity/lang/ast/src/traits/subst.rs:92
        34: 0x5e70281eeafc - <T as ast::traits::subst::SubstUnderCtx>::subst_under_ctx::h3f2b6ca8426a9ecb
                      at /home/tim/Dev/polarity-lang/polarity/lang/ast/src/traits/subst.rs:164
        35: 0x5e70282150d4 - <ast::exp::Hole as ast::traits::zonk::Zonk>::zonk::h4c80aadea3d69ccb
                      at /home/tim/Dev/polarity-lang/polarity/lang/ast/src/exp.rs:1413
        36: 0x5e7028210f5e - <ast::exp::Exp as ast::traits::zonk::Zonk>::zonk::hae9dc3452a39b089
                      at /home/tim/Dev/polarity-lang/polarity/lang/ast/src/exp.rs:308
        37: 0x5e70281eeb7b - <alloc::boxed::Box<T> as ast::traits::zonk::Zonk>::zonk::h3f67b78b397df559
                      at /home/tim/Dev/polarity-lang/polarity/lang/ast/src/traits/zonk.rs:21
        38: 0x5e70282104fe - <ast::exp::Arg as ast::traits::zonk::Zonk>::zonk::h47194512a2c3f423
                      at /home/tim/Dev/polarity-lang/polarity/lang/ast/src/exp.rs:148
        39: 0x5e70282167dc - <ast::exp::Args as ast::traits::zonk::Zonk>::zonk::h1918517fc9c225cf
                      at /home/tim/Dev/polarity-lang/polarity/lang/ast/src/exp.rs:1750
        40: 0x5e7028211c3f - <ast::exp::TypCtor as ast::traits::zonk::Zonk>::zonk::h5e211dd2f1214fdb
                      at /home/tim/Dev/polarity-lang/polarity/lang/ast/src/exp.rs:540
        41: 0x5e7028210e57 - <ast::exp::Exp as ast::traits::zonk::Zonk>::zonk::hae9dc3452a39b089
                      at /home/tim/Dev/polarity-lang/polarity/lang/ast/src/exp.rs:301
        42: 0x5e70281eeb7b - <alloc::boxed::Box<T> as ast::traits::zonk::Zonk>::zonk::h3f67b78b397df559
                      at /home/tim/Dev/polarity-lang/polarity/lang/ast/src/traits/zonk.rs:21
        43: 0x5e70282215af - <ast::decls::Param as ast::traits::zonk::Zonk>::zonk::h09ffd177e63d2f88
                      at /home/tim/Dev/polarity-lang/polarity/lang/ast/src/decls.rs:1225
        44: 0x5e70282210c9 - <ast::decls::Telescope as ast::traits::zonk::Zonk>::zonk::h35ef5a73df00d528
                      at /home/tim/Dev/polarity-lang/polarity/lang/ast/src/decls.rs:1057
        45: 0x5e702821fa4c - <ast::decls::Let as ast::traits::zonk::Zonk>::zonk::hbde07b17d2084b58
                      at /home/tim/Dev/polarity-lang/polarity/lang/ast/src/decls.rs:865
        46: 0x5e702821b53c - <ast::decls::Decl as ast::traits::zonk::Zonk>::zonk::hd245fcfbedc517d2
                      at /home/tim/Dev/polarity-lang/polarity/lang/ast/src/decls.rs:413
        47: 0x5e7027fb0a19 - <alloc::vec::Vec<T> as ast::traits::zonk::Zonk>::zonk::h081f05fb73f73df7
                      at /home/tim/Dev/polarity-lang/polarity/lang/ast/src/traits/zonk.rs:28
        48: 0x5e7027fe38bb - elaborator::typechecker::decls::check_with_lookup_table::hf759bcb4f7b846ef
                      at /home/tim/Dev/polarity-lang/polarity/lang/elaborator/src/typechecker/decls/
      mod.rs:30
        49: 0x5e7027b32226 - driver::database::Database::recompute_ast::h931a3378e1e6db17
                      at /home/tim/Dev/polarity-lang/polarity/lang/driver/src/database.rs:229
        50: 0x5e7027b31841 - driver::database::Database::ast::ha74b6b9664a231cb
                      at /home/tim/Dev/polarity-lang/polarity/lang/driver/src/database.rs:210
        51: 0x5e70278ad9a4 - pol::cli::format::exec::hb2b82ca7d7c637a7
                      at /home/tim/Dev/polarity-lang/polarity/app/src/cli/format.rs:53
        52: 0x5e702768b524 - pol::cli::exec::hfb9a6f8bc3f7861a
                      at /home/tim/Dev/polarity-lang/polarity/app/src/cli/mod.rs:32
        53: 0x5e7027929fbc - pol::main::hbbb4f0354cacb635
                      at /home/tim/Dev/polarity-lang/polarity/app/src/main.rs:9
        54: 0x5e702778401b - core::ops::function::FnOnce::call_once::h6645865137313491
                      at /rustc/051478957371ee0084a7c0913941d2a8c4757bb9/library/core/src/ops/
      function.rs:250
  help: set the `RUST_BACKTRACE=1` environment variable to display a backtrace.

Polarity elaboration trace:

Recomputing ast for: file:///home/tim/Dev/polarity-lang/polarity/examples/foo.pol
Recomputing dependencies for: file:///home/tim/Dev/polarity-lang/polarity/examples/foo.pol
Recomputing source for: file:///home/tim/Dev/polarity-lang/polarity/examples/foo.pol
Recomputing cst for: file:///home/tim/Dev/polarity-lang/polarity/examples/foo.pol
Found source in cache: file:///home/tim/Dev/polarity-lang/polarity/examples/foo.pol
Found dependencies in cache: file:///home/tim/Dev/polarity-lang/polarity/examples/foo.pol
Recomputing type info table for: file:///home/tim/Dev/polarity-lang/polarity/examples/foo.pol
Recomputing ust for: file:///home/tim/Dev/polarity-lang/polarity/examples/foo.pol
Found cst in cache: file:///home/tim/Dev/polarity-lang/polarity/examples/foo.pol
Found dependencies in cache: file:///home/tim/Dev/polarity-lang/polarity/examples/foo.pol
Recomputing symbol table for: file:///home/tim/Dev/polarity-lang/polarity/examples/foo.pol
Found cst in cache: file:///home/tim/Dev/polarity-lang/polarity/examples/foo.pol
Lowering codata declaration: Fun
Lowering destructor: Ident { span: Span { start: ByteIndex(37), end: ByteIndex(39) }, id: "ap" }
Lowering top-level let: bar
Created fresh metavariable: 0 in context: [[]]
Created fresh metavariable: 1 in context: [[]]
Created fresh metavariable: 2 in context: [[()]]
Created fresh metavariable: 3 in context: [[()]]
Created fresh metavariable: 4 in context: [[()]]
Created fresh metavariable: 5 in context: [[()]]
Found ust in cache: file:///home/tim/Dev/polarity-lang/polarity/examples/foo.pol
Checking module: file:///home/tim/Dev/polarity-lang/polarity/examples/foo.pol
Checking well-formedness of codata type: Fun
[[]] |- Type <= Type
Type =? Type
[[]] |- Type ▷ Type
↓Type ~> Type
[[Type]] |- Type <= Type
Type =? Type
[[[email protected]]] |- Type ▷ Type
↓Type ~> Type
Checking well-formedness of destructor: ap
[[]] |- Type <= Type
Type =? Type
[[]] |- Type ▷ Type
↓Type ~> Type
[[Type]] |- Type <= Type
Type =? Type
[[[email protected]]] |- Type ▷ Type
↓Type ~> Type
[[Type,Type]] |- [email protected] <= Type
Type =? Type
[[[email protected],[email protected]]] |- a ▷ [email protected]
↓[email protected] ~> [email protected]
[[[email protected],[email protected],[email protected]]] |- a ▷ [email protected]
[[[email protected],[email protected],[email protected]]] |- b ▷ [email protected]
[[[email protected],[email protected],[email protected]]] |- a -> b ▷ Fun(([email protected], [email protected]))
↓[email protected] ~> [email protected]
↓[email protected] ~> [email protected]
↓Fun(([email protected], [email protected])) ~> [email protected] -> [email protected]
[[[email protected],[email protected],[email protected]]] |- Type ▷ Type
↓Type ~> Type
[[Type,Type,[email protected]]] |- [email protected] <= Type
Type =? Type
[[[email protected],[email protected],[email protected]]] |- Type ▷ Type
↓Type ~> Type
[[Type,Type,[email protected]]] |- [email protected] <= Type
Type =? Type
[[Type,Type,[email protected]],[[email protected] -> [email protected]]] |- [email protected] => Type
Checking well-formedness of global let: bar
[[]] |- ?0 -> ?1 <= Type
[[]] |- Type ▷ Type
↓Type ~> Type
[[]] |- ?0 <= Type
[[]] |- Type ▷ Type
↓Type ~> Type
[[]] |- ?1 <= Type
Type =? Type
[[]] |- ? ▷ ?
[[]] |- ? ▷ ?
[[]] |- ? -> ? ▷ Fun((?, ?))
↓?0 ~> ?0
↓?1 ~> ?1
↓Fun((?0, ?1)) ~> ?0 -> ?1
[[[email protected]]] |- Type ▷ Type
↓Type ~> Type
[[?0 -> ?1]] |- ?2 <= Type
[[?0 -> ?1]] |- [email protected] => ?0 -> ?1
[[[email protected]]] |- Type ▷ Type
↓Type ~> Type
[[?0 -> ?1]] |- ?3 <= Type
[[?0 -> ?1]] |- [email protected] => ?0 -> ?1
[[[email protected]]] |- f ▷ [email protected]
[[[email protected]]] |- ? ▷ ?
↓[email protected] ~> [email protected]
↓?2 ~> ?2
[[?0 -> ?1]] |- ?4 <= ?2
[[?0 -> ?1]] |- [email protected] => ?0 -> ?1
[[[email protected]]] |- f ▷ [email protected]
[[[email protected]]] |- ? ▷ ?
[[[email protected]]] |- f ▷ [email protected]
[[[email protected]]] |- ? ▷ ?
[[[email protected]]] |- ? -> ? ▷ Fun((?, ?))
↓[email protected] ~> [email protected]
↓?2 ~> ?2
↓[email protected] ~> [email protected]
↓?3 ~> ?3
↓Fun((?2, ?3)) ~> ?2 -> ?3
[[?0 -> ?1]] |- [email protected] <= ?2 -> ?3
?0 -> ?1 =? ?2 -> ?3
Solved metavariable: 1 with solution: ?3
Solved metavariable: 0 with solution: ?2
[[[email protected]]] |- f ▷ [email protected]
[[[email protected]]] |- ? ▷ ?
↓[email protected] ~> [email protected]
↓?3 ~> ?3
[[?0 -> ?1]] |- [email protected](?2, ?3, ?4) => ?3
[[[email protected]]] |- f ▷ [email protected]
[[[email protected]]] |- f ▷ [email protected]
[[[email protected]]] |- ? ▷ ?
[[[email protected]]] |- f ▷ [email protected]
[[[email protected]]] |- ? ▷ ?
[[[email protected]]] |- f ▷ [email protected]
[[[email protected]]] |- ? ▷ ?
[[[email protected]]] |- f.ap(?, ?, ?) ▷ [email protected]((?, ?, ?))
↓[email protected] ~> [email protected]
↓?2 ~> ?2
↓[email protected] ~> [email protected]
↓?3 ~> ?3
↓[email protected] ~> [email protected]
↓?4 ~> ?4
↓[email protected]((?2, ?3, ?4)) ~> [email protected](?2, ?3, ?4)
[[?0 -> ?1]] |- ?5 <= [email protected](?2, ?3, ?4)
[[?0 -> ?1]] |- [email protected] => ?0 -> ?1

[timsueberkrueb]

The core of the problem is that unification violates the binding structure.
To explain this, let's annotate the metavars in the example:

let bar(f: Fun(?0, ?1)): f.ap(?2, ?3, ?4) {
    ?
}

Unification correctly equates ?0 = ?2. However, it tries to zonk ?0 := ?2 which is the wrong way around: ?0 is defined under the empty context, but ?2 is defined under [f: Fun(?0, ?2)].

[MangoIV]

codata Fun(a: Type, b: Type) {
    Fun(a, b).ap(a: Type, b: Type, x: a) : b
}

codef Id(a: Type): Fun(a, ?) {
    .ap(a, b, x) => x
}

this is another reproducer I stumbled over, don't know if it is useful, I haven't looked at the problem, sorry if it isn't.