Kind ambiguity when using PolyKinds and type families

Question

I have two type-families, one of which maps one type to another type of different kind and polymorphic function:

{-# LANGUAGE PolyKinds, TypeFamilies, FlexibleContexts, ScopedTypeVariables #-} 

type family F (a :: k1) :: k2
type family G (a :: k2) :: *

f :: forall k1 k2 (a :: k1) (p :: k1 -> *) . p (a :: k1) -> G (F (a :: k1) :: k2)
f = undefined

This code does not typecheck with following error message:

• Couldn't match type ‘G k20 (F k20 k1 a)’ with ‘G k2 (F k2 k1 a)’
  Expected type: p a -> G k2 (F k2 k1 a)
    Actual type: p a -> G k20 (F k20 k1 a)
  NB: ‘G’ is a non-injective type family

but I can't understand where ambiguity came from and how can I specify missing kinds?

When I use only one type family, it works:

g :: forall k1 k2 (a :: k1) (p :: k1 -> *) (q :: k2 -> *). p (a :: k1) -> q (F (a :: k1) :: k2)
g = undefined

Answer 1

f :: forall k1 k2 (a :: k1) (p :: k1 -> *). p a -> G (F a :: k2)

Let me try to say:

x :: [String]
x = f (Just 'a')

This goes and instantiates f with k1 ~ Type, a ~ Char, and p ~ Maybe

f :: forall k2. Maybe Char -> G (F Char :: k2)

Now what? Well, I further need G (F Char :: k2) ~ [String], but G is a non-injective type family, so there's no telling what either of its arguments—k2 and F Char :: k2—should be. Therefore, the definition of x is in error; k2 is ambiguous and it's impossible to infer an instantiation for it.

However, you can pretty clearly see that no usage of f will ever be able to infer k2. The reasoning is that k2 only appears in the type of f underneath a non-injective type family application (the other "bad position" is the LHS of a =>). It never appears in a position where it can be inferred. Therefore, without an extension like TypeApplications, f is useless, and can never be mentioned without raising this error. GHC gives detects this and raises an error at the definition rather than the usages. The error message you see is about the same error you get if you try:

f0 :: forall k10 k20 (a :: k10) (p0 :: k10 -> *). p0 a0 -> G (F a0 :: k20)
f0 = f

This produces the same type mismatch, as there is no reason the k20 of f0 must match the k2 of f1.

You can silence the error in the definition of f by enabling AllowAmbiguousTypes, which disables this uselessness check on all definitions. However, alone, this just pushes the error to every usage of f. In order to actually call f, you should enable TypeApplications:

f0 :: forall k10 k20 (a :: k10) (p0 :: k10 -> *). p0 a0 -> G (F a0 :: k20)
f0 = f @k10 @k20 @a0 @p0

The alternative to TypeApplications is something like Data.Proxy.Proxy, but that's pretty much obsolete, except in higher-rank contexts. (And even then, it'll really be out of its job once we have something like type-lambdas.)

Answer 2

The ambiguity check was originally intended to reject functions which can't ever be called, because of type parameters and constraints which are not inferable from explicit function arguments.

However, as of GHC 8.6.x, there are no such functions, because everything can be made explicit by TypeApplications. I recommend to just enable AllowAmbiguousTypes and TypeApplications. GHC's warning about ambiguous types is not very informative by itself, since it rejects many of the valid use cases of type applications.