Wie kann ich GHC dazu bringen, Instanzen von Data.Type für GADTs mit Typable im Kontext zu generieren?

Question

Angenommen, ich habe den folgenden Code:

{-# 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 

Dann arbeitet die folgende Instanzdeklaration, ohne eine Einschränkung t:

instance OnlyEq (Wrapper t) 

und tut, was ich erwarten, dass es zu tun.

---

Aber die folgende Instanzdeklaration nicht funktioniert:

instance BothEqAndTypeable (Wrapper t) 

seit GHC - Ich 7.6.1 mit - beklagt, dass:

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)' 

Typeable t dem Kontext hinzufügen funktioniert natürlich. Aber fügt auch die folgende Instanz hinzu:

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

Gibt es eine Möglichkeit, GHC diese letzte Instanz für mich zu schreiben? Wenn das so ist, wie? Wenn nicht, warum nicht?

Ich habe gehofft, GHC Lage wäre, den Typeable Zwang aus dem Kontext auf dem Wrap Konstruktor zu ziehen, so wie es mit der Eq Einschränkung tat. Ich denke, dass meine Probleme darauf hinauslaufen, dass GHC explizit das Schreiben von deriving instance Typeable (Wrapper t) verbietet, und die Standard (Typeable1 s, Typeable a) => Typeable (s a) Instanz kann nicht nach innen schauen s a, um ein Typeable a Wörterbuch zu finden.

Answer 1

ich GHC habe gehofft, wäre in der Lage, den Typeable Zwang aus dem Kontext auf dem Wrap Konstruktor

zu ziehen Wenn es einen Wrap Konstruktor hat, kann er den Typeable Zwang daraus ziehen.

Aber es hat keinen Wrap Konstruktor.

Der Unterschied besteht darin, dass die Eq Instanz den Wert verwendet, so ist es entweder ein Wrap something, wo der Wrap Konstruktor der Eq Wörterbuch für den umschlossenen Typen zur Verfügung stellt, und alles ist in Ordnung, oder es ist ⊥, und dann ist alles zu fein , Bewertung x == y Böden aus.

beachte, dass die abgeleitete

instance Eq (Wrapper a) 

tut nicht haben eine Eq Einschränkung für die Art variable 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 

Aber die Typeable Instanz muss nicht Verwendung des Wertes machen, so gibt es keine Bodenbildung, wenn der angegebene Wert kein Wrap something ist.

Somit liefert die abgeleitete instance Typeable1 Wrapper

instance Typeable t => Typeable (Wrapper t) 

aber nicht ein unbeschränkte

instance Typeable (Wrapper t) 

und unbeschränkte Instanz nicht durch GHC abgeleitet werden.

Daher müssen Sie entweder eine eingeschränkte

instance Typeable t => BothEqAndTypeable (Wrapper t) 

oder eine ungezwungene

instance Typeable (Wrapper t) 

selbst.