Istanza tipizzabile per torsione di vincoli

Question

Sto provando a ricavare un'istanza Typeable per i vincoli di tipo tupla. Vedere il seguente codice:

{-# LANGUAGE ConstraintKinds, GADTs #-} 
{-# LANGUAGE DataKinds, PolyKinds, AutoDeriveTypeable #-} 
{-# LANGUAGE StandaloneDeriving, DeriveDataTypeable #-} 

import Data.Proxy 
import Data.Typeable 

data Foo (p :: (*, *)) 

data Dict ctx where 
    Dict :: ctx => Dict ctx 
    deriving (Typeable) 

deriving instance Typeable '(,) 
deriving instance Typeable Typeable 
deriving instance Typeable Show 

works :: IO() 
works = print (typeRep (Proxy :: Proxy (Foo '(Bool, Char)))) 

alsoWorks :: IO() 
alsoWorks = print (typeRep (Dict :: Dict (Show Bool))) 

fails :: IO() 
fails = print (typeRep (Dict :: Dict (Show Bool, Typeable Bool))) 

main :: IO() 
main = works >> alsoWorks >> fails 

Se si compila questo con -fprint-explicit-kinds, viene dato il seguente errore:

No instance for (Typeable 
        (Constraint -> Constraint -> Constraint) (,)) 

Esiste un modo per ricavare un caso del genere? Tutto ciò che provo si rifiuta di disambiguare dal costruttore ★ -> ★ -> ★.

Answer 1

GHC non può attualmente fare un esempio Typeable, o di qualsiasi altro esempio, per (,) :: Constraint -> Constraint -> Constraint. Il tipo di costruttore (,) ha solo il tipo * -> * -> *. There is no type constructor for products of the kind Constraint -> Constraint -> Constraint. Il costruttore (,) è sovraccarico per la costruzione di tuple e prodotti di Constraint s, ma non ha alcun costruttore di tipo corrispondente quando viene utilizzato per creare un prodotto di Constraint s.

Se disponessimo di un costruttore di tipi per prodotti di Constraint s dovremmo essere in grado di definire un'istanza come segue. Per fare ciò, fingiamo che (,) sia anche un costruttore di tipi con tipo (,) :: Constraint -> Constraint -> Constraint. Per definire un'istanza per esso, si userebbe KindSignatures e importare GHC.Exts.Constraint essere in grado di parlare del tipo di vincoli esplicitamente

{-# LANGUAGE ConstraintKinds #-} 
{-# LANGUAGE StandaloneDeriving #-} 
{-# LANGUAGE DeriveDataTypeable #-} 
{-# LANGUAGE KindSignatures #-} 

import GHC.Exts (Constraint) 
import Data.Typeable 

deriving instance Typeable ((,) :: Constraint -> Constraint -> Constraint) 

Se facciamo questo ora, il risultato e 'il seguente errore, a causa del tipo del costruttore del tipo (,).

The signature specified kind `Constraint 
           -> Constraint -> Constraint', 
    but `(,)' has kind `* -> * -> *' 
In the stand-alone deriving instance for 
    `Typeable ((,) :: Constraint -> Constraint -> Constraint)' 

Il pacchetto constraints funziona anche con prodotti di vincoli, e comprende the following note.

causa l'hack per il tipo di (,) nella versione attuale del GHC non possiamo effettivamente fare le istanze per (,) :: Constraint -> Constraint -> Constraint

presumo l'hack Edward Kmett si riferisce è il sovraccarico del Costruttore (,) per Constraint s senza un costruttore di tipi corrispondente.

Answer 2

Sembra che non sia attualmente possibile. C'è un commento rivelatore nel latest version di constraint:

causa l'hack per il tipo di (,) nella versione corrente di GHC non possiamo effettivamente fare istanze per (,) :: vincolo -> Constraint -> Constraint