Instance declaration possibly not total

[nicolabotta]

The skeleton

> import Data.So

> %default total

> data LTE : Double -> Double -> Type where
>   MkLTE : {x : Double} -> {y : Double} -> So (x <= y) -> LTE x y

> NonNegDouble : Type
> NonNegDouble = Subset Double (\ x => 0.0 `LTE` x)

> zero     : NonNegDouble
> one      : NonNegDouble
> toDouble : NonNegDouble -> Double
> plus     : NonNegDouble -> NonNegDouble -> NonNegDouble
> mult     : NonNegDouble -> NonNegDouble -> NonNegDouble
> div      : NonNegDouble -> NonNegDouble -> NonNegDouble
> fromNat  : (n : Nat) -> NonNegDouble

> implementation [NumNonNegDouble] Num NonNegDouble where
>   (+) = plus
>   (*) = mult
>   fromInteger = fromNat . fromIntegerNat

> using implementation NumNonNegDouble
>   ||| NonNegDouble is an implementation of Fractional
>   implementation [FractionalNonNegDouble] Fractional NonNegDouble where
>     (/) = div

> ||| NonNegDouble is an implementation of Eq
> implementation [EqNonNegDouble] Eq NonNegDouble where
>   (==) x y = (toDouble x) == (toDouble y)

> using implementation NumNonNegDouble
>   using implementation EqNonNegDouble
>     ||| NonNegDouble is an implementation of Ord
>     implementation [OrdNonNegDouble] Ord NonNegDouble where
>       compare x y = compare (toDouble x) (toDouble y)

fails to type check with

- + Errors (7)
 |-- ./NonNegDouble/Properties.lidr line 36 col 21:
 |   Main.OrdNonNegDouble is possibly not total due to recursive path Main.OrdNonNegDouble
 |-- ./Prelude/Interfaces.idr line 86 col 4:
 |   Prelude.Interfaces.Main.OrdNonNegDouble, method < is possibly not total due to: Main.OrdNonNegDouble
 |-- ./Prelude/Interfaces.idr line 91 col 4:
 |   Prelude.Interfaces.Main.OrdNonNegDouble, method > is possibly not total due to: Main.OrdNonNegDouble
 |-- ./Prelude/Interfaces.idr line 96 col 4:
 |   Prelude.Interfaces.Main.OrdNonNegDouble, method <= is possibly not total due to: Main.OrdNonNegDouble
 |-- ./Prelude/Interfaces.idr line 99 col 4:
 |   Prelude.Interfaces.Main.OrdNonNegDouble, method >= is possibly not total due to: Main.OrdNonNegDouble
 |-- ./Prelude/Interfaces.idr line 102 col 4:
 |   Prelude.Interfaces.Main.OrdNonNegDouble, method max is possibly not total due to: Main.OrdNonNegDouble
 `-- ./Prelude/Interfaces.idr line 105 col 4:
     Prelude.Interfaces.Main.OrdNonNegDouble, method min is possibly not total due to: Main.OrdNonNegDouble

Is this the expected behavior? Any idea how to avoid the errors?

[ahmadsalim]

@nicolabotta Thank you for reporting, this does indeed seem weird.

[ahmadsalim]

@edwinb Any idea what could cause this?
Is there anything special happening when elaborating named implementations?

[nicolabotta]

Replacing the last block of code with

> using implementation EqNonNegDouble
>   partial
>   implementation [OrdNonNegDouble] Ord NonNegDouble where
>     compare x y = compare (toDouble x) (toDouble y)

makes the program type check but it is not clear to me what it means. What is actually declared to be partial here?

[ahmadsalim]

@nicolabotta It seems that somehow the named implementation itself is seen to be non-total, and I have no idea why.

[melted]

Probably the totality checker can’t see through toDouble. You can always %assert_total if you know better than it.

…

14 nov. 2017 kl. 08:06 skrev nicolabotta ***@***.***>: Replacing the last block of code with > using implementation EqNonNegDouble > partial > implementation [OrdNonNegDouble] Ord NonNegDouble where > compare x y = compare (toDouble x) (toDouble y) makes the program type check but it is not clear to me what it means. What is actually declared to be partial here? — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or mute the thread.

[ahmadsalim]

@melted I have tried replacing it with a hole as well.

[nicolabotta]

@melted Implementing toDouble

> toDouble : NonNegDouble -> Double
> toDouble = getWitness

does not improve things.

[nicolabotta]

@melted

You can always %assert_total if you know better than it.

How to do so?

[ahmadsalim]

%assert_total is getting removed I believe.

assert_total is currently on applicable at expression level, but here it seems that the interface declaration itself is non-total.

[nicolabotta]

@ahmadsalim That's the point, thanks. And, to me, it is not even clear what it means for an interface declaration to be possibly not total!

[ahmadsalim]

@nicolabotta Yes, I believe this is truly a bug. I am just mentioning what the tool says which is that there is some kind of recursive path from the instance declaration to itself, which is to say surprising.

[edwinb]

This may be to do with the fact that instances are elaborated as functions which build a dictionary for the instance, and it relies on some inlining to make sure that recursive calls to methods don't build dictionaries recursively forever. I will take a closer look.

[nicolabotta]

@edwinb Great, thanks! If this issue is fixed, I should be able to move to Idris 1.1.1. For the time being I am stuck with 0.99.

[edwinb]

I'm still looking at why this happens, but here's one thing to note at least - the intended syntax for stating which parent implementations to use for a named instance is:

implementation [OrdNonNegDouble] Ord NonNegDouble using NumNonNegDouble, EqNonNegDouble where
  compare x y = compare (toDouble x) (toDouble y)

This resolves the totality problem. However - the "using implementation" notation should behave in exactly the same way in this context. I will dig further.

[edwinb]

Oh. It turns it it is working exactly the same way, but the totality checker is running at the wrong time because the top level "using implementation" declaration isn't being handled properly. The fix is one line, and on its way...

[nicolabotta]

Thanks Edwin, I will now try to get IdrisLibs to 1.1 and report my findings!

[nicolabotta]

@edwinb I have almost managed to port IdrisLibs to 1.1.2 using named implementations!

The good news is that the port is trivial and requires virtually no modification of the legacy code. One only has to nest the original code in (often nested) using implementation blocks. If you want to see how this looks like in practice, compare for instance

https://gitlab.pik-potsdam.de/botta/IdrisLibs/blob/towards1.1.1/NonNegDouble/Properties.lidr

to

https://gitlab.pik-potsdam.de/botta/IdrisLibs/blob/master/NonNegDouble/Properties.lidr

The new code is obviously not as clean as the original one and the nested using implementationreminds one of the using namespace c++ patterns.

But it's still much better than renouncing to Sigma types altogether, I believe. Anyway, thanks againg for fixing this bug!