5

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
schernichkin
  • 1,013
  • 7
  • 15
  • 1
    This is a nicely presented question. However, when posting such issues, it is always better to post the _full_ error message :-) . Here, GHCi also adds `To defer the ambiguity check to use sites, enable AllowAmbiguousTypes` which is a tale-teller. I couldn't see what was wrong at first above, but after reading the ambiguity error everything was much clearer. (BTW, that's another extension that I wish would be turned on by default in a future Haskell revision.) – chi Jan 14 '19 at 12:37

2 Answers2

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

HTNW
  • 27,182
  • 1
  • 32
  • 60
  • I think I got it. I was thinking that defining `type family F (a :: k1) :: k2` will introduce dependency between k1 and k2, but it doest not, kinds are arguments itself and we can have multiple instances mapping Char to different kinds. It can be seen from istance signatures, e.g. for `type instance F Char = Bool` `:i F` will give `type instance F * * Char = Bool` where both kind variables located on the left side. – schernichkin Jan 13 '19 at 22:42
  • You may declare `type family FTy (k :: Type) :: Type; type family F (a :: k) :: FTy k` to enforce each that each input kind has one output kind, or `type family FTy (a :: k) :: Type; type family F (a :: k) :: FTy a` to enforce one output of any kind for each input. I didn't realize this was your original issue when writing the answer, sorry. – HTNW Jan 14 '19 at 15:05
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.

András Kovács
  • 29,931
  • 3
  • 53
  • 99
  • Actually I do not need `PolyKinds` for my task at all. Multiple kinds came from promoted datatypes, by I can define instances for proxied types of kind `*`. The first argument of `f` namelly `p (a :: k1)` is a singleton proxy. I personally don't like the idea of disabling ambiguity checks, event of enabling `PolyKinds` without sufficient reasons, because kind-monomorphic code allows simplier signatures. – schernichkin Jan 13 '19 at 23:21