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.)

score 5 · Accepted Answer · answered Jun 04 '14 at 15:49

5

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.

answered Jun 04 '14 at 15:49

kosmikus

19,549
3
51
66

1

Interesting. As an alternative to adding `Proxy`, `AllowAmbiguousTypes` also works to resolve the declaration error. Is there a way to resolve the application error without using `Proxy`, for example by mangling the signature of `Bar`? I'm okay with using `AllowAmbiguousTypes` since presumably GHC will be able to make the necessary inferences from concrete applications. – crockeea Jun 04 '14 at 15:53
1

Can I explicitly kind `Modulus zq :: k1` and `Modulus zq' :: k2` and use kind equality `k1 ~ k2`? – crockeea Jun 04 '14 at 15:56
1

You could perhaps use a functional dependency instead: `class HasModulus (zq :: *) (m :: k) | zq -> m`. Here, the kind `k` is an "output", whereas in the kind-polymorphic type family `Modulus`, the kind `k` is an "input". Then `data Bar :: (* -> *) where Bar :: (HasModulus zq m, zq' ~ Foo zq m) => Bar (zq -> zq')` should work. – kosmikus Jun 04 '14 at 16:22
1

Hm, I guess I was hoping the type family would do something similar to the fundep. While the output kind of the `Modulus` type family is polymorphic, it is determined by its input. Is there a way to capture that with type families? – crockeea Jun 04 '14 at 17:50

Ambiguous types with PolyKinds

1 Answers1