Utilizzo di Type.Equality con PolyKinds

Question

Questo codice di compilazione è un esempio ridotto di this code da una risposta a this issue con sintattica-2.0. Sto anche usando una definizione di sameModType derivata da sameNat in Data.Type.Equality.

avevo usato questa soluzione senza problema, ma mi piacerebbe fare il modulo q essere gentile-polimorfico, con l'obiettivo specifico di rendere Proxy (nat :: Nat) ad appena nat :: Nat (pur essendo in grado di utilizzare moduli di tipo *) .

{-# LANGUAGE GADTs, 
      MultiParamTypeClasses, 
      FunctionalDependencies, 
      FlexibleContexts, 
      FlexibleInstances, 
      TypeOperators, 
      ScopedTypeVariables, 
      DataKinds, 
      KindSignatures #-} 

import Data.Tagged 
import Data.Proxy 
import Data.Type.Equality 
import Data.Constraint 
import Unsafe.Coerce 
import GHC.TypeLits 

newtype Zq q i = Zq i 

data ZqType q 
    where 
    ZqType :: (Modulus q Int) => Proxy q -> ZqType (Zq q Int) 

class (Integral i) => Modulus a i | a -> i where 
    value :: Tagged a i 

instance (KnownNat q) => Modulus (Proxy (q :: Nat)) Int where 
    value = Tagged $ fromIntegral $ natVal (Proxy :: Proxy q) 

sameModType :: (Modulus p i, Modulus q i) 
      => Proxy p -> Proxy q -> Maybe (p :~: q) 
sameModType p q | (proxy value p) == (proxy value q) = 
        Just $ unsafeCoerce Refl 
       | otherwise = Nothing 

typeEqSym :: ZqType p -> ZqType q -> Maybe (Dict (p ~ q)) 
typeEqSym (ZqType p) (ZqType q) = do 
     Refl <- sameModType p q -- LINE 39 
     return Dict    -- LINE 40 

Ma quando aggiungo l'estensione -XPolyKinds al codice di cui sopra, ottengo molti errori di compilazione:

Foo.hs:39:36: 
    Could not deduce (k1 ~ k) 
    ... 
    Expected type: Proxy q0 
     Actual type: Proxy q2 
    Relevant bindings include 
     q :: Proxy q2 (bound at Foo.hs:38:30) 
     p :: Proxy q1 (bound at Foo.hs:38:19) 
    In the second argument of ‘sameFactoredType’, namely ‘q’ 
    In a stmt of a 'do' block: Refl <- sameFactoredType p q 

Foo.hs:40:16: 
    Could not deduce (k ~ k1) 
    ... 
    Relevant bindings include 
     q :: Proxy q2 (bound at Foo.hs:38:30) 
     p :: Proxy q1 (bound at Foo.hs:38:19) 
    In the first argument of ‘return’, namely ‘Dict’ 
    In a stmt of a 'do' block: return Dict 
    In the expression: 
     do { Refl <- sameFactoredType p q; 
      return Dict } 

Foo.hs:40:16: 
    Could not deduce (q1 ~ q2) 
    ... 
    Relevant bindings include 
     q :: Proxy q2 (bound at Foo.hs:38:30) 
     p :: Proxy q1 (bound at Foo.hs:38:19) 
    In the first argument of ‘return’, namely ‘Dict’ 
    In a stmt of a 'do' block: return Dict 
    In the expression: 
     do { Refl <- sameFactoredType p q; 
      return Dict } 

Non conosco abbastanza la magia in corso nella uguaglianza tipo di sapere come per risolvere questo. Sembra che la maggior parte dei tipi in questione sia irrimediabilmente fuori dal campo di applicazione in termini di capacità di far rispettare i vincoli che GHC sta chiedendo, ma non ho mai avuto questo tipo di problema con PolyKinds. Cosa deve essere modificato per compilare il codice con PolyKinds?

Answer 1

Non so se questo è quello che stai cercando, ma si può semplicemente esporre quel tipo dell'argomento sottostante per un uso successivo:

data ZqType q k where 
    ZqType :: Modulus q Int => Proxy (q :: k) -> ZqType (Zq q Int) ('KProxy :: KProxy k) 

typeEqSym :: ZqType p k -> ZqType q k -> Maybe (Dict (p ~ q)) 
typeEqSym (ZqType p) (ZqType q) = do 
     Refl <- sameModType p q 
     return Dict    

instance Modulus Int Int where 
instance Modulus (n :: Nat) Int where 

KProxy dovrebbe essere in Data.Proxy, ma è solo data KProxy (x :: *) = KProxy.

Escogitato esempio:

>let x = ZqType (Proxy :: Proxy (10 :: Nat)) 
>let y = ZqType (Proxy :: Proxy Int) 
>typeEqSym x y 
<interactive>:25:13: 
    Couldn't match kind `*' with `Nat' 
    Expected type: ZqType (Zq Int Int) 'KProxy 
     Actual type: ZqType (Zq Int Int) 'KProxy 
    In the second argument of `typeEqSym', namely `y' 
    In the expression: typeEqSym x y 

Answer 2

Posso spiegare il problema, ma poiché non sono completamente sicuro di ciò che si vuole fare, non sono sicuro di come si possa risolvere il problema.

Il problema è nella definizione di ZqType:

data ZqType q 
    where 
    ZqType :: (Modulus q Int) => Proxy q -> ZqType (Zq q Int) 

E 'un po' fuorviante che il parametro tipo di ZqType si chiama q. Questo è un GADT e i parametri di tipo non hanno nulla a che fare con i parametri di tipo che appaiono nei costruttori. Preferisco dare una firma gentile invece. Qual è il tipo di ZqType? Bene, Zq q Int è un tipo di dati, quindi ha tipo *. Stai applicando ZqType a Zq q Int, quindi il tipo di ZqType è * -> * (nonostante PolyKind s). Così abbiamo

data ZqType :: * -> * where 
    ZqType :: (Modulus q Int) => Proxy q -> ZqType (Zq q Int) 

Avanti, vediamo qual è il tipo di costruttore ZqType? Senza tipi poli, è quello che hai scritto:

ZqType :: (Modulus q Int) => Proxy q -> ZqType (Zq q Int) 

Ma con PolyKind s, q è presente solo in posizioni di tipo-polimorfa, quindi questa diventa:

ZqType :: forall (q :: k). (Modulus q Int) => Proxy q -> ZqType (Zq q Int) 

Ora diamo un'occhiata a come si usa questo in sameModType:

typeEqSym :: ZqType a -> ZqType b -> Maybe (Dict (a ~ b)) 
typeEqSym (ZqType p) (ZqType q) = do 
    ... 

ho rinominato variabili di tipo per evitare confusione. Quindi a è un tipo di tipo sconosciuto * e è un altro tipo sconosciuto di tipo *. Stai eseguendo la corrispondenza del modello sul GADT. In questo momento, GHC viene a sapere che è in realtà Zq q1 Int per alcuni sconosciuti k1. Inoltre, GHC viene a sapere che è in realtà Zq q2 Int per alcuni sconosciuti q2 di un tipo sconosciuto k2.In particolare, non abbiamo idea che lo k1 e lo k2 siano gli stessi, perché questo non viene applicato da nessuna parte.

Si prosegue chiamando lo sameModType che si aspetta che entrambi i proxy siano dello stesso tipo, causando il primo dei vostri errori di tipo. Gli errori rimanenti sono tutti una conseguenza dello stesso problema.