Dipendenza funzionale Haskell a b -> c secondo c?

Question

Si consideri il seguente codice Haskell:

{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, 
    FunctionalDependencies #-} 

class C a b c | a b -> c 

instance C (l (i,j)) (r i j) j 
instance C (l i j) (r (i,j)) j 
-- Conflict between the following two lines 
instance C (l (i,j)) (r (i,j)) j 
instance C (l i j) (r i j) j 

Qui, GHC produce un errore di dipendenze funzionali tra le ultime due righe. Se si rilascia una delle ultime due dichiarazioni di istanza, il codice viene compilato. Ho provato un analogo usando famiglie di tipi, che hanno anche prodotto un conflitto. La mia prima domanda è: perché le ultime due righe sono in conflitto, mentre le altre dichiarazioni funzionano tutte insieme?

Inoltre, se cambio l'ultima linea per

instance C (l i j) (r i j) i 

GHC accetta il codice. Questo sembra abbastanza strano, poiché l'unica cosa che cambia è la variabile di tipo dipendente c. Qualcuno può spiegare questo comportamento?

Answer 1

Le ultime due istanze hanno un'unione in conflitto. Mi permetta di utilizzare completamente diversi nomi di variabili:

C (a c (d,e)) (b c (d,e)) e 
vs. 
C (a c (d,e)) (b c (d,e)) (d,e) 

In particolare, il vostro l dalla terza istanza può essere unificato con un tipo di costruzione che ha già un argomento applicata.

Cambiare il j-i fa l'ultimo invece:

C (a c (d,e)) (b c (d,e)) c 

io ancora non capisco perché questo non dà una denuncia. Forse perché è possibile assegnare i tipi tali che c = e, ma non tale che e = (d,e) (che darebbe un tipo infinito che Haskell non consente), ma sembra ancora una cosa dubbiosa da consentire. Forse questo è anche un bug di GHC.

Le altre combinazioni di istanze non sono in conflitto perché quando si tenta di unificarle, si ottengono contraddizioni simili allo e = (d,e) precedente, ma nelle parti non dipendenti, quindi non possono corrispondere.