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