[GHC] #15177: Faulty instance termination check, with PolyKinds and/or TypeInType

[GHC]

#15177: Faulty instance termination check, with PolyKinds and/or TypeInType
-------------------------------------+-------------------------------------
           Reporter:  simonpj        |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.6.1
          Component:  Compiler       |           Version:  8.2.2
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 When checking the [http://downloads.haskell.org/~ghc/master/users-
 guide/glasgow_exts.html#instance-termination-rules 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`!

 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 actualy `instance (Category @(TYPE
 LiftedRep) w, ...) => Monad (WriterT w m)`, and now the predicate in the
 context and the head both ahve 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.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15177>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler