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

Astolat

@dfeuer, I think that the problem is that is not implemented. – Astolat

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

Astolat

Answer 2

There is an open issue at the idris-dev repository. Edwin Brady states that

Currently (by design) named instances can only be used to resolve a class by being named explicitly, even if there is no normal instance.

So here we have Idris trying to resolve the unnamed Semigroup Lógico instance, which is needed in order to define a VerifiedSemigroup Lógico instance.

We need some way to specify, in the instance declaration, that a named instance should be used to satisfy a class constraint. I do not know whether this is possible. Quoting Edwin from the linked issue:

this behaviour isn't documented anywhere

Obscurantism

Well, yes, I know that's the problem. What I need to know is how I can tell the instance of VerifiedSemigroup to use the previously defined Semigroup instance. – Astolat