Interface resolution bug

[nickdrozd]

Steps to Reproduce

Stick this code at the bottom of Prelude.idr:

interface Semigroup a => VerifiedSemigroup a where
  semigroupOpIsAssociative : (l, c, r : a) -> l <+> (c <+> r) = (l <+> c) <+> r

interface (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where
  monoidNeutralIsNeutralL : (l : a) -> l <+> Prelude.neutral = l
  monoidNeutralIsNeutralR : (r : a) -> Prelude.neutral <+> r = r

mtimes : Monoid a => (n : Nat) -> a -> a
mtimes Z x = Prelude.neutral
mtimes (S k) x = x <+> mtimes k x

mtimesTimes : VerifiedMonoid a => (x : a) -> (n, m : Nat) ->
  mtimes (n + m) x = mtimes n x <+> mtimes m x
mtimesTimes x Z m = sym $ monoidNeutralIsNeutralR $ mtimes m x
mtimesTimes x (S k) m =
  rewrite mtimesTimes x k m in
    semigroupOpIsAssociative x (mtimes k x) (mtimes m x)

Expected Behavior

No problem

Observed Behavior

mtimesTimes fails with this error:

Prelude.idr:1703:5--1704:1:While processing right hand side of mtimesTimes at Prelude.idr:1701:1--1704:1:
Can't solve constraint between:
	Constraint (Semigroup a) (let 0 _ = \{rwarg:8186} => x <+> rwarg = (x <+> mtimes k x) <+> mtimes m x in let 0 _ = mtimesTimes x k m in Constraint (VerifiedSemigroup a) conArg)
and
	Constraint (Semigroup ty) (Constraint (Monoid a) conArg)

But the proof itself is fine, and it goes through with this change:

-mtimes : Monoid a => (n : Nat) -> a -> a
+mtimes : VerifiedMonoid a => (n : Nat) -> a -> a

mtimes, with the Monoid constraint, says, if you implement those syntactic elements, you get to use this syntactic element. mtimesTimes, with the VerifiedMonoid constraint, says, if you further prove certain guarantees about the behavior of those syntactic elements, you also get some guarantees about the behavior of this new element. So the "verified" constraint shouldn't be necessary for defining mtimes, because mtimes doesn't make any guarantees about behavior.

The inheritance structure looks like this:

Semigroup  -------------->  Monoid

    |	                      |
    |	                      |
    |	                      |
    |	                      |
   \/                        \/

VerifiedSemigroup  ------>  VerifiedMonoid

This bug is in Idris 1 too.

[edwinb]

Diamond shaped inheritance structures are awkward because implementations of the same interface aren't guaranteed to be equal. There's a bit of noise in the error message, but it looks like it doesn't know whether to go to Semigroup via Monoid or VerifiedSemigroup.

So, this code as it stands isn't going to work without some modification. This diamond issue is a pain and I don't know if anyone has found a nice solution for this sort of problem (with proofs) yet.

By the way, I don't think we should use the names VerifiedX any more - having the repeated longer prefix doesn't fit will with tab compleition and I don't find it very helpful visually either. I don't know what they should be called, mind. Maybe MonoidProps?

[nickdrozd]

I'm pretty sure this is what's responsible for blocking the proof at https://github.com/idris-lang/Idris-dev/pull/4848/files#diff-fb2a7c0a9ce133762a38755823a01d7aR73.

By the way, I don't think we should use the names VerifiedX any more - having the repeated longer prefix doesn't fit will with tab compleition and I don't find it very helpful visually either. I don't know what they should be called, mind. Maybe MonoidProps?

MonoidV would be economical in terms of characters, and it also looks decent. GroupV, RingV, etc. I would be happy to implement that change on the Idris 1 side.

[nickdrozd]

This change does not fix the issue, or even affect the error message:

-interface (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where
+interface (Monoid a, VerifiedSemigroup a) => VerifiedMonoid a where

[ghost]

So, this code as it stands isn't going to work without some modification. This diamond issue is a pain and I don't know if anyone has found a nice solution for this sort of problem (with proofs) yet.

@edwinb I'm not sure if this fits the problem, but the comment reminds me of the recent Tabled Typeclass Resolution paper.

[Sventimir]

By the way, I don't think we should use the names VerifiedX any more - having the repeated longer prefix doesn't fit will with tab compleition and I don't find it very helpful visually either. I don't know what they should be called, mind. Maybe MonoidProps?

@nickdrozd once suggested in a dicussion on Idris-dev repo, that these interfaces should actually be merged together (i.e. Semigroup with VerifiedSemigroup and so on). This would solve the problem of naming and remove the diamond-shaped inheritance pattern. In my opinion this is the way to go.