Type checking times again!

[nicolabotta]

I ran into another example which takes ages to type check. Here's the code

> import Syntax.PreorderReasoning

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

> %default total
> %access public export
> %auto_implicits off


> ||| The sum of n terms of the form 1/(S m) is n/(S m)
> lala : (n : Nat) -> (m : Nat ) -> 
>        sum (replicate n (fromFraction (1, Element (S m) MkPositive))) = fromFraction (n, Element (S m) MkPositive)

> lala Z m =
>   let Sm' = Element (S m) MkPositive in
>   let SZ' = Element 1 MkPositive in
>     ( sum (replicate Z (fromFraction (1, Sm'))) )
>   ={ Refl }=
>     ( sum Nil )
>   ={ Refl }=
>     ( fromFraction (0, SZ') )
>   ={ fromFractionEqLemma (0, SZ') (0, Sm') Refl }=
>     ( fromFraction (0, Sm') )
>   QED

> lala (S n) m =
>   let Sm' = Element (S m) MkPositive in
>   let Sm  = toNat Sm' in
>   let Sn  = S n in 
>     ( sum (replicate (S n) (fromFraction (1, Sm'))) )
>   ={ Refl }=
>     ( sum (fromFraction (1, Sm') :: replicate n (fromFraction (1, Sm'))) )
>   ={ Refl }=
>     ( fromFraction (1, Sm') + sum (replicate n (fromFraction (1, Sm'))) )
>   ={ cong (lala n m) }=
>     ( fromFraction (1, Sm') + fromFraction (n, Sm') )
>   ={ fromFractionLinear (1, Sm') (n, Sm') }=
>     ( fromFraction ((1, Sm') + (n, Sm')) )
>   ={ Refl }=
>     ( fromFraction (1 * Sm + n * Sm, Sm' * Sm') )
>   ={ cong (sym (multDistributesOverPlusLeft 1 n Sm)) }=
>     ( fromFraction ((1 + n) * Sm, Sm' * Sm') )
>   ={ multElimRight (1 + n) Sm' Sm' }=
>     ( fromFraction (1 + n, Sm') )      
>   ={ cong (plusOneSucc n) }=
>     ( fromFraction (Sn, Sm') )
>   QED

On a fresh installation of https://github.com/nicolabotta/SeqDecProbs, you should be able to just do

$ cd SeqDecProbs/frameworks/14-
$ make testTypeCheckingSpeed

On a reasonably fast processor (Xeon E5-2667 v3 8C, 3.2GHz) it should take a few minutes to type check the dependencies of TestTypeCheckingSpeed.lidr and more than ... one hour to (fail to?) type check TestTypeCheckingSpeed.lidr itself!

I am not sure that this problem is an instance of #3199. I have tried to prevent expanding features by a careful use of %freeze directives with no success.

There must be something pathological in the example above. But, generally speaking, I have the impression that type checking proofs of properties of specific Num implementations has become very time consuming lately.

Again, I have not done any systematic attempt at finding out whether this is a regression (as I did for #3209) but I have the impression that type checking times have worsened over the last weeks. I might be wrong, of course.

Any idea how to get back to acceptable type checking times? This having to wait for hours is starting to become a bit annoying!

[nicolabotta]

I can now confirm that the program eventually fails to type check. But it takes about 5 hours (14 hours on my laptop) to do so! What is going on here?

[ahmadsalim]

I think issue is the same as #172 which is that the Idris type checker does complete normalization instead of just to whnf-form. I am unsure if there is a particular satisfying workaround for your current issue.

It would probably take less time if there were less terms in pre-order syntax reasoning, but that affects readability.

[nicolabotta]

I think issue is the same as #172 which is that the Idris type checker does complete normalization instead of just to whnf-form.

You are probably right but there might be something more than #172 (or #3199) at stake here. The facts look like the following: type checking the base case and

> lala (S n) m = ?guga

takes about 2 minutes to succeed. Type checking the base case and

> lala (S n) m = 
>   let Sm' = Element (S m) MkPositive in
>   let Sm  = toNat Sm' in
>   let Sn  = S n in 
>     ( sum (replicate (S n) (fromFraction (1, Sm'))) )
>   ={ ?lala }=
>     ( fromFraction (Sn, Sm') )
>   QED

takes about two minutes to fail. Here, the error message is

Type checking ./TestTypeCheckingSpeed.lidr
TestTypeCheckingSpeed.lidr:35:6:When checking right hand side of lala with expected type
        sum (replicate (S n) (fromFraction (1, Element (S m) MkPositive))) =
        fromFraction (S n, Element (S m) MkPositive)

Can't infer type for {letval115}

suggesting that something strange might be happening. Type checking the base case and

> lala (S n) m = 
>   let Sm' = Element (S m) MkPositive in
>   let Sm  = toNat Sm' in
>   let Sn  = S n in 
>     ( sum (replicate (S n) (fromFraction (1, Sm'))) )
>   ={ Refl }=
>     ( sum (fromFraction (1, Sm') :: replicate n (fromFraction (1, Sm'))) )
>   ={ ?lala }=
>     ( fromFraction (Sn, Sm') )
>   QED

also fails in about two minutes and with the same error message. Even

> lala (S n) m = 
>   let Sm' = Element (S m) MkPositive in
>   let Sm  = toNat Sm' in
>   let Sn  = S n in 
>     ( sum (replicate (S n) (fromFraction (1, Sm'))) )
>   ={ Refl }=
>     ( sum (fromFraction (1, Sm') :: replicate n (fromFraction (1, Sm'))) )
>   ={ Refl }=
>     ( fromFraction (1, Sm') + sum (replicate n (fromFraction (1, Sm'))) )
>   ={ cong (lala n m) }=
>     ( fromFraction (1, Sm') + fromFraction (n, Sm') )
>   ={ ?lala }=
>     ( fromFraction (Sn, Sm') )
>   QED

fails to type check in only about 4 minutes and, again, with the same error message! It is only when one tries to type check the base case with

> lala (S n) m = 
>   let Sm' = Element (S m) MkPositive in
>   let Sm  = toNat Sm' in
>   let Sn  = S n in 
>     ( sum (replicate (S n) (fromFraction (1, Sm'))) )
>   ={ Refl }=
>     ( sum (fromFraction (1, Sm') :: replicate n (fromFraction (1, Sm'))) )
>   ={ Refl }=
>     ( fromFraction (1, Sm') + sum (replicate n (fromFraction (1, Sm'))) )
>   ={ cong (lala n m) }=
>     ( fromFraction (1, Sm') + fromFraction (n, Sm') )
>   ={ fromFractionLinear (1, Sm') (n, Sm') }=
>     ( fromFraction ((1, Sm') + (n, Sm')) )
>   ={ ?lala }=
>     ( fromFraction (Sn, Sm') )
>   QED

that type checking times start to diverge to values of the order of hours. At this point, freezing fromFraction brings type checking times down to about 10 seconds, again, with the above error message. This supports your hypothesis that this issue is just another aspect of #172 or #3199.

However, the base case with

> lala (S n) m = 
>   let Sm' = Element (S m) MkPositive in
>   let Sm  = toNat Sm' in
>   let Sn  = S n in 
>     ( sum (replicate (S n) (fromFraction (1, Sm'))) )
>   ={ Refl }=
>     ( sum (fromFraction (1, Sm') :: replicate n (fromFraction (1, Sm'))) )
>   ={ Refl }=
>     ( fromFraction (1, Sm') + sum (replicate n (fromFraction (1, Sm'))) )
>   ={ cong (lala n m) }=
>     ( fromFraction (1, Sm') + fromFraction (n, Sm') )
>   ={ fromFractionLinear (1, Sm') (n, Sm') }=
>     ( fromFraction ((1, Sm') + (n, Sm')) )
>   ={ ?guga }=
>     ( fromFraction (1 * Sm + n * Sm, Sm' * Sm') )
>   ={ ?lala }=
>     ( fromFraction (Sn, Sm') )
>   QED

fails to type check (again, with frozen fromFraction, in a few seconds) with another suspicious error message:

When checking argument x to function Syntax.PreorderReasoning.Equal.step:
        Type mismatch between
                fromFraction (plus (getWitness (fromFraction (1, Sm')))
                                   (getWitness (fromFraction (n, Sm')))) (Inferred value)
        and
                fromFraction ((1, Sm') + (n, Sm')) (Given value)

        Specifically:
                Type mismatch between
                        plus
                and
                        MkPair

Here, it seems that the type checker is using a wrong version of plus. Thus, it appears that we have to do with problems related with complete normalization but also with possibly erroneous error messages. Any idea what {letval115} means and where the type mismatch between plus and MkPair could come from?

[ahmadsalim]

The {letval155} is machine generated name for the assigned value of one of the let-bindings you have. I am not sure why you get the error message however.

[nicolabotta]

I do not know either but replacing

>   let Sm' = Element (S m) MkPositive in

with

>   let Sm' : PNat = Element (S m) MkPositive in

makes the

Can't infer type for {letval115}

error disappear. We are now left with the second error (and with the problem of understanding why the type of Sm' cannot be inferred).

[nicolabotta]

I think issue is the same as #172 ...

You are probably right! The code

> import Syntax.PreorderReasoning

> import NonNegRational
> import NonNegRationalBasicOperations
> import NonNegRationalBasicProperties
> import NatPositive
> import Fraction
> import FractionNormal
> import FractionPredicates
> import FractionBasicOperations
> import FractionBasicProperties
> import PNat
> import PNatOperations
> import PNatProperties

> %default total
> %access public export
> %auto_implicits off

> %freeze fromFractionLinear
> %freeze fromFraction

> ||| The sum of n terms of the form 1/(S m) is n/(S m)
> lala : (n : Nat) -> (m : Nat ) -> 
>        sum (replicate n (fromFraction (1, Element (S m) MkPositive))) = fromFraction (n, Element (S m) MkPositive)

> lala Z m =
>   let Sm' = Element (S m) MkPositive in
>   let SZ' = Element 1 MkPositive in
>     ( sum (replicate Z (fromFraction (1, Sm'))) )
>   ={ Refl }=
>     ( sum Nil )
>   ={ Refl }=
>     ( fromFraction (0, SZ') )
>   ={ fromFractionEqLemma (0, SZ') (0, Sm') Refl }=
>     ( fromFraction (0, Sm') )
>   QED

> lala (S n) m = 
>   let Sm' : PNat = Element (S m) MkPositive in
>   let Sm  : Nat  = toNat Sm' in
>   let Sn  : Nat  = S n in 
>     ( sum (replicate (S n) (fromFraction (1, Sm'))) )
>   ={ Refl }=
>     ( sum (fromFraction (1, Sm') :: replicate n (fromFraction (1, Sm'))) )
>   ={ Refl }=
>     ( fromFraction (1, Sm') + sum (replicate n (fromFraction (1, Sm'))) )
>   ={ cong {f = \ X => fromFraction (1, Sm') + X} (lala n m) }=
>     ( fromFraction (1, Sm') + fromFraction (n, Sm') )
>   ={ sym (fromFractionLinear (1, Sm') (n, Sm')) }=
>     ( fromFraction ((1, Sm') + (n, Sm')) )
>   ={ cong {f = fromFraction} Refl }=
>     ( fromFraction (1 * Sm + n * Sm, Sm' * Sm') )
>   ={ cong {f = \ X => fromFraction (X, Sm' * Sm')} (sym (multDistributesOverPlusLeft 1 n Sm)) }=
>     ( fromFraction ((1 + n) * Sm, Sm' * Sm') )
>   ={ multElimRight (1 + n) Sm' Sm' }=
>     ( fromFraction (1 + n, Sm') )      
>   ={ cong {f = \ X => fromFraction (X, Sm')} (plusOneSucc n) }=
>     ( fromFraction (Sn, Sm') )
>   QED

type checks in about 20 seconds. But commenting out

> %freeze fromFractionLinear
> %freeze fromFraction

increases the type checking time to hours! It will be interesting to see whether type checking based on whnf-form will make it possible to type in reasonable times and without having to introduce ad-hoc %freeze directives.

[edwinb]

I've been playing around with WHNF, and it's not actually clear to me now that it's always going to be a win in practice. Even here, it would end up having to reduce fromFraction to get at the relevant head, and it's clear from the %freeze that unification can make progress even avoiding that.

I'm reading around what other systems do - there must be a good strategy lurking somewhere.

[nicolabotta]

Thanks Edwin! I am going to post a self-contained example that exhibits a similar behavior. Best, Nicola

[edwinb]

As an update, I have found the cause of recent slow downs, which is to do with partial evaluation doing too much work. I'll aim to fix this later this week, but in the meantime you can probably get much better (compile time) performance with --no-partial-eval

[ahmadsalim]

@edwinb Maybe it's a good time to consider having multiple optimization levels?

[edwinb]

@ahmadsalim we already do, in a sense, but that's nothing to do with the problem here. The partial evaluator does too much work and that is a bug (it's repeating work it's done before), not a failure in setting the right optimisation levels.

[nicolabotta]

@edwinb Hmm ... I do not see improvements with the --no-partial-eval option, my type checking times are:

1. 20s with frozen fromFractionLinear, fromFraction, standard flags
2. 20s with frozen fromFractionLinear, fromFraction, standard flags + --no-partial-eval
3. 31m with no freezing, standard flags
4. 30m with no freezing standard flags + --no-partial-eval

This is with Idris-dev-ff776da which I'm sticking to essentially because of #3405. Is it possible that --no-partial-eval improves the type checking times with more recent Idris versions but not with ff776da?