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
Let me try to say:
This goes and instantiates
f
withk1 ~ Type
,a ~ Char
, andp ~ Maybe
Now what? Well, I further need
G (F Char :: k2) ~ [String]
, butG
is a non-injective type family, so there's no telling what either of its arguments—k2
andF Char :: k2
—should be. Therefore, the definition ofx
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 inferk2
. The reasoning is thatk2
only appears in the type off
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 likeTypeApplications
,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:This produces the same type mismatch, as there is no reason the
k20
off0
must match thek2
off1
.You can silence the error in the definition of
f
by enablingAllowAmbiguousTypes
, which disables this uselessness check on all definitions. However, alone, this just pushes the error to every usage off
. In order to actually callf
, you should enableTypeApplications
:The alternative to
TypeApplications
is something likeData.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.)