Inferring dependent kinds for non-recursive types
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