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)
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
Bottom line: GHC mostly uses Plan A, except for an inconsistent use of Plan B at top level of
I tried doing it both ways and fell into a swamp.
Fails plan A:
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).
- So is
Fails plan B
instance Prelude.Num a => XNum a, where
XNumis poly-kinded. Under (A) this would be OK, but not under B.
typecheck/should_compile/T14441is 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
P. But the type-family applications in the RHS also each have two visible, e.g.
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/T13910is 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.