Dlaczego nie można wyprowadzić wystąpienia instancji dla produktu MaybeT?

Question

Jeśli zdefiniuję typ transformatora monad dla Identity, jest on w stanie wywnioskować instancję Show.

newtype IdentityT f a = 
    IdentityT { runIdentityT :: f a } 
    deriving (Show) 

będą czerpać

instance Show (f a) => Show (IdentityT f a) 

Ale jeśli określić rodzaj transformatora monada dla Maybe

newtype MaybeT m a = 
    MaybeT { runMaybeT :: m (Maybe a) } 
    deriving (Show) 

pojawia się błąd

• No instance for (Show (m (Maybe a))) 
     arising from the first field of ‘MaybeT’ (type ‘m (Maybe a)’) 

Od Maybe a ma instancję Show, spodziewam go do pracy i czerpać

instance Show (m (Maybe a)) => Show (MaybeT m a) 

Dlaczego nie może?

Answer 1

GHC używa heurystyki do określenia, czy instancja gwarantuje zakończenie wyszukiwania. Przez zakończenie tutaj rozumiemy, że podczas wyszukiwania instancji nie będziemy pętli na zawsze. Konkretnie, musi być zabroniony

instance Show a => Show a where ... 

Oprócz tego

instance Show [a] => Show a where ... 

GHC przybliżeniu wymaga ograniczenia w kontekście przykład (część przed =>) musi być „mniejsza” niż ograniczeniem w głowa (po =>). Tak, że przyjmuje to:

instance Show a => Show [a] where ... 

od a zawiera jeden konstruktor typu mniej niż [a].

akceptuje również to:

instance Show (f a) => Show (IdentityT f a) where ... 

od f a zawiera jeden konstruktor typu mniej niż IdentityT f a.

Jednak

instance Show (f (Maybe a)) => Show (MaybeT f a) where ... 

wykorzystuje tę samą liczbę konstruktorów! Dlatego nie jest akceptowane, aby upewnić się, że nie spowoduje pętli. W końcu później możemy spotkać się z tym, że możemy spotkać się z tym, że co najmniej jedno z tych dwóch wystąpień musi zostać odrzucone, aby zagwarantować rozwiązanie.GHC decyduje się na odrzucenie obu z nich.

UndecidableInstances rozluźnia to ograniczenie. GHC zaakceptuje obie instancje, a teraz obciążenie jest dla nas, aby uniknąć pętli.

Answer 2

myślę, że możemy zobaczyć ten problem przez następujące propozycje GHC jest (używam 8.2.1), aż trafiliśmy w ślepy zaułek:

Prelude> :{ 
Prelude| newtype MaybeT m a = 
Prelude| MaybeT { runMaybeT :: m (Maybe a) } 
Prelude| deriving (Show) 
Prelude| :} 

<interactive>:12:13: error: 
    • No instance for (Show (m (Maybe a))) 
     arising from the first field of ‘MaybeT’ (type ‘m (Maybe a)’) 
     Possible fix: 
     use a standalone 'deriving instance' declaration, 
      so you can specify the instance context yourself 
    • When deriving the instance for (Show (MaybeT m a)) 
Prelude> :set -XStandaloneDeriving 
Prelude> deriving instance Show (m (Maybe a)) => Show (MaybeT m a) 

<interactive>:17:19: error: 
    • The constraint ‘Show (m (Maybe a))’ 
     is no smaller than the instance head 
     (Use UndecidableInstances to permit this) 
    • In the stand-alone deriving instance for 
     ‘Show (m (Maybe a)) => Show (MaybeT m a)’ 

Ok, więc Show nie było wyprowadzić na MaybeT prawdopodobnie dlatego, ograniczenie to byłoby niedopuszczalne, ponieważ jest to rodzaj ograniczenia, z jakim typechecker nie może udowodnić zakończenia. Więcej informacji na temat tego, co oznacza "nie mniej niż głowa instancji" w tej odpowiedzi: https://stackoverflow.com/a/17866970/176841