# 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 `k`s 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.