GADT Typargument für typeclass Auflösung nicht

Question

verwendet werden Betrachten Sie den folgenden Code

data Foo f where 
    Foo :: Foo Int 

class DynFoo t where 
    dynFoo :: Foo f -> Foo t 

instance DynFoo Int where 
    dynFoo Foo = Foo 

obsFoo :: (DynFoo t) => Foo f -> Foo t 
obsFoo = dynFoo 

useDynFoo :: Foo f -> Int 
useDynFoo (obsFoo -> Foo) = 1 

Das Muster Spiel in useDynFoo sollte die Verwendung von obsFoo beschränken haben Typ Foo f -> Foo Int, die es für eine Instanz von DynFoo Int zu suchen führen sollte . Es sucht jedoch stattdessen nach einer Instanz DynFoo t für unbekannte t, und natürlich schlägt fehl.

No instance for (DynFoo t0) arising from a use of ‘obsFoo’ 
    The type variable ‘t0’ is ambiguous 

Wenn ich jedoch die Definition von useDynFoo zu

useDynFoo :: Foo f -> Int 
useDynFoo (obsFoo -> (Foo :: Foo Int)) = 1 

Dann funktioniert es plötzlich ändern, auch wenn meine Art Signatur völlig überflüssig ist.

Warum passiert das und wie kann ich obsFoo verwenden, ohne eine Typ-Signatur geben zu müssen?

Answer 1

Es ist klarer, wenn Sie es schreiben, mit einem expliziten case (Ansicht Muster recht sind verdunkeln WRT Typ-Informationsfluss):

useDynFoo :: Foo f -> Int 
useDynFoo foof = case obsFoo foof of 
    Foo -> 1 

Hier die Informationen f ~ Int sind perfekt erreichbar für die 1. Nun, aber dafür brauchen wir diese Information nicht: wir brauchen sie schon bei obsFoo foof. Und die Information kann nicht dorthin gelangen: GADT-Musterübereinstimmungen wirken als eine vollständige "Typinformationsdiode", d. H. Jegliche Information von außen kann innerhalb des übereinstimmenden Bereichs verwendet werden, aber keine Information von innen kann ohne verwendet werden. (Aus guten Gründen offensichtlich, da diese Informationen nur zur Laufzeit bestätigt werden, wenn Sie tatsächlich haben ein GADT Konstruktor es nehmen aus.)

Die interessantere Frage ist, warum es funktioniert, wenn Sie die :: Foo Int hinzufügen Unterschrift? Nun, das ist insbesondere eine Verrücktheit des Betrachtungsmusters. Siehe die folgenden würde nicht Arbeit:

useDynFoo :: Foo f -> Int 
useDynFoo foof = case obsFoo foof of 
    (Foo :: Foo Int) -> 1 

Diese Informationen, wie Sie selbst gesagt, ist völlig überflüssig.

Allerdings stellt sich heraus, dass diese Ansicht Muster tatsächlich entspricht die Unterschrift auf dem anderen Teil des Gehäuses zu setzen:

useDynFoo :: Foo f -> Int 
useDynFoo foof = case obsFoo foof :: Foo Int of 
    Foo -> 1 

und das ist ein ganz anderes Paar Schuhe, weil jetzt die Foo Int nicht ist innerhalb der GADT-Muster übereinstimmen.

Ich weiß nicht, warum Ansicht Muster mit Unterschriften desugar so, vielleicht um dieses Muster möglich zu machen.

Answer 2

Typensignaturen sind bei Verwendung von GADTs nicht redundant. Beachten Sie den letzten Aufzählungspunkt von GHC Users Guide: GADTs