Type checking should use whnf, not normal form

[edwinb]

The following program should type check more or less instantly, but doesn't:

data IsSuc : Nat -> Type where
     YesItIs : IsSuc (S x)

ouch : IsSuc (100 * 100)
ouch = YesItIs

The reason is that the type checker just uses normalisation by evaluation, so needs to produce a normal form for 100 * 100, whereas weak head normal form would be enough and would evaluation to S [stuff] instantly.

I've been meaning to implement this for about 4 years, but have still not got around to it. It really needs doing before version 1.0, however, and should address the underlying problem described in #3198

[nicolabotta]

Consider

> %default total
> %access public export

> data IsSuc : Nat -> Type where
>      YesItIs : {x : Nat} -> IsSuc (S x)

> PNat : Type
> PNat = Subset Nat IsSuc

> fromNat : (m : Nat) -> Z `LT` m -> PNat
> fromNat  Z zLTz = absurd zLTz
> fromNat (S m) _ = Element (S m) (YesItIs {x = m})

> x : PNat
> x = Element (S 12748) (YesItIs {x = 12748})
> -- x = fromNat (S 12748) (LTESucc LTEZero)

Here x = Element (S 12748) (YesItIs {x = 12748}) type checks almost instantaneously while it takes ages to type check x = fromNat (S 12748) (LTESucc LTEZero).

Why so? Here I would have expected fromNat (S 12748) (LTESucc LTEZero) to reduce to
Element (S 12748) (YesItIs {x = 12748}) and both implementations of x to take about the same time to type check.

[nicolabotta]

Although this is not a self-contained example, I am adding it here to further illustrate the potential consequences of the issue pointed out by Edwin. It is a nice example, I think. We basically want to show that 1/8 = 3/24. Here it goes:

> module Main

> import NonNegRational
> import NonNegRationalBasicOperations
> import NonNegRationalBasicProperties
> import Fraction
> import FractionPredicates
> import PNat
> import PNatOperations
> import PNatProperties
> import NatPositive

> %default total
> %auto_implicits off

> dz1 : PNat
> dz1 = Element (S 7) (MkPositive {n = 7})
> f1  : Fraction
> f1  = (1, dz1)
> z1  : NonNegRational
> z1  = fromFraction f1

> dz2 : PNat
> dz2 = Element (S 23) (MkPositive {n = 23})
> f2  : Fraction
> f2  = (3, dz2)
> z2  : NonNegRational
> z2  = fromFraction f2

> f1Eqf2 : f1 `Eq` f2
> f1Eqf2 = Refl

> %freeze fromFraction

> z1EQz2 : z1 = z2
> z1EQz2 = fromFractionEqLemma f1 f2 f1Eqf2

The program type checks almost instantaneously. But commenting out %freeze fromFraction yields

$ time idris --check TestNonNegRationalEquality.lidr

real    12m52.125s
user    12m27.895s
sys 0m21.393s

on a Intel Xeon E5-2690v3 12c/2.6GHz CPU!

[edwinb]

I'm no longer convinced that this is a good idea, simply because I've tried it and sometimes it leads to horrific slowdowns. I think, unfortunately, a much more drastic rewrite is necessary in order to get better performance from the type checker in cases like this, without spoiling it elsewhere.

Still, I'm leaving this open because we need to deal with this kind of issue. But it's way harder than it seems at first due to some implementation decisions I made years ago that turn out to be bad.

[milessabin]

due to some implementation decisions I made years ago that turn out to be bad.

For posterity, could you say what those bad decisions were and why?