Ambiguous types with PolyKinds

Question

The following compiles without PolyKinds:

{-# LANGUAGE TypeFamilies, GADTs #-}

type family Modulus zq

type family Foo zq q

data Bar :: (* -> *) where
    Bar :: (zq' ~ Foo zq (Modulus zq)) => Bar (zq -> zq')

All appearances of zq are some type (kind *) representing modular arithmetic mod q. It'd be convenient to use Nats to represent these moduli. If I add PolyKinds and poly-kind the moduli in the type families:

{-# LANGUAGE TypeFamilies, GADTs, PolyKinds #-}

type family Modulus zq :: k

type family Foo zq (q :: k)

data Bar :: (* -> *) where
    Bar :: (zq' ~ Foo zq (Modulus zq)) => Bar (zq -> zq')

GHC 7.8 complains:

Could not deduce (zq' ~ Foo zq (Modulus zq))
...
In the ambiguity check for:
  forall zq' zq. zq' ~ Foo zq (Modulus zq) => Bar (zq -> zq')
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the definition of data constructor ‘Bar’

Did adding PolyKinds really make this ambiguous? Where is the ambiguity? Also related: When is -XAllowAmbiguousTypes appropriate?

If I throw GHC a bone and add AllowAmbiguousTypes the error moves from the declaration of the GADT to the use of the GADT (sans the suggestion to add the extension):

bar :: (zq' ~ Foo zq (Modulus zq))
  => Bar (zq -> zq')
bar = Bar

which makes me think using AllowAmbiguousTypes is a GHC red herring.

EDIT

To clarify, the types above might be instantiated as follows:

newtype Zq q = Zq Int

Then zq ~ (Zq 3), q ~ 3, and Modulus (Zq 3) ~ 3, Foo (Zq 3) 3 ~ (Zq 3) (I stripped the work out of the Foo type family, so think of it as identity.)

Answer 1

Let's restrict the zq arguments to kind * for the time being:

type family Modulus (zq :: *) :: k

type family Foo (zq :: *) (q :: k)

Then you get a slightly better error message that can be further improved by saying -fprint-explicit-kinds (assuming GHC 7.8):

Could not deduce ((~) * zq' (Foo k0 zq (Modulus k0 zq)))
from the context ((~) * zq' (Foo k zq (Modulus k zq)))

So the problem is that Modulus is polymorphic in its output kind, and Foo is polymorphic in its input kind. There's nothing that fixes this intermediate kind, so it remains ambiguous. One option to fix it is to use a Proxy:

import Data.Proxy

...

data Bar :: (* -> *) where
    Bar :: (m ~ Modulus zq, zq' ~ Foo zq m) => Proxy m -> Bar (zq -> zq')

Now you could even remove the * annotations for Modulus and Foo again and it would still work.