HigherOrderCO
Some rules with variables are not being substituted
In some cases where there is more than one rule available for a substitution HVM does not reduce a term even though it should.
Main = @var (Sub var)
(Sub var) = var
(Sub A ) = B
I expect this to evaluate to @var var, but instead this reduction doesn't occur and the result is @var (Sub var).
But removing the second rule,
Main = @var (Sub var)
(Sub var) = var
This now reduces correctly.
If the rules were ordered differently, it would make sense not to reduce since we wouldn't know which path to take. But even in cases where there is no doubt of which rule to take, where i doesn't depend on the value of the variable, this still happens.
Main = @var (Sub var A)
(Sub var A) = var
(Sub B C) = D
As far as I've tested, the problem only happens when a rule matches a parameter to a variable and then another rule of the same group matches the same parameter to a constructor.
This is causing some problems with the Kind2 type-checker and I think is the cause behind https://github.com/Kindelia/Kind2/issues/38
https://github.com/Kindelia/Kind2/issues/38 was not caused by this, but I think this example is:
Rule (a: Nat) (b: Nat): Nat
Rule a Nat.zero = a
Rule Nat.zero (Nat.succ b) = Nat.zero
Q (a: Nat) : Equal (Rule a Nat.zero) a
Q a = Equal.refl
Type mismatch.
- Expected: (Equal _0 (Rule a Nat.zero) a)
- Detected: (Equal _0 (Rule a Nat.zero) (Rule a Nat.zero))
Context:
- a : Nat
On 'test.kind2':
6 | Q a = *Equal.refl*
But,
Rule (a: Nat) (b: Nat): Nat
Rule a Nat.zero = a
Q (a: Nat) : Equal (Rule a Nat.zero) a
Q a = Equal.refl
All terms check.
The problem is that, by adding the second rule, you make the first argument of Rule strict. That means that Rule a Nat.zero is stuck on the first argument, since it is a variable, not a constructor or a number (i.e., it isn't on weak normal form). That is a consequence of the optimal reduction model used by the HVM. Note that Kind2 type-level computations run on the HVM (via normalization-by-evaluation), so, it follows the same evaluation model.
The solution, thus, for theorem proving purposes, is to treat it like any other stuck variable, and un-stuck it by pattern-matching:
Q (a: Nat) : Equal (Rule a Nat.zero) a
Q Nat.zero = Equal.refl
Q (Nat.succ b) = Equal.refl
This completes the proof. The same should apply to any instance where this happens.
