Num instances: am I missing something? Idris error?

[nicolabotta]

The program

> module Main
> import NonNegRational
> import NonNegRationalOperations
> import NonNegRationalProperties
> import Fraction
> import PNat
> import PNatOperations
> import NatProperties
> %default total
> zLTs : {m : Nat} -> LT Z (S m)
> zLTs {m} = ltZS m
> x : NonNegRational
> x = fromFraction (7, fromNat 3 zLTs) 
> y : NonNegRational
> y = fromFraction (28, fromNat 8 zLTs)
> z : NonNegRational
> z = x `plus` y
> main : IO ()               
> main = putStrLn $ show z

type checks fine, see https://github.com/nicolabotta/SeqDecProbs/blob/master/frameworks/14-/NonNegRationalTest.lidr

But replacing

> z = x `plus` y

with

> z = x + y

yields

- + Errors (1)
 `-- NonNegRationalTest.lidr line 24 col 2:
     When checking right hand side of z with expected type
             NonNegRational

     Type mismatch between
             PNat (Type of _ + _)
     and
             Subset (Nat, Subset Nat Positive) Normal (Expected type)

     Specifically:
             Type mismatch between
                     Nat
             and
                     (Nat, Subset Nat Positive)

although NonNegRational has been declared to be an instance of Num in the NonNegRationalProperties module (at lines 75-79 of NonNegRationalProperties.lidr) and +, - and fromInteger have been successfully used there.

I have not been able to reproduce this behavior in a simple, self-contained example. Am I missing something obvious here? Is this an Idris error?

[nicolabotta]

What happens is pretty clear: the module PNatOperations defines

> (+) : PNat -> PNat -> PNat
> (+) = plus

The module NonNegRationalProperties registers NonNegRational as an instance of Num but Idris neglects this declaration. Notice that PNat cannot be an instance of Num because there is no canonical way of implementing fromInteger for positive natural numbers. At the same time one wants to be able to define (+) and (*) for PNat: both for convenience, see PNatProperties and FractionOperations, FractionProperties, and because PNat is closed w.r.t. standard addition and multiplication.

My understanding is that this is an Idris error but it is possible that I have not understood how type classes are meant to be used.

[nicolabotta]

I have managed to reproduce the error in a simpler environment: you should be able to download the files in

github.com/nicolabotta/SeqDecProbs/tree/master/issue_reports/num_type_mismatch

and get the error message reported in my first comment by just entering idris NonNegRationalTest.lidr. I think this is an Idris bug. Any idea how to avoid the problem?

[david-christiansen]

Commenting out (+) in PNatOperations.lidr also makes the issue go away. So it seems that it's committing too early to something. This can also be fixed by manually specifying which + is meant, as in:

> z = Classes.(+) x y

So as far as I can see, this should work, but it doesn't. But the workaround of specifying the specific + should let you make progress, anyway.

[nicolabotta]

David Christiansen notifications@github.com wrote:

Commenting out (+) in PNatOperations.lidr also makes the issue go away. So it seems that it's committing too early to something. This can also be fixed by manually specifying which + is meant, as in:

z = Classes.(+) x y

Thanks David! So it appears this is another instance of the name resolution bug with type class member names that has been plaguing us since the beginning of the time!

Is there any hope that this bug will be eradicated once for ever? I have to admit that, in spite of a number of attempts, I have not been able so far to use Idris type classes in a profiecient way for application-level programs. The funny thing is that, if you look at, for instance,

https://github.com/nicolabotta/SeqDecProbs/blob/master/frameworks/14-/FractionProperties.lidr

you will realize that (+) and (*) are perfectly resolved for different instances of Num and as operations of PNat in the same context. For instance, in

||| Addition is commutative plusCommutative : (x : Fraction) -> (y : Fraction) -> x + y = y + x plusCommutative (m, d') (n, e') = let d = toNat d' in let e = toNat e' in ( (m, d') + (n, e') ) ={ Refl }= ( (m * e + n * d, d' * e') ) ={ cong2 (plusCommutative (m * e) (n * d)) (multCommutative d' e') }= ( (n * d + m * e, e' * d') ) ={ Refl }= ( (n, e') + (m, d') ) QED %freeze plusCommutative

Fraction.(+), Nat.(+) and PNat.(+) happily coexist. But then, at the level of Main, the system fails to type check even the simplest expression ...

[nicolabotta]

Commenting out (+) in PNatOperations.lidr also makes the issue go away. So it seems that it's committing too early to something. This can also be fixed by manually specifying which + is meant, ...

David, commenting out (+) in PNatOperations.lidr is not really an option. I would have to comment out (*) as well which is needed in files importing PNatOperations.lidr. Specifying which (+) is meant manually is not an option either. At this point I can as well write z = plus x y or avoid type classes altogether. The question here is why type classes are so brittle and whether they can be made more robust, see also #2505. Best, Nicola

[nicolabotta]

David, Edwin, this is just to confirm that the error is still there in 10.2. You should be able to reproduce the error by downloading the SeqDecProbs repository and doing

$ cd SeqDecProbs-master/issue_reports/num_type_mismatch/
$ make

This should yield

idris +RTS -K32000000 -RTS -p contrib -p effects --warnreach -V NonNegRationalTest.lidr
Type checking ./NatPositive.lidr
Type checking ./PNat.lidr
Type checking ./PNatOperations.lidr
Type checking ./PNatProperties.lidr
Type checking ./Fraction.lidr
Type checking ./FractionOperations.lidr
Type checking ./FractionNormal.lidr
Type checking ./FractionProperties.lidr
Type checking ./NonNegRational.lidr
Type checking ./NonNegRationalOperations.lidr
Type checking ./NonNegRationalProperties.lidr
Type checking ./NonNegRationalTest.lidr
NonNegRationalTest.lidr:25:3:When checking right hand side of z with expected type
        NonNegRational

Type mismatch between
        PNat (Type of _ + _)
and
        Subset (Nat, Subset Nat Positive) Normal (Expected type)

Specifically:
        Type mismatch between
                Nat
        and
                (Nat, Subset Nat Positive)
Holes: Main.z
*NonNegRationalTest>

Replacing

> z = x + y

with

> z = x `plus` y

makes the program type checks fine. It would be great if you could look into this issue because it makes implementations of Num hardly usable in this context. Ciao, Nicola

[nicolabotta]

Also in 0.11-git:1368cb3, the type checker is committing too early to a specific implmentation:

nicola@cirrus:~/github/SeqDecProbs/issue_reports/num_type_mismatch$ idris NonNegRationalTest.lidr 
Type checking ./NatPositive.lidr
Type checking ./PNat.lidr
Type checking ./PNatOperations.lidr
Type checking ./PNatProperties.lidr
Type checking ./Fraction.lidr
Type checking ./FractionOperations.lidr
Type checking ./FractionNormal.lidr
Type checking ./FractionProperties.lidr
Type checking ./NonNegRational.lidr
Type checking ./NonNegRationalOperations.lidr
Type checking ./NonNegRationalProperties.lidr
Type checking ./NonNegRationalTest.lidr
NonNegRationalTest.lidr:25:3:When checking right hand side of z with expected type
        NonNegRational

Type mismatch between
        PNat (Type of _ + _)
and
        Subset (Nat, Subset Nat Positive) Normal (Expected type)

Specifically:
        Type mismatch between
                Nat
        and
                (Nat, Subset Nat Positive)
Holes: Main.z
*NonNegRationalTest>

This is a very annoying bug since it makes overloading Num operations unusable in applications. Is there a chance of getting rid or circumventing this problem? Best, Nicola

[edwinb]

Idris commits early given a choice between a concrete version that works, and a typeclass version which might, because the alternative (checking everything and seeing what works) is unbearably slow in many common contexts (alternative implementations of >>= for example, where the type checker can't immediately reject the Monad version).

This violates the principal that if something type checks, it should be unambiguous. If I can't find an efficient way around it, I'm more inclined to report an error that a name is ambiguous, to be honest...

[edwinb]

Oh, I see, it's committing to something that isn't actually going to work. The type-based pruning of alternatives is being a bit overenthusiastic, so I think I can fix this after all.

There's still a problem to think about when overloaded names and interfaces coincide. But this doesn't seem to be an instance of that problem, at least.

(Edit: perhaps a useful thing would be to warn or even give an error if you attempt to define an overloading that could feasibly clash with an interface method, because then you can decide whether it should be an instance after all.)

[nicolabotta]

Edwin, thanks for looking into this issue again! I am afraid I do not grasp the subtleties behind the problem, I do not see any concrete implementation for

(+) : NonNegRational -> NonNegRational -> NonNegRational

except for the one that should actually be used here. I am sure that there are many implementations of (+) floating around in the context, but it seems to me that there should be only one for NonNegRationals, namely

> ||| NonNegRational is an implementation of Num
> implementation Num NonNegRational where
>   (+) = plus
>   (*) = mult
>   fromInteger = fromNat . fromIntegerNat

from NonNegRationalProperties. Now NonNegRationalProperties.lidr type checks fine and we import this file in NonNegRationalTest. Thus, I would expect

> z = x + y

to type check as fine as if z, x and y were Nats. I am not sure issuing a warning would be a good idea here. In fact, I am not even sure where the warning should be issued. To me it seems that committing to PNatOperations.(+) should not even be considered here and if warnings had to be issued every time an interface method is overloaded we would easily get tons of warnings, I'm afraid ... Ciao, N.

[nicolabotta]

Hmm ... with 0.11-git:951b631 I now get a

- + Errors (1)
 `-- PNatProperties.lidr line 76 col 16:
     When checking right hand side of PNat.multAssociative with expected type
             Element m pm * (Element n pn * Element o po) =
             Element m pm * Element n pn * Element o po

     When checking an application of function PNat.toNatEqLemma:
             Can't disambiguate since no name has a suitable type: 
                     Prelude.Nat.multAssociative, PNat.multAssociative

