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
hasinstance (Category w, ...) => Monad (WriterT w m)
. With kind arguments this is actuallyinstance (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
hasinstance Prelude.Num a => XNum a
, whereXNum
is polykinded. 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
andP
. But the typefamily applications in the RHS also each have two visible, e.g.Demote
andk
forDemote k
. Confusingly, these applications are hidden inside the invisible argument ofP
; 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.