Seltsame Interaktion zwischen Typfamilien und inkohärenten Instanzen

Question

Dieses Codebeispiel wird nicht kompiliert.

{-# LANGUAGE TypeFamilies, FlexibleInstances, UndecidableInstances, ScopedTypeVariables #-} 
module IncoherentBug where 

type family F a where 
    F() = Int 
    F a = a 

class C a where 
    c :: a -> Int 

instance C Int where 
    c y = y 

instance {-# INCOHERENT #-} Monoid a => C a where 
    c _ = 0 

class TwoPossible a where 
    x :: a 

instance a ~() => TwoPossible [a] where 
    x = [] 

instance TwoPossible Bool where 
    x = False 

f :: (F a -> Int) -> [a] ->() 
f _ _ =() 


test = f (\v -> c v) x 

Im Grunde, was hier geschieht, die Unterschrift von f Anfragen ist, dass die Art von x-[()] aufgelöst wird, dann ist die Art von v ist F() die Int ist, und schließlich die erste Instanz von C sollte abgeholt werden. Was passiert stattdessen ist, dass ich einen fehlenden Monoid Int Instanzfehler bekomme.

Der Code kompiliert in Ordnung, wenn ich die INCOHERENT-Instanz in eine OVERLAPPABLE eine ändern. Es funktioniert auch, wenn ich v mit entweder Int oder F() annotate. Es funktioniert auch, wenn ich x (als der Parameter zu f) mit [()] annotate.

Ist das ein Fehler oder missverstand ich etwas hier? ghc-mod meldet den Typ F() für v, auch wenn ich es nicht als solches annotiere. Neben der Tatsache, dass die Fehlermeldung eine Int erwähnt, bedeutet das, dass der Typüberprüfer den richtigen Typ für v herausgefunden hat, aber aus irgendeinem Grund die spezifischere Instanz nicht ausgewählt hat.

Ich sollte auch vielleicht beachten, dass ich GHC 8 verwende. Ich weiß nicht, ob dieses Problem in den früheren Versionen auftritt.

Answer 1

GHC stimmt diesen Code vollständig ab. Sie haben eine C (F a) Beschränkung, die von

f c :: C (F a) => [a] ->() 

entsteht, wenn Sie auf INCOHERENT drehen, GHC wird sofort diese

f c :: Monoid (F a) => [a] ->() 

reduzieren, ohne selbst den Typ des Arguments zu betrachten. Das ist, was Inkohärenz bedeutet - eine Instanziierung könnte eine spezifischere Instanz bereitstellen, aber eine inkohärente Instanz passt sowieso. Und natürlich passt die Instanz ... => C aalle Typ, wenn also Ihre C Constraint irgendwo erscheint, wird diese Instanz sofort zugeordnet werden.

Mit OVERLAPPABLE oder dergleichen, die C (F a) Einschränkung nicht kann durch Auswahl der Monoid a => C a Instanz reduziert werden, da die C Int Instanz als auch passen könnte (diese Kohärenz ist das Gegenteil von Inkohärenz).

Wenn Sie sich selbst sehen möchten, fragen Sie GHC nach dem abgeleiteten Typ f c mit INCOHERENT und OVERLAPPABLE.