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