Test build typecheck fails Haskell pattern match on #4357

[SaraWolffs]

Quoting from #4357 , which changes Prelude.Nat.fromIntegerNat but nothing else:

The appveyor build is failing (travis build as well), but I can't for the life of me see why. Relevant bits of the log:

Type checking .\Prelude\Nat.idr
.
.
.
Type checking .\Data\Bits.idr
Uncaught error: user error (Pattern match failure in do expression at src\Idris\Elab\Transform.hs:32:10-72)

The compiler itself builds just fine. Prelude.Nat still typechecks fine. So do lots of other libraries, and Data.Bits was left untouched, as was all Haskell code. Locally, building with Stack works fine. But when typechecking Data.Bits, the test environment fails a Haskell pattern match.

Looking at Transform.hs, it seems to expect an ElabResult with an empty (that is, []) resultCaseDecls field, which is the only part of the pattern match that looks like it could fail. Since I did add a case block, this seems at least related, but I'm still not sure how this case caused a problem but nothing else did.

Steps to Reproduce

None, continuous integration for PR #4357 demonstrates the issue.

Expected Behavior

Either

• Prelude.Nat failing typecheck
• Some other file failing typecheck in a way traceable to an error in fromIntegerNat
• Tests failing, or
• Everything passing

Observed Behavior

The Idris compiler throws an uncaught Haskell exception while typechecking Data.Bits, citing a Haskell user error, dying without reporting the Idris code it choked on.