używać nazwanych wystąpień do innych przypadkach

Question

Próbuję dokonać Semigroup i VerifiedSemigroup wystąpienie na mój zwyczaj Bool typu danych zarówno od operatora && i operatora ||:

%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 

Więc najpierw dokonać nazwie instancji do Semigroup na operatora &&:

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

Ale kiedy robię instancję VerifiedSemigroup, jak mogę powiedzieć Idrisowi, aby użył instancji TodosSemigroup z Lógico?

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

Ten kod daje mi następujący błąd:

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

Answer 1

Było nowo wprowadzony mechanizm za to ze słowem kluczowym using:

%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 where 
    semigroupOpIsAssociative l c r = ?vsemigroupTodos 

Answer 2

Jest open issue w repozytorium Idris-dev. Edwin Brady twierdzi, że

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

Więc tutaj mamy Idris próbuje rozwiązać ten nienazwany Semigroup Lógico instancji, który jest potrzebny w celu określenia instancji VerifiedSemigroup Lógico.

Potrzebujemy sposobu, aby określić w deklaracji instancji, że nazwana instancja powinna być używana do spełnienia ograniczenia klasy. Nie wiem, czy to możliwe. Cytowanie Edwin z połączonego wydania:

this behaviour isn't documented anywhere