StrataVerify Panic in Type inference

[yizhou7]

I seem to run into a PANIC during type inferencing when running StrataVerify. Here is a small example Core program that would trigger this bug:

program Core;

datatype Option (a : Type) { None(), Some(val: a) };

datatype MethodSetting () {
  MethodSetting_Cons(LoggingLevel: Option string)
};

datatype Stage () {
  Stage_Cons(MethodSettings: Option (Sequence MethodSetting))
};

function method_ok(ms: MethodSetting): bool {
  (MethodSetting..LoggingLevel(ms) == Some("ERROR"))
  || (MethodSetting..LoggingLevel(ms) == Some("INFO"))
}

function stage_ok(stage: Stage): bool {
  forall i: int ::
    (Stage..MethodSettings(stage) != None()
     && 0 <= i
     && i < Sequence.length(Option..val(Stage..MethodSettings(stage))))
    ==>
    method_ok(Sequence.select(Option..val(Stage..MethodSettings(stage)), i))
}

const s: Stage;
const grouped: Sequence Stage;
axiom Sequence.length(grouped) == 1;
axiom Sequence.select(grouped, 0) == s;

procedure Check() returns ()
{
  assert [check]:
    forall i: int :: (0 <= i && i < Sequence.length(grouped)) ==>
      stage_ok(Sequence.select(grouped, i));
};

Here is the error I am getting:

PANIC at Strata.Elab.inferType Strata.DDM.Elab.Core:988:11: Cannot instantiate type Strata.TypeExprF.bvar { start := { byteIdx := 3018 }, stop := { byteIdx := 3019 } } 2 with args #[Strata.ArgF.op
    { ann := { start := { byteIdx := 0 }, stop := { byteIdx := 0 } },
      name := { dialect := "", name := "" },
      args := #[] },
  Strata.ArgF.expr
    (Strata.ExprF.app
      { start := { byteIdx := 622 }, stop := { byteIdx := 662 } }
      (Strata.ExprF.fvar { start := { byteIdx := 622 }, stop := { byteIdx := 633 } } 5)
      (Strata.ArgF.expr
        (Strata.ExprF.app
          { start := { byteIdx := 634 }, stop := { byteIdx := 661 } }
          (Strata.ExprF.fvar { start := { byteIdx := 634 }, stop := { byteIdx := 655 } } 15)
          (Strata.ArgF.expr (Strata.ExprF.bvar { start := { byteIdx := 656 }, stop := { byteIdx := 661 } } 1))))),
  Strata.ArgF.expr (Strata.ExprF.bvar { start := { byteIdx := 665 }, stop := { byteIdx := 666 } } 0)]
backtrace:
StrataVerify(+0x96cd2de) [0x55d0e06d22de]
StrataVerify(+0x96cd76c) [0x55d0e06d276c]
StrataVerify(+0x120b813) [0x55d0d8210813]
StrataVerify(+0x96dabc2) [0x55d0e06dfbc2]
StrataVerify(+0x120c668) [0x55d0d8211668]
StrataVerify(+0x121a8aa) [0x55d0d821f8aa]
StrataVerify(+0x122213a) [0x55d0d822713a]
StrataVerify(+0x1215854) [0x55d0d821a854]
StrataVerify(+0x121802f) [0x55d0d821d02f]
StrataVerify(+0x96daf59) [0x55d0e06dff59]
StrataVerify(+0x11e07e5) [0x55d0d81e57e5]
StrataVerify(+0x121a52f) [0x55d0d821f52f]
StrataVerify(+0x122213a) [0x55d0d822713a]
StrataVerify(+0x1215854) [0x55d0d821a854]
StrataVerify(+0x1215758) [0x55d0d821a758]
StrataVerify(+0x96db42a) [0x55d0e06e042a]
StrataVerify(+0x11e07e5) [0x55d0d81e57e5]
StrataVerify(+0x12169cf) [0x55d0d821b9cf]
StrataVerify(+0x96daf59) [0x55d0e06dff59]
StrataVerify(+0x11e07e5) [0x55d0d81e57e5]
StrataVerify(+0x121a52f) [0x55d0d821f52f]
StrataVerify(+0x1221b2e) [0x55d0d8226b2e]
StrataVerify(+0x1215854) [0x55d0d821a854]
StrataVerify(+0x1215758) [0x55d0d821a758]
StrataVerify(+0x96db42a) [0x55d0e06e042a]
StrataVerify(+0x11e07e5) [0x55d0d81e57e5]
StrataVerify(+0x12169cf) [0x55d0d821b9cf]
StrataVerify(+0x96daf59) [0x55d0e06dff59]
StrataVerify(+0x11e07e5) [0x55d0d81e57e5]
StrataVerify(+0x121a52f) [0x55d0d821f52f]
StrataVerify(+0x1221b2e) [0x55d0d8226b2e]
StrataVerify(+0x1215854) [0x55d0d821a854]
StrataVerify(+0x122e71e) [0x55d0d823371e]
StrataVerify(+0x122ea36) [0x55d0d8233a36]
StrataVerify(+0x96db512) [0x55d0e06e0512]
StrataVerify(+0x11e07e5) [0x55d0d81e57e5]
StrataVerify(+0x122f4e1) [0x55d0d82344e1]
StrataVerify(+0x1233f7a) [0x55d0d8238f7a]
StrataVerify(+0x96daf59) [0x55d0e06dff59]
StrataVerify(+0x1233369) [0x55d0d8238369]
StrataVerify(+0x1234a17) [0x55d0d8239a17]
StrataVerify(+0x96db10e) [0x55d0e06e010e]
StrataVerify(+0x128e164) [0x55d0d8293164]
StrataVerify(+0x128e7bb) [0x55d0d82937bb]
StrataVerify(+0x129164f) [0x55d0d829664f]
StrataVerify(+0xde316f) [0x55d0d7de816f]
StrataVerify(+0xde95e4) [0x55d0d7dee5e4]
/lib/x86_64-linux-gnu/libc.so.6(+0x29d90) [0x7f628f8d1d90]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x80) [0x7f628f8d1e40]
StrataVerify(+0xdde36a) [0x55d0d7de336a]
Error: /input/test.st:24:14: error: Encountered .|| expression when MethodSetting expected.

Finished with 1 errors.

[MikaelMayer]

🤖 Autopilot started working on this (branch issue-650-strataverify-panic-in-type-inference)