[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
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Description changed by simonpj:

Old description:

> 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.

New description:

 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`!  Moreover, `sizeTypes` itself does not do the
 `filterOutInvisibleTypes` when it finds a `TyConApp`.

 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#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler