Missing substitutions in smart motive

[rigille]

Describe the bug

Sometimes the smart motive doesn't make all the substitutions it should and that results in confusing error messages.

To Reproduce

Copy and paste the following snippet:

TestType(b: Bool): Type
  case b {
    true: Nat
    false: String
  }
ComplexType(b: Bool, t: TestType(b)): Type
  case b with t {
    true: Nat
    false: String
  }!
  
Test(b: Bool, t: TestType(b)): ComplexType(b, t)
  case b {
    true: ?a
    false: ?b
  }!

Typechecking it results in a type error

Type mismatch.
- Expected: TestType(b)
- Detected: TestType(b)

Expected behavior

I expected those goals to appear with no type errors:

Goal ?a:
With type: ComplexType(Bool.true,t)
With context:
- b: Bool
- t: TestType(b)
- t: TestType(Bool.true)

Goal ?b:
With type: ComplexType(Bool.false,t)
With context:
- b: Bool
- t: TestType(b)
- t: TestType(Bool.false)

indeed that's what happens if you manually expand the lambda encoding:

Test(b: Bool, t: TestType(b)): ComplexType(b, t)
  b(
    (mb) (mt: TestType(mb)) -> ComplexType(mb, mt),
    (t) ?a,
    (t) ?b
  )(t)

my guess is that the smart motive is just replacing the ocurrences of mb and is forgetting mt. Like this

Test(b: Bool, t: TestType(b)): ComplexType(b, t)
  b(
    (mb) (mt: TestType(mb)) -> ComplexType(mb, t),
    (t) ?a,
    (t) ?b
  )(t)

and that explains the confusing error message.

Environment (please complete the following information):

• Ubuntu 20.04
• kind@1.0.91

[algebraic-dev]

Closed because the repository now only contains the code for the Kind2 language.