Steve Dunham

The issue here is that we silently ignore `impossible` clauses with `fromInteger` on the left side. So essentially, you can't have numbers in impossible clauses and Idris doesn't tell you...

Idris stumbles when trying to unify `if` statements. This is because the `if` gets turned into a case statement and then lifted to a top level function. Each instance is...

It looks like it also breaks idris2-lsp and katla.

I haven't had time to look more closely, but these tests are failing because of lost documentation: | test | | | - | - | | idris2/warning/warning002 | On...

It is considering the missing impossible because of an internal error while checking it: ``` LOG declare.def.impossible:5: impossible because INTERNAL ERROR: Empty pattern in coverage check ``` Thrown from this...

The application of `id` is required to reproduce this issue. It appears to be exponential in the number of arguments to `bar`. The slowness is happening in totality checking. It...

Yeah, I kind of held off on that patch since it seemed kludgy. I was going to see if there was something more precise I could do to specifically target...

@spcfox - this version handles your examples. Unless I'm missing something, the original code was stripping args on the RHS and falling back to `sizeEq` if the recursion said `Unknown`...

Thanks for taking the time. It looks like [Abel's Foetus paper](https://andreasabel.github.io/foetus-report/) says "Be `x`, `y` variables, `a` a vector of terms (arguments of `y`), `ρ` a relation in {

Yeah, I believe that is the issue I'm trying to fix here, although I might not have explained it as well as you. By not recursing for each prefix, we...