Can't solve constraints with UndecidableSuperClasses but can infer kind (+ undesired order of kinds)

The Glorious Glasgow Haskell Compilation System, version 8.0.1.

Code taken from gist with

 fmap :: p a b -> q (f a) (f b)

replaced by

 fmap :: Dom f a b -> Cod f (f a) (f b)

If you enable DataKinds and TypeInType :kind will happily tell you its kind:

ghci> :kind 'Main.Nat
'Main.Nat :: forall j i (p :: Cat i) (q :: Cat j) (f :: i
                                                        -> j) (g :: i -> j).
             (FunctorOf p q f, FunctorOf p q g) =>
             (forall (a :: i). Ob p a => q (f a) (g a)) -> Main.Nat p q f g

but if you try :type Nat it spits out a long list of unsolved constraints

ghci> :type Nat

<interactive>:1:1: error:
    solveWanteds: too many iterations (limit = 1)
      Unsolved: WC {wc_simple =
                      [W] $dFunctor_ag3Y :: Main.Functor f_ag3S (CDictCan)
                      [W] $dFunctor_ag4d :: Main.Functor g_ag3T (CDictCan)
                      [D] _ :: Main.Functor s_ag51 (CDictCan)
                      [D] _ :: Main.Functor s_ag5a (CDictCan)
                      [D] _ :: Main.Functor s_ag4W (CDictCan)
                      [D] _ :: Main.Functor s_ag55 (CDictCan)
                      [D] _ :: Category s_ag51 (CDictCan)
                      [D] _ :: Category s_ag5a (CDictCan)
                      [D] _ :: Category s_ag4W (CDictCan)
                      [D] _ :: Category s_ag55 (CDictCan)
                      [W] hole{ag4Y} :: Dom g_ag3T ~ Dom f_ag3S (CNonCanonical)
                      [W] hole{ag53} :: Cod g_ag3T ~ Cod f_ag3S (CNonCanonical)
                      [D] _ :: Dom (Dom f_ag3S) ~ Op (Dom f_ag3S) (CNonCanonical)
                      [D] _ :: Cod (Dom f_ag3S)

This seems like #11480 (closed). This makes undecidable superclasses a harsh master and raises two questions that I'll bundle together:

1. Why can the :kind be inferred but not the :type? It works when given extra information:

ghci> :type Nat @_ @_ @(->) @(->) Nat @_ @_ @(->) @(->) :: (Cod g ~ (->), Dom g ~ (->), Cod f ~ (->), Dom f ~ (->), Main.Functor g, Main.Functor f) => (forall a. Vacuous (->) a => f a -> g a) -> Main.Nat (->) (->) f g

ghci> :type Nat @_ @_ @_ @_ @[] @Maybe Nat @_ @_ @_ @_ @[] @Maybe :: (forall a. Vacuous (->) a => [a] -> Maybe a) -> Main.Nat (->) (->) [] Maybe

ghci> :type Nat @_ @_ @_ @_ @[] @Maybe listToMaybe Nat @_ @_ @_ @_ @[] @Maybe listToMaybe :: Main.Nat (->) (->) [] Maybe

1. Why is j positioned before i (most likely because of forall a. ... but I tried tinkering without success? Is there any trick to ordering it as you'd expect forall i j (p :: Cat i) (q :: Cat j) or is it not possible per #12025 (closed)?

Trac metadata

Trac field	Value
Version	8.0.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture