## Inferring dependent kinds for non-recursive types

Consider this

```
data Proxy k (a :: k) = MkProxy
data Proxy2 k a = MkP (Proxy k a)
```

which is discussed in a corner of the user manual.

Surprisingly, we reject `Proxy2`

-- but there is nothing difficult about inferring its kind. There would be if it was recursive -- but it isn't.

Simple solution: for non-recursive type declarations (we do SCC analysis so we know which these are) do not call `getInitialKinds`

; instead, just infer the kind of the definition! Simple.

Warning: is this recursive?

```
data Proxy2 k a where
MkP :: Proxy k a -> Proxy2 k a
```

Presumably no more than the other definition. But currently we need `Proxy2`

in the environment during kind inference, because we kind-check the result type. That seems jolly odd and inconsistent. Needs more thought.

Similar questions for

```
data T a where
T :: Int -> T Bool
type family F a where
F Int = True
F _ = False
```

See also: