Interface resolution bug

[nickdrozd]

Steps to Reproduce

mtimes' : Monoid a => (n : Nat) -> a -> a
mtimes' Z x = 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)

(with appropriate imports)

Expected Behavior

no problem

Observed Behavior

     When checking right hand side of mtimesTimes with expected type
             mtimes' (S k + m) x = mtimes' (S k) x <+> mtimes' m x

     When checking an application of function rewrite__impl:
             Type mismatch between
                     x <+> (mtimes' k x <+> mtimes' m x) =
                     x <+> mtimes' k x <+>
                     mtimes' m x (Type of semigroupOpIsAssociative x
                                                                   (mtimes' k x)
                                                                   (mtimes' m x))
             and
                     (\replaced =>
                        x <+> replaced =
                        x <+> mtimes' k x <+> mtimes' m x) (mtimes' k x <+>
                                                            mtimes' m
                                                                    x) (Expected type)

             Specifically:
                     Type mismatch between
                             (<+>) {{constructor of Control.Algebra.VerifiedSemigroup#Semigroup a {{constructor of Control.Algebra.VerifiedMonoid#VerifiedSemigroup a}}}}
                                   x
                                   (mtimes' k x) <+>
                             mtimes' m x
                     and
                             (<+>) {{constructor of Prelude.Algebra.Monoid#Semigroup ty {{constructor of Control.Algebra.VerifiedMonoid#Monoid a}}}}
                                   x
                                   (mtimes' k x) <+>
                             mtimes' m x

It looks like the typechecker can't figure out that multiple distinct paths down the inheritance hierarchy end up at the same place.

Fixed with this change, which shouldn't be necessary:

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

Also a bug in Idris 2; see https://github.com/edwinb/Idris2/issues/356