W jaki sposób można uzyskać GHC do generowania wystąpień Data.Typeable dla GADT z Typeable w kontekście?

Question

Załóżmy, że mam następujący kod:

{-# LANGUAGE GADTs, DeriveDataTypeable, StandaloneDeriving #-} 
import Data.Typeable 

class Eq t => OnlyEq t 
class (Eq t, Typeable t) => BothEqAndTypeable t 

data Wrapper a where 
    Wrap :: BothEqAndTypeable a => a -> Wrapper a 

deriving instance Eq (Wrapper a) 
deriving instance Typeable1 Wrapper 

Wówczas następujące oświadczenie instancja działa, bez ograniczenie na t:

instance OnlyEq (Wrapper t) 

i robi to, co od niego oczekujesz.

---

Ale następującą deklarację instancji nie działa:

instance BothEqAndTypeable (Wrapper t) 

od GHC - używam 7.6.1 - skarży się, że:

No instance for (Typeable t) 
    arising from the superclasses of an instance declaration 
Possible fix: 
    add (Typeable t) to the context of the instance declaration 
In the instance declaration for `BothEqAndTypeable (Wrapper t)' 

Dodawanie Typeable t do kontekstu działa, oczywiście. Ale tak samo dodaje się następujący przykład:

instance Typeable (Wrapper t) where 
    typeOf (Wrap x) = typeOf1 (Wrap x) `mkAppTy` typeOf x 

Czy istnieje sposób, aby GHC napisał dla mnie tę ostatnią instancję? Jeśli tak to jak? Jeśli nie, dlaczego nie?

Miałem nadzieję, że GHC będzie w stanie wyciągnąć ograniczenie z Typeable z kontekstu konstruktora Wrap, tak jak miało to miejsce z ograniczeniem Eq. Myślę, że moje problemy sprowadzają się do faktu, że GHC wyraźnie uniemożliwia pisanie deriving instance Typeable (Wrapper t), a standardowa instancja (Typeable1 s, Typeable a) => Typeable (s a) nie może "zajrzeć do środka" s a, aby znaleźć słownik Typeable a.

Answer 1

Miałem nadzieję GHC będzie w stanie pociągnąć Typeable ograniczenie z kontekstu na konstruktora

Wrap Jeśli miał Wrap konstruktora, może to pociągnąć Typeable ograniczenie od niego.

Ale nie ma konstruktora Wrap.

Różnica polega na tym, że instancja Eq używa wartości, więc to albo Wrap something, gdzie konstruktor Wrap sprawia słownika Eq dla zawiniętego typu nie jest dostępna, i wszystko jest w porządku, czy to ⊥, a następnie wszystko jest w porządku , oceniając dna od x == y.

Zauważ, że pochodzi

instance Eq (Wrapper a) 

robi nie mieć Eq ograniczenia na typ zmiennej a.

Prelude DerivT> (undefined :: Wrapper (Int -> Int)) == undefined 
*** Exception: Prelude.undefined 
Prelude DerivT> (undefined :: (Int -> Int)) == undefined 

<interactive>:3:29: 
    No instance for (Eq (Int -> Int)) arising from a use of `==' 
    Possible fix: add an instance declaration for (Eq (Int -> Int)) 
    In the expression: (undefined :: Int -> Int) == undefined 
    In an equation for `it': 
     it = (undefined :: Int -> Int) == undefined 

Ale instancja Typeable nie musi skorzystać z wartości, więc nie ma najniższy jeśli dostarczony wartość nie jest Wrap something.

Tak więc pochodnego instance Typeable1 Wrapper dostarcza

instance Typeable t => Typeable (Wrapper t) 

ale nie nieograniczającą

instance Typeable (Wrapper t) 

i nieograniczony przykład, nie może być uzyskany przez GHC.

Stąd trzeba też zapewnić ograniczony

instance Typeable t => BothEqAndTypeable (Wrapper t) 

lub niewymuszony

instance Typeable (Wrapper t) 

samemu.