error when when type checking PNatProperties.lidr. This can be fixed by replacing line 86

>   ={ toNatEqLemma (multAssociative m n o) }=

with

>   ={ toNatEqLemma (Prelude.Nat.multAssociative m n o) }=

Thus, there is a name with a suitable type (and there is only one, I believe). This seems an Idris bug to me. Ciao, Nicola

[nicolabotta]

Ok, so now we are getting massive problems when trying to type check

https://github.com/nicolabotta/SeqDecProbs/blob/master/frameworks/14-/PNatProperties.lidr

but also (after fixing PNatProperties.lidr as in my previous post) when type checking

https://github.com/nicolabotta/SeqDecProbs/blob/master/frameworks/14-/NonNegRationalProperties.lidr:

- + Errors (3)
 |-- NonNegRationalProperties.lidr line 129 col 20:
 |   When checking right hand side of NonNegRationalProperties.plusZeroLeftNeutral with expected type
 |           0 + x = x
 |   
 |   When checking an application of function Syntax.PreorderReasoning.Equal.step:
 |           Can't disambiguate since no name has a suitable type: 
 |                   FractionProperties.plusCommutative, 
 |                   Prelude.Nat.plusCommutative, 
 |                   NonNegRationalProperties.plusCommutative
 |-- NonNegRationalProperties.lidr line 202 col 19:
 |   When checking right hand side of NonNegRationalProperties.multOneLeftNeutral with expected type
 |           1 * x = x
 |   
 |   When checking an application of function Syntax.PreorderReasoning.Equal.step:
 |           Can't disambiguate since no name has a suitable type: 
 |                   FractionProperties.multCommutative, 
 |                   Prelude.Nat.multCommutative, 
 |                   NonNegRationalProperties.multCommutative, 
 |                   PNat.multCommutative
 `-- NonNegRationalProperties.lidr line 233 col 17:
     When checking right hand side of NonNegRationalProperties.multZeroLeftZero with expected type
             0 * x = 0

     When checking an application of function Syntax.PreorderReasoning.Equal.step:
             Can't disambiguate since no name has a suitable type: 
                     FractionProperties.multCommutative, 
                     Prelude.Nat.multCommutative, 
                     NonNegRationalProperties.multCommutative, 
                     PNat.multCommutative

I could probably fix these problems by fully qualifying interface methods as done above but it is clear that we have a problem with overloading here. Best, Nicola

[edwinb]

It's likely that my new pruning code (that I wrote on the train earlier today...) has missed a case that wasn't caught by the tests. Taking a quick look now.

What would be a massive help in general would be some small, self contained, test cases that we could add to the test suite that cover this kind of thing. In this case, perhaps some small files independent of the framework that have proofs with overloaded uses of multCommutative etc.

[edwinb]

I had indeed missed a case in the code that attempts to prune overloadings quickly (this is necessary to make type checking fast enough in the common case) where I forgot that some names can be functions so those overloadings had better not be pruned because we don't know their concrete types yet.

This makes NonNegRationalProperties type check, probably also PNatProperties. I'll push when I've confirmed the tests pass.

In any case, a few self contained test cases that exercise the elaborator on this sort of thing would be an extremely valuable contribution if you have a moment to do that some time... (especially if they are things which have been broken in older versions). It's quite hard for me to extract minimal test cases from this code base since I don't know it so well.

[nicolabotta]

Thanks Edwin, this works fine now! I'd like to contribute to testing but I am not sure how to proceed in practice. Would it be enough to add a few seqDecProbs00* directories unter Idris-dev/test and then send you a pull request? If this is the way to go, I could start right now. Best, Nicola