With-clause doesn't take advantage of ruled out patterns to normalise

[ohad]

I'm not sure this is really a language problem, maybe a feature request? Potentially related to #139. Also, the example below is not realistic (because of the go_figure hole), it's just there to illustrate the problem in a short example.

Steps to Reproduce

Foo.idr

foo : Nat -> Bool
foo n = case compare n Z of
          LT => False
          _  => True
          
foo_true : (n : Nat) -> foo n = True
foo_true  n with (compare n Z)
 foo_true n | LT = ?go_figure  -- That's fine
 foo_true n | _  = ?hole       -- That's not

Expected Behavior

$ idris2 Foo.idr
Foo> :t hole
   n : Nat
-------------------------------------
hole : True = True

Observed Behavior

   n : Nat
-------------------------------------
hole : (case _ of { LT => False ; _ => True }) = True

We can, of course, prove the foo_true lemma (modulo go_figure) by exhausting all the other cases:

foo_true' : (n : Nat) -> foo n = True
foo_true'  n with (compare n Z)
 foo_true' n | LT = ?go_figure' -- That's fine
 foo_true' n | GT = Refl         
 foo_true' n | EQ = Refl

But it would be nicer to follow the same pattern that execution takes.

[edwinb]

This'd be nice, but would require the normaliser to keep track of a lot of information. I think this is a feature request that's very unlikely to get done, unfortunately. I've added a label, just in case anyone is enthusiastic enough to do it, but my feeling is that it'd be very complicated to achieve.

(My feeling on this sort of thing is often wrong though, so who knows...)