Use named instances for other instances

Question

I'm trying to make a Semigroup and VerifiedSemigroup instance on my custom Bool datatype both on operator && and operator ||:

%case data Lógico = Cierto | Falso

(&&) : Lógico -> Lógico -> Lógico
(&&) Cierto Cierto = Cierto
(&&) _ _ = Falso

(||) : Lógico -> Lógico -> Lógico
(||) Falso Falso = Falso
(||) _ _ = Cierto

So I first make a named instance for Semigroup over the && operator:

-- Todos
instance [TodosSemigroup] Semigroup Lógico where
    (<+>) a b = a && b

But when making the VerifiedSemigroup instance, how do I tell Idris to use the TodosSemigroup instance of Lógico?

instance [TodosVerifiedSemigroup] VerifiedSemigroup Lógico where
    semigroupOpIsAssociative l c r = ?vsemigroupTodos

That code gives me the following error:

When elaborating type of Prelude.Algebra.Main.TodosVerifiedSemigroup, method semigroupOpIsAssociative: Can't resolve type class Semigroup Lógico

Answer 1

There was a newly introduced mechanism for this with the using keyword:

%case data Lógico = Cierto | Falso

(&&) : Lógico -> Lógico -> Lógico
(&&) Cierto Cierto = Cierto
(&&) _ _ = Falso

(||) : Lógico -> Lógico -> Lógico
(||) Falso Falso = Falso
(||) _ _ = Cierto

instance [TodosSemigroup] Semigroup Lógico where
    (<+>) a b = a && b

instance [TodosVerifiedSemigroup] VerifiedSemigroup Lógico using TodosSemigroup where
    semigroupOpIsAssociative l c r = ?vsemigroupTodos