Compile time Nats need to be optimised

[UlfNorell]

Here's half the proof that (==) on nats does the right thing.

eqComplete : (x : Nat) -> (y : Nat) -> so (not (x == y)) -> x = y -> Bool -> _|_
eqComplete Z Z         oh eq   _ impossible
eqComplete Z (S _)     p  refl _ impossible
eqComplete (S _) Z     p  refl _ impossible
eqComplete (S x) (S y) p  eq   True  = eqComplete x y p (sucInj eq) True
eqComplete (S x) (S y) p  eq   False = eqComplete x y p (sucInj eq) False

This takes about 3s:

*slow> eqComplete 1000 1001
eqComplete 1000 1001 : (so True) -> (1000 = 1001) -> Bool -> _|_

This is very strange since eqComplete cannot actually evaluate, as made sured by the spurious Bool argument.

[david-christiansen]

Following discussion on Friday, I'm pretty sure this is due to fromInteger : Integer -> Nat taking time linear to the size of the Nat. Idris also takes quite some time to evaluate the Nat 10000.

Probably the way to fix this is to replace Nats with Integers in the evaluator, but there are some trade-offs regarding complexity of implementation there.

[edwinb]

I've changed the title to reflect the fact that the slowness is no longer mysterious, but we do need to get around to implementing better compile time Nats. I don't like implementing special cases, but as special cases go, this one is particularly special...