Allow more predictable type checking with totality assertions

[nicolabotta]

The program

> %default total
> %auto_implicits off

> Foo : Type
> Bar : Foo -> Type
> foo : (x : Foo) -> Bar x -> Foo
> bar : (x : Foo) -> Bar x -> Foo -> Nat

> Pol : Type
> Pol = (x : Foo) -> Bar x

> val : Foo -> Pol -> Nat
> val = \ x => \ p => let y  = p x in
>                     let x' = foo x y in
>                     assert_total (bar x y x' `plus` val x' p)

> Opt : Pol -> Type
> Opt = \ p => (x : Foo) -> (p' : Pol) -> val x p' `LTE` val x p

> opt : Pol

> prf : Opt opt
> -- prf = \ x => \ p' => ?kika

type checks fine and almost immediately. But uncommenting the last line, type checking aborts after about 30 minutes.

I understand that this is due to the unjustified assert_total in val but still I am not sure that this is the expected behavior.

[edwinb]

I think I would expect this, because you have a non terminating thing that you claim is total, so Idris has decided to trust you and evaluate it further. I guess it's aborting with some kind of fatal error?

[nicolabotta]

Yes, idris --check gets killed by the OS after abot 30 minutes.

I agree that this can happen because of the unjustified assert_total, but I am wandering whether this should happen!

Here, there is no need to use the definition of val to deduce the type of the goal kika.

I have reported the issue because it is yet another facet of the issues that led to #3199: the type checker runs into a trouble because it tries to do more than it is actually needed.

You can see that this is the case by deferring the implementation of val. For instance

> %default total
> %auto_implicits off

> Foo : Type
> Bar : Foo -> Type
> foo : (x : Foo) -> Bar x -> Foo
> bar : (x : Foo) -> Bar x -> Foo -> Nat

> Pol : Type
> Pol = (x : Foo) -> Bar x

> val : Foo -> Pol -> Nat

> Opt : Pol -> Type
> Opt = \ p => (x : Foo) -> (p' : Pol) -> val x p' `LTE` val x p

> opt : Pol

> prf : Opt opt
> prf = \ x => \ p' => ?kika

> val = \ x => \ p => let y  = p x in
>                     let x' = foo x y in
>                     assert_total (bar x y x' `plus` val x' p)

type checks in a breeze and the goal kika is computed correctly.

[ahmadsalim]

@nicolabotta I certainly think that you are right in that this is a greyzone, and I can relate to the unpredictability in behaviour. If it is OK, I will close this as expected behaviour, since it is a result of an assertion and I am unsure whether there is a good way to account for them. If you or Edwin believe that the issue is important, please reopen it.

[nicolabotta]

Ahmad, I believe that the issue should be re-opened. It is true that the behavior is triggered by an unjustified assertion, but this is not the point.

The point here is that the type checker gets stuck in performing operations that are not actually needed to type check the code. This can be demonstarted by deferring the point of definition of val as in my second example.

This is a fundamental deficiency of the type checker which was originally planned to be addressed with 1.0. Some weeks ago Edwin realized that type checking using whnf was not going to be a viable approach, see #3199.

The reported issue is just an instance of #3199 like #3246, #3358 and, I believe, #172!

[ahmadsalim]

As you wish, I have reopened the issue. I unfortunately do not know enough about the intrinsics of the type checker to know how it should optimally be resolved.

[nicolabotta]

@ahmadsalim Thanks Ahmad, I have of course no idea how the issue could be addressed but it seems counterintuitive that a code that type checks for every val : Foo -> Pol -> Nat does not type check for a specific value of val! Perhaps naively, I would expect that type checking is done in stages and that a stage in which definitions are used is only attempted after type checking based on type information alone has failed.