Mehrdeutige Typvariable, die mit Typgleichheitsbeschränkung behoben wird

Question

Ich arbeite an einer monadischen Streaming-Bibliothek und bin in eine Art Sache geraten, die ich nicht verstehe. Ich habe es geschafft, es auf das folgende Beispiel zu reduzieren:

{-# LANGUAGE MultiParamTypeClasses #-} 
{-# LANGUAGE TypeFamilies #-} 

class Foo a b where 
    type E a b :: * 
    (>->) :: a -> b -> E a b 

data Bar x 

instance Foo (Bar x) (Bar x) where 
    type E (Bar x) (Bar x) = Bar x 
    (>->) = undefined 

x = undefined :: Bar a 
y = undefined :: Bar Int 

z = x >-> y 

Wenn ich es zu kompilieren versuchen, erhalte ich:

No instance for (Foo (Bar a0) (Bar Int)) 
    arising from a use of ‘>->’ 
The type variable ‘a0’ is ambiguous 
Relevant bindings include 
    z :: E (Bar a0) (Bar Int) 
    (bound at /usr/local/google/home/itaiz/test/test.hs:17:1) 
Note: there is a potential instance available: 
    instance Foo (Bar x) (Bar x) 
    -- Defined at /usr/local/google/home/itaiz/test/test.hs:10:10 
In the expression: x >-> y 
In an equation for ‘z’: z = x >-> y 

das, glaube ich, überrascht mich ein wenig, aber vielleicht nicht zu viel. Was mich wirklich überrascht, ist, dass, wenn ich die Instanz mit folgendem dann alles ersetzen funktioniert:

instance (x ~ x') => Foo (Bar x) (Bar x') where 
    type E (Bar x) (Bar x') = Bar x 
    (>->) = undefined 

ich nicht den Unterschied zwischen den beiden Instanzdeklarationen sehen. Ich vermute, dass dies etwas damit zu tun hat, wie Typvariablen definiert sind. Kann jemand erklären, was vor sich geht?

[Abgesehen: Ich sehe die gleiche Sache, wenn fundeps stattdessen verwenden.]

Answer 1

bearbeiten: Die GHC user guide section on instance resolution ist ein guter Ort zu starten.

Hier erfahren Sie, wie Sie das Problem lösen können. Ihr z entspricht in etwa folgendermaßen aus:

z :: Bar a -> Bar Int -> E (Bar a) (Bar Int) 
z = (>->) 

Ist es jetzt klarer, warum es nicht möglich ist? Der Fehler, den wir bekommen, ist:

SO26146983.hs:20:5: 
    No instance for (Foo (Bar a) (Bar Int)) arising from a use of `>->' 
    In the expression: (>->) 
    In an equation for `z': z = (>->) 

Es gibt nichts zu zeigen, dass a ~ Int. Lassen Sie uns es umschreiben:

z' :: (a ~ Int) => Bar a -> Bar Int -> E (Bar a) (Bar Int) 
z' = (>->) 

Dies funktioniert auch mit Ihrer ursprünglichen Instanz. (Edit: Ich vermute, der folgende Satz ist entweder nicht hilfreich oder irreführend oder beides.) z' ist (in etwa), wo der Typchecker endet mit Ihrer neu geschriebenen Instanzdefinition: Es sieht eine Instanz für (Bar a) (Bar a'), die (a ~ a') erfordert, und fügt nur diese Einschränkung zum Anruf.

Grob gesagt geht die Instanzauflösung von rechts nach links, mit manchmal unerwarteten Folgen.

Edit: Und das Ergebnis der von rechts nach links Auflösung ist, dass instance (x ~ x') => Foo (Bar x) (Bar x') Streichhölzer alle zwei Typen x und x', ob oder ob nicht x ~ x' tatsächlich der Fall ist. Die Einschränkung wird nur an die Aufrufstelle weitergegeben. Sie können dann keine weitere Instanz für bestimmte Typen schreiben. Es würde sich überschneiden, was standardmäßig verboten ist, und außerdem rückt GHC beim Auflösen von Instanzen nicht zurück. instance Foo (Bar x) (Bar x) auf der anderen Seite wird nicht angewendet, es sei denn, es ist der gleiche Typ an beiden Orten - GHC wird die Nebenbedingung nicht erfinden, weil (x ~ y) => M x y nicht dasselbe ist wie M x x.

Abhängig von Ihrem tatsächlichen Anwendungsfall sollten Sie die Dokumentation für OverlappingInstances lesen. Abhängig davon, was Sie tun, können einige der jüngsten Innovationen in , wie closed type families, relevant sein.