Using Type.Equality with PolyKinds

Question

This compiling code is a minimized example of this code from an answer to this issue with syntactic-2.0. I'm also using a definition of sameModType derived from sameNat in Data.Type.Equality.

I had been using this solution without issue, but I'd like to make the modulus q be kind-polymorphic, with the specific goal of making Proxy (nat :: Nat) to just nat :: Nat (while still being able to use moduli of kind *).

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

But when I add the -XPolyKinds extension to the code above, I get several compile errors:

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 }

I don't know enough about the magic going on in the type equality to know how to fix this. It appears that most of the kinds in question are hopelessly out of scope in terms of being able to enforce the constraints GHC is asking for, but I've never had this sort of problem before with PolyKinds. What needs to change to make the code compile with PolyKinds?

Answer 1

I can explain the problem, but as I'm not completely sure what you want to do, I'm not sure how you can best fix it.

The problem is in the definition of ZqType:

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

It's somewhat misleading that the type parameter of ZqType is called q. This is a GADT, and the type parameters have nothing to do with the type parameters appearing in the constructors. I prefer giving a kind signature instead. What is the kind of ZqType? Well, Zq q Int is a datatype, so it has kind *. You're applying ZqType to Zq q Int, so the kind of ZqType is * -> * (despite PolyKinds). So we have

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

Next, let's see what's the type of the ZqType constructor? Without poly kinds, it's what you wrote down:

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

But with PolyKinds, q is appearing only in kind-polymorphic positions, so this becomes:

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

Now let's look at how you use this in sameModType:

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

I've renamed type variables to avoid confusion. So a is an unknown type of kind *, and b is another unknown type of kind *. You're pattern matching on the GADT. At this time, GHC learns that a is actually Zq q1 Int for some unknown q1 of some unknown kind k1. Furthermore, GHC learns that b is actually Zq q2 Int for some unknown q2 of some unknown kind k2. In particular, we have no idea here that k1 and k2 are the same, because this is nowhere enforced.

You then go on calling sameModType which expects both proxies to be of the same kind, resulting in the first of your kind errors. The remaining errors are all a consequence of the same problem.