Kind inference examples

This page is intended to collect examples of tricky cases for kind inference. Any proposed algorithm should be applied to each of these cases to see how it would behave.

More discussion is at GhcKinds/KindInference.

Associated types

class C1 (a :: k) where
  type F a

Question: What should the visibilities on F be?

Ryan and Richard think F :: forall k. k -> Type. That is, k is Specified, because we can always order implicit kind variables using the same ordering that appears in the class header (after kind inference).

class C2 (a :: k) (b :: k2) where
  type T a

Proposed: T :: forall k. k -> Type, with no mention of b or k2.

class C3 (a :: k) (b :: k2) hwere
  type T (z :: k3) a

Proposed: T :: forall k k3. k3 -> k -> Type. This puts k before k3, because class variables come before other ones (unless the user explicitly puts them later, as has been done with a). This rule always works because class variables cannot depend on local ones.

class C4 a (b :: a) where
  type T b a

This must be rejected, as b depends on a.

class C5 (a :: k) where
  type T (a :: k2)

Reject: k and k2 are distinct skolems.

class C6 a (b :: a) (c :: Proxy b) where
  type T (x :: Proxy '(a, c))

Proposed: T :: forall (a :: Type) (b :: a) (c :: Proxy b). Proxy '(a, c) -> Type. Note that b is included here as a Specified variable. It could also be an Inferred, if we prefer.

class C7 a (b :: a) (c :: Proxy b) where
  type T a c

Proposed: T :: forall (a :: Type) -> forall (b :: a). Proxy b -> Type. We've inserted b between a and c, but b is Specified, not Required. Other possibilities: make b Inferred, or reject altogether.

Datatypes, dependency, and polymorphic recursion

Assume

data Prox k (a :: k)

data Prox2 k a = MkP2 (Prox k a)

Question: Do we allow k to be dependently quantified, even if this is not lexically apparent from the declaration? This is rejected today.

data S2 k (a :: k) b = MkS (S2 k b a)

Proposed: S2 :: forall k -> k -> k -> Type. Note that a and b are inferred to have the same kind, as that avoid polymorphic recursion.

data S3 k (a :: k) b = MkS (S3 Type b a)

Proposed: reject as polymorphically recursive. Yet the idea in GhcKinds/KindInference#Simonssuggestion accepts this.

data Q2 k a where
  MkQ2 :: Prox k a -> Q2 k a

data Q3 k a where
  MkQ3 :: Q3 k a -> Prox k a -> Q3 k a

data Q4 k a where
  MkQ4 :: Q4 Bool False -> Prox k a -> Q4 k a

data Q5 k a where
  MkQ5 :: Q5 Bool False -> Q5 Nat 3 -> Prox k a -> Q5 k a

Agda accepts all of the above. It puts us to shame!

data Proxy2 a where
  Mk1 :: Proxy2 (a :: k)
  Mk2 :: Proxy2 (b :: j)

This should really be accepted. But it's challenging to arrange this, because a, k, b, and j all scope locally within their constructors. How can the kind of Proxy2 unify with any of them?

data T a where
  Mk :: forall k1 k2 (a :: k1) (b :: k2). T b -> T a

This is polymorphically recursive. Yet hGhcKinds/KindInference#SimonsProposedSolution accepts it. (That's what's implemented in GHC 8.6.) Richard thinks we should reject.

data T2 a where
  Mk :: forall (a :: k). T2 Maybe -> T2 a

This one is rejected, as it should be. So we don't accept all polymorphic recursion (how could we?). But we don't have a good specification for what we do accept and what we don't.

data T3 a b where
  Mk :: T3 b a -> T3 a b

This should be accepted with T3 :: forall k. k -> k -> Type; it's not polymorphically recursive. Yet, it would seem any specification which accepted T would also give T3 the polymorphically recursive kind forall k1 k2. k1 -> k2 -> Type.

data T4 k (a :: k) b = MkT4 (T4 k b a)

Here, we have a dependent kind for T4. Richard thinks this should be accepted. Proposed rule: dependent variables must be fixed an unchanging at all occurrences within a mutually recursive group (otherwise, we have polymorphic recursion). That is, it would be an error to mention, say, T4 k2 anywhere in the body of T4: it must be T4 k.

Generalization

Contrast

class C8 a where
  meth :: Proxy (a :: k)

with

data V1 a where
  MkV1 :: Proxy (a :: k) -> V1 a

Currently (GHC 8.6) we reject C8 while accepting V1. This may be just a bug, but it has to do with the fact that the type of meth isn't quantified over a, but it is over k (lexically).

Dependency ordering

What if we do something simple? Like just use lexical ordering.

data Proxy (a :: k)

Then this example fails, with k after a.

Refinement: consider the RHS of :: before the LHS.

Then this one fails:

data T4 a (b :: k) (x :: SameKind a b)

The k would end up between the a and the b, even though a depends on k.

Also, consider

data T5 a (c :: Proxy b) (d :: Proxy a) (x :: SameKind b d)

Here, b needs to be between a and x somewhere. But where? Currently (GHC 8.6), this is rejected because implicitly declared variables come before explicit ones.

And more

There are many more examples in the testsuite, of course. In particular, see the T14066 tests and the BadTelescope tests.

Comparison to Idris

Idris accepts T4 and T5, so we think Idris use some kind of ScopedSort.

However, Idris also accepts

data T6 :  (a:k) -> (k:Type) -> Type

with type {k : Type} -> (a : k) -> (k2 : Type) -> Type. We think both this acceptance and the inferred type are odd, as we would expect these two ks to be the same k. Then T6 should be rejected because a cannot refer to a variable k that appears after.

Idris would reject

data T7 : (a : k) -> (k:Type) -> (b : k) -> SameKind a b -> Type

with a kind mismatch error between a:k2 and b:k. We agree this should be rejected but it should be rejected with another error: a cannot refer to k.

Difference between Specified and Inferred

The reason we want to accept T4 but reject T6 is because there is a difference between Specified type variable and Inferred type variable. In T4, k is Inferred; thus when we generalize its type, we can put k before a. In contrast, in T6, k is specified, and its order is indicated explicitly by the user, so a is not allowed to refer to it.