Faulty instance termination check, with PolyKinds and/or TypeInType

When checking the Paterson conditions for termination an instance declaration, we check for the number of "constructors and variables" in the instance head and constraints. Question: Do we look at

• A. All the arguments, visible or invisible?
• B. Just the visible arguments?

I think both will ensure termination, provided we are consistent.

A current bug in GHC means that we are not consistent. In particular in TcValidity.checkInstTermination we see

checkInstTermination tys theta
  = check_preds theta
  where
   ...
   head_size = sizeTypes tys

   ...
   check pred
     = case classifyPredType pred of
         ...
           -> check2 pred (sizeTypes $ filterOutInvisibleTypes (classTyCon cls) tys)

Notice the filterOutInvisibleTypes in the context predicate, but not for the head_size! Similarly in sizePred (which itself looks very ad hoc; used only for 'deriving'). Moreover, sizeTypes itself does not do the filterOutInvisibleTypes when it finds a TyConApp.

Bottom line: GHC mostly uses Plan A, except for an inconsistent use of Plan B at top level of checkInstTermination and sizePred.

I tried doing it both ways and fell into a swamp.

Fails plan A:

• rebindable/T5908 has instance (Category w, ...) => Monad (WriterT w m). With kind arguments this is actually instance (Category @* w, ...) => Monad (WriterT w m), and now the predicate in the context and the head both have size 4. So under (B) this is OK but not under (A).
• deriving/should_compile/T11833 is similar
• So is overloadedrecflds/should_run/hasfieldrun02.

Fails plan B

• polykinds/T12718 has instance Prelude.Num a => XNum a, where XNum is poly-kinded. Under (A) this would be OK, but not under B.
• typecheck/should_compile/T14441 is tricky. Putting in explicit kinds we have

type family Demote (k :: Type) :: Type
-- Demote :: forall k -> Type

type family DemoteX (a :: k) :: Demote k
-- DemoteX :: forall k. k -> Demote k

data Prox (a :: k) = P
-- P :: forall k (a:k). Prox @k a

type instance DemoteX P = P
-- type instance DemoteX (Prox @k a) (P @k @a)
--    = P @(Demote k) @(DemoteX @k a)

So the LHS has 2 visible constructors and variables, namely DemoteX and P. But the type-family applications in the RHS also each have two visible, e.g. Demote and k for Demote k. Confusingly, these applications are hidden inside the invisible argument of P; but we really must look at them to ensure termination. Aaargh.

• dependent/should_compile/T13910 is similar, but a lot more complicated.

Currently, because of the bug, these all pass. But I think it should be possible to exploit the bug to defeat the termination check, so things are not good at all.