Korzystanie z Type.Equality with PolyKinds

Question

Ten kod kompilujący jest zminimalizowanym przykładem this code z odpowiedzi na this issue z syntactic-2.0. Używam również definicji sameModType pochodzącej z sameNat w Data.Type.Equality.

byłem korzystania z tego rozwiązania bez problemu, ale chciałbym, aby moduł q być niby-polimorficzny, z konkretnym celem dokonywania Proxy (nat :: Nat) tylko nat :: Nat (a jednocześnie jest w stanie wykorzystać moduły E z rodzaju *) .

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

Ale kiedy dodać rozszerzenie -XPolyKinds z kodem powyżej, mam kilka błędów kompilacji:

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 } 

nie wiem wystarczająco dużo o magia dzieje w równości typu umieć to naprawić. Wygląda na to, że większość omawianych rodzajów jest beznadziejnie poza zasięgiem, jeśli chodzi o możliwość egzekwowania ograniczeń, o które prosi GHC, ale nigdy wcześniej nie miałem takiego problemu z PolyKinds. Co trzeba zmienić, aby kod skompilował się z PolyKinds?

Answer 1

Nie wiem, czy to jest to, czego szukasz, ale można po prostu wystawiać rodzaju bazowego argumentu do późniejszego użytku:

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 powinny być w Data.Proxy, ale jest tylko data KProxy (x :: *) = KProxy.

wymyślony przykład:

>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

Mogę wyjaśnić problem, ale ponieważ nie jestem całkowicie pewien, co chcesz zrobić, nie jestem pewien, jak najlepiej go naprawić.

Problem jest w definicji ZqType:

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

Jest to nieco mylące, że parametr typu ZqType nazywa q. Jest to GADT, a parametry typu nie mają nic wspólnego z parametrami typu pojawiającymi się w konstruktorach. Zamiast tego wolę nadawać odpowiedni podpis. Jaki jest rodzaj ZqType? Cóż, Zq q Int jest typem danych, więc ma rodzaj *. Podajesz ZqType do Zq q Int, więc rodzaj ZqType jest * -> * (pomimo PolyKind s). Więc mamy

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

Następny, zobaczmy, co jest rodzajem konstruktora ZqType? Bez poli rodzaju, to co napisałeś w dół:

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

Ale PolyKind s q pojawia się tylko w pozycji na rodzaj polimorficzny, więc staje się:

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

Teraz przyjrzyjmy się, jak używać to w sameModType:

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

mam przemianowany zmiennych typu, aby uniknąć nieporozumień. Tak więc a jest nieznanym rodzajem rodzaju *, a b jest kolejnym nieznanym rodzajem rodzaju *. Pasujesz do wzorca na GADT. W tym czasie GHC dowiaduje się, że a jest faktycznie Zq q1 Int dla nieznanego q1 jakiegoś nieznanego rodzaju k1. Ponadto GHC dowiaduje się, że b jest faktycznie Zq q2 Int dla nieznanego q2 jakiegoś nieznanego rodzaju k2.W szczególności nie mamy pojęcia, że ​​są one takie same, ponieważ nigdzie nie jest to egzekwowane.

Następnie dzwonisz pod numer sameModType, który oczekuje, że oba serwery proxy będą tego samego rodzaju, co spowoduje błędy pierwszego rodzaju. Pozostałe błędy są konsekwencją tego samego problemu.