Steve Dunham

A little additional information: the last issue posted by buzden, the one by ohad, and #3276 are caused by confusion between types. There is an impossible clause generated with a...

I've updated that branch to handle the `IAlternative` issue by choosing the default alternative, and it resolves the issue. But it breaks frex. One spot in frex appears to be...

There are two different `()`, which confuses discussion a little. For clarity, I may say `MkUnit` for the value `()` and `Unit` for the Type `()`. _Why the unification error...

Yeah, I missed that. In Idris we can often leave a case-alt out if it is not possible. (No valid constructor given the context.) So we can remove all of...

Interestingly, if we use a `Bool` instead of `Maybe String`: ```idris data Foo : Type where NoFoo : Foo MkFoo : (0 _ : Bool) -> Foo data Bar :...

Are on an M1 Mac with the racket Chez scheme? I hit a similar issue and tracked it down to that scheme needing the files loaded in order. We could...

A couple notes from my investigation into the issue: I dropped the `P a =>` to get a different test case. It gives a slightly different unification error. In the...

For me, when running in an x86 Linux VM with insufficient memory, it would die at the last step of building idris. The idris compiler was using a lot of...

I had an idea to do an incremental build on another machine, copy the build tree, have chez rebuild all of the .so files, and do a make install. I've...

I was poking at this issue trying to understand it, and this seems to get further: ```idris ffg : (f : Nat -> Nat) -> (k, n : Nat) ->...