Pattern match failure when using induction without a forall

[roboguy13]

If I go inside the forall of the nil-append lemma from examples/laws/ListLaws.hs and then try to run induction 'xs, I get a pattern match failure:

hermit<0> rule-to-lemma nil-append
nil-append (Not Proven)
  ∀ △ xs. (++) ▲ ([] ▲) xs ≡ xs
hermit<1> prove-lemma nil-append
Goal:
  ∀ △ xs. (++) ▲ ([] ▲) xs ≡ xs
proof<2> forall-body
Goal:
  (++) ▲ ([] ▲) xs ≡ xs
proof<3> induction 'xs
Error in expression: induction 'xs
Pattern match failure in do expression at src/HERMIT/Dictionary/Induction.hs:43:5-16
proof<3> 

[ecaustin]

I'm assuming this is intentional as induction in other logical systems almost always requires that the inductive variable be universally quantified.

I suppose there's an argument to be made for adding the capability to strip away just the universally quantified types before induction (maybe that was your intention here?), but given the current definition of forall-body everything appears to be functioning as intended.

Is that right, @xich?

[roboguy13]

@ecaustin Well, I'm sure that it's intentionally an error, but a pattern match failure along with a source location inside of HERMIT doesn't seem like the most descriptive message. It took me a moment to figure out what the cause was when I ran into it.

I was trying to descend into a type quantifier body, and I accidentally went into the body of the value-level quantifier too. It probably wouldn't have been valid either way since I was led there by a bug in my script, but I did end up at this pattern match failure.

[ecaustin]

Oh. Your "bug" label confused me.

I've added a guard before pattern matching to provide an error message instead of a pattern match failure exception with commit https://github.com/ku-fpg/hermit/commit/522603fe168157c6fd18520678a552bba2f15f82.