[GHC] #12734: Unexpected context reduction stack overflow
#12734: Unexpected context reduction stack overflow -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 8.0.1 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: -------------------------------------+------------------------------------- Hello! I don't have a minimal example, but I've got a very clear strange bahavior: We've got a function: {{{ nstar3 :: ( ExprCons t layers m, Bindable t m, Self.MonadSelfBuilder (Binding (Expr2 t layers AnyLayout)) m , ExprInferable t layers m) => m (Binding (PrimExpr2' t layers Star)) nstar3 = Self.put . anyLayout2 =<<& (nstar2 >>= mkBinding) }}} If I use it in a different function and use following explicit type, I get the error: {{{ test_gr3 :: ( ExprCons t layers m, Bindable t m, ExprInferable t layers m , MonadIO m, Show bind, Show (PrimExpr2' t layers Star), layers~'[Data, Type] , Self.MonadSelfBuilder (Binding (Expr2 t layers AnyLayout)) m , bind ~ Binding (PrimExpr2' t layers Star) ) => m bind test_gr3 = do sref <- nstar3 }}} error (while using the function and evaluating monads): {{{ • Reduction stack overflow; size = 201 When simplifying the following type: MonadFix (Self.SelfBuilderT (Binding (Expr2 t0 '[Data, Type] AnyLayout)) m) Use -freduction-depth=0 to disable this check (any upper bound you could choose might fail unpredictably with minor updates to GHC, so disabling the check is recommended if you're sure that type checking should terminate) • In the second argument of ‘($)’, namely ‘(test_gr3)’ In the second argument of ‘($)’, namely ‘runInferenceT2 @TermType @Net $ (test_gr3)’ In the second argument of ‘($)’, namely ‘runInferenceT2 @InfLayers @'[Data, Type] $ runInferenceT2 @TermType @Net $ (test_gr3)’ }}} What is "funny" is that if I change the type of `test_gr3` to a very similar one, I just replace the part `=> m bind` with manually expanded one `m (Binding (PrimExpr2' t layers Star))` everything compiles fine. It would be really hard to get minimal example out of it – it uses nested mfixes and will take much time to cut it down. The question is – can we locate the error based on the description? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12734 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12734: Unexpected context reduction stack overflow -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 8.0.1 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: | -------------------------------------+------------------------------------- Comment (by simonpj): I know how hard it can be to boil out a repro case, but it's difficult to debug this kind of thing without it. One that might give some insight is to try `-ddump-cs-trace` which gives you soe idea of what the constraint solver is doing. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12734#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12734: Unexpected context reduction stack overflow -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 8.0.1 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: | -------------------------------------+------------------------------------- @@ -26,2 +26,2 @@ - test_gr3 = do - sref <- nstar3 + test_gr3 = nstar3 + New description: Hello! I don't have a minimal example, but I've got a very clear strange bahavior: We've got a function: {{{ nstar3 :: ( ExprCons t layers m, Bindable t m, Self.MonadSelfBuilder (Binding (Expr2 t layers AnyLayout)) m , ExprInferable t layers m) => m (Binding (PrimExpr2' t layers Star)) nstar3 = Self.put . anyLayout2 =<<& (nstar2 >>= mkBinding) }}} If I use it in a different function and use following explicit type, I get the error: {{{ test_gr3 :: ( ExprCons t layers m, Bindable t m, ExprInferable t layers m , MonadIO m, Show bind, Show (PrimExpr2' t layers Star), layers~'[Data, Type] , Self.MonadSelfBuilder (Binding (Expr2 t layers AnyLayout)) m , bind ~ Binding (PrimExpr2' t layers Star) ) => m bind test_gr3 = nstar3 }}} error (while using the function and evaluating monads): {{{ • Reduction stack overflow; size = 201 When simplifying the following type: MonadFix (Self.SelfBuilderT (Binding (Expr2 t0 '[Data, Type] AnyLayout)) m) Use -freduction-depth=0 to disable this check (any upper bound you could choose might fail unpredictably with minor updates to GHC, so disabling the check is recommended if you're sure that type checking should terminate) • In the second argument of ‘($)’, namely ‘(test_gr3)’ In the second argument of ‘($)’, namely ‘runInferenceT2 @TermType @Net $ (test_gr3)’ In the second argument of ‘($)’, namely ‘runInferenceT2 @InfLayers @'[Data, Type] $ runInferenceT2 @TermType @Net $ (test_gr3)’ }}} What is "funny" is that if I change the type of `test_gr3` to a very similar one, I just replace the part `=> m bind` with manually expanded one `m (Binding (PrimExpr2' t layers Star))` everything compiles fine. It would be really hard to get minimal example out of it – it uses nested mfixes and will take much time to cut it down. The question is – can we locate the error based on the description? -- Comment (by danilo2): I know @Simon, and I'll try to help as much as possible. When passing `-ddump-cs-trace` to stack as `--ghc-options` I don't get any additional compilation output - both in terminal as well in the stack compilation log file. Does anybody know if stack blocks it somehow? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12734#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12734: Unexpected context reduction stack overflow -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 8.0.1 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: | -------------------------------------+------------------------------------- Comment (by danilo2): Ok, @Simon: 1) There are some special cases using stack regarding how it outputs its dump files, the docs for stack have been updated: https://github.com/commercialhaskell/stack/issues/2720 2) I was cutting down the example this evening. It took some time, but I've got it. It could be probably much simpler, but I think it is small enough to put it here, so here goes the example file we can test to investigate the error! :) {{{ {-# LANGUAGE NoMonomorphismRestriction #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeApplications #-} module Main where import Prelude import Control.Applicative import Control.Monad.Fix import Control.Monad.Trans.Identity import Control.Monad.Trans data A data B data Net data Type data Layer4 t l data TermStore -- Helpers: Stack data Stack layers (t :: * -> *) where SLayer :: t l -> Stack ls t -> Stack (l ': ls) t SNull :: Stack '[] t instance ( Constructor m (t l) , Constructor m (Stack ls t)) => Constructor m (Stack (l ': ls) t) instance Monad m => Constructor m (Stack '[] t) -- Helpers: Expr newtype Expr t layers = Expr (TermStack t layers) type TermStack t layers = Stack layers (Layer4 (Expr t layers)) -- Helpers: Funny typeclass class Monad m => Constructor m t instance ( Monad m, expr ~ Expr t layers, Constructor m (TermStack t layers) ) => Constructor m (Layer4 expr Type) -- HERE IS A FUNNY BEHAVIOR: the commented line raises context reduction stack overflow test_gr :: ( Constructor m (TermStack t layers), Inferable A layers m, Inferable B t m , bind ~ Expr t layers -- ) => m (Expr t layers) ) => m bind test_gr = undefined -- Explicit information about a type which could be infered class Monad m => Inferable (cls :: *) (t :: k) m | cls m -> t newtype KnownTypex (cls :: *) (t :: k) (m :: * -> *) (a :: *) = KnownTypex (IdentityT m a) deriving (Show, Functor, Monad, MonadIO, MonadFix, MonadTrans, Applicative, Alternative) instance {-# OVERLAPPABLE #-} (t ~ t', Monad m) => Inferable cls t (KnownTypex cls t' m) instance {-# OVERLAPPABLE #-} (Inferable cls t n, MonadTrans m, Monad (m n)) => Inferable cls t (m n) runInferenceTx :: forall cls t m a. KnownTypex cls t m a -> m a runInferenceTx = undefined -- running it test_ghc_err :: (MonadIO m, MonadFix m) => m (Expr Net '[Type]) test_ghc_err = runInferenceTx @B @Net $ runInferenceTx @A @'[Type] $ (test_gr) main :: IO () main = return () }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12734#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12734: Unexpected context reduction stack overflow -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by danilo2): * failure: None/Unknown => GHC rejects valid program -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12734#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12734: Unexpected context reduction stack overflow -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Terrific. I can reproduce, thank you. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12734#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12734: Unexpected context reduction stack overflow -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by danilo2): That's strange – maybe we're using some strange pattern, but our team is getting this error very often recently and we're using hacks to make it working just by expanding variables to full types. In this case I'll raise the priority of this bug. If anyone don't agree, feel free to lower it – it just slows down our workflow much. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12734#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12734: Unexpected context reduction stack overflow -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: Type: bug | Status: new Priority: highest | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by danilo2): * priority: high => highest -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12734#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12734: Unexpected context reduction stack overflow -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by mpickering): * priority: highest => high Comment: @danilo2 Could one of your team perhaps investigate this problem further? If you want it to be quickly fixed then an analysis of what is going on would be very helpful. I don't think this should be marked as highest priority as that is usually reserved for released blocking bugs. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12734#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12734: Missed use of solved dictionaries leads to context stack overflow -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Here's a cut-down version: {{{ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE NoMonomorphismRestriction #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeApplications #-} module T12734 where import Prelude import Control.Applicative import Control.Monad.Fix import Control.Monad.Trans.Identity import Control.Monad.Trans.Class import Control.Monad.IO.Class data A data B data Net data Type data Layer4 t l data TermStore -- Helpers: Stack data Stack lrs (t :: * -> *) where SLayer :: t l -> Stack ls t -> Stack (l ': ls) t SNull :: Stack '[] t instance ( Con m (t l) , Con m (Stack ls t)) => Con m (Stack (l ': ls) t) instance Monad m => Con m (Stack '[] t) instance ( expr ~ Expr t lrs , Con m (TStk t lrs)) => Con m (Layer4 expr Type) newtype Expr t lrs = Expr (TStk t lrs) type TStk t lrs = Stack lrs (Layer4 (Expr t lrs)) class Con m t -- HERE IS A FUNNY BEHAVIOR: the commented line raises context reduction stack overflow test_gr :: forall m t lrs bind. ( Con m (TStk t lrs) , bind ~ Expr t lrs -- ) => m (Expr t lrs) -- Works with this line ) => m bind -- Does not work with this line test_gr = undefined newtype KT (cls :: *) (t :: k) (m :: * -> *) (a :: *) = KT (IdentityT m a) test_ghc_err :: KT A '[Type] IO (Expr Net '[Type]) test_ghc_err = test_gr @(KT A '[Type] IO) @_ @'[Type] @(Expr Net '[Type]) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12734#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12734: Missed use of solved dictionaries leads to context stack overflow -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): OK I know what is going on. With the cut-down example above, when checking the cod for `test_ghc_err` we are faced with {{{ [W] Con m (TStk t lrs) where m := KT A '[Type] IO bind := Expr Net '[Type] t := Net lrs := '[Type] }}} The `:=` are unifications that can take place pretty eagerly. Now let's try solving that wanted constraint {{{ [W] Con m (TStk t lrs) = (Type synonym) [W] Con m (Stack lrs (Layer4 bind)) = (inline lrs) [W] Con m (Stack '[Type] (Layer4 bind)) --> instance decl for (Con m (Stack (l :' ls) t)) [W] Con m (Stack '[] bind) [W] Con m (Layer4 bind Type) The first of these rapidly reduces to (Monad m). The second is harder: [W] Con m (Layer4 bind Type) --> instance decl for (Con m (Layer4 expr Type) [W] bind ~ Expr t0 lrs0 -- C1 [W] Con m (TStk t0 lrs0) -- C2 where t0, lrs0 are fresh unification variables. If we simplify (C1), using the fact that bind := Expr Net '[Type] we get t0 := Net lrs0 := lrs And now we have (C2): [W] Con m (TStk Net lrs) which is the very same thing we start with. So we can "tie the knot" via the `inert_solved_dicts` and we are done. }}} This makes essential use of GHC's ability to solve a set of constraints with a ''recursive'' dictionary binding. So what goes wrong? * If we fail to prioritise C1 over C2, we'll embark on simplifying C2, not spotting the loop. Result: an infinite regress. * We do prioritise equality constraints * But C1, namely `bind ~ Expr t0 lrs0` is actually a ''class'' constraint, not an equality. It has a built-in reduction to the homogeneous-equality class constraint `bind ~~ Expr t0 lrs0`; and that in turn has a built-in reduction to the true equality constraint `bind ~# Expr t0 lrs0`. So a solution that works is to prioritise the two equality-class constraints `t1 ~ t2` and `t1 ~~ t2` just as we do equality constraints. That's a good thing to do anyway. But I'm concerned that it does not truly solve the problem. Two worries: * To "tie the knot" we rely on saying "I've see this goal before". But to be sure of that we should rewrite `inert_solved_dicts` with the current substitution, and currently we don't do that. Maybe we should. It's more work but we might in exchange sometimes get more sharing. * What if we have a class constraint `(C t1 t2)` where C has a perhaps- distant superclass `(s1 ~ s2)`. Then should we prioritise the `(C t1 t2)` constraint? But the superclass might not even be revealed until we do some reduction on `(C t1 t2)`. This way lies madness. I think wes should not even attempt to do this. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12734#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12734: Missed use of solved dictionaries leads to context stack overflow
-------------------------------------+-------------------------------------
Reporter: danilo2 | Owner:
Type: bug | Status: new
Priority: high | Milestone:
Component: Compiler | Version: 8.0.1
Resolution: | Keywords:
Operating System: Unknown/Multiple | Architecture:
Type of failure: GHC rejects | Unknown/Multiple
valid program | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Simon Peyton Jones
#12734: Missed use of solved dictionaries leads to context stack overflow -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): danilo2: maybe try HEAD? Should be fixed, I hope. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12734#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12734: Missed use of solved dictionaries leads to context stack overflow -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by danilo2): simonpj: thank you for a fast fix, I'm building head at the moment and I'll try it here! By the way, based on your description it reminded me about other bug I filled some time ago. Do you think it could be connected? It is not a high priority bug, but if it's connected maybe it's worth to mention it: https://ghc.haskell.org/trac/ghc/ticket/10778 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12734#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
By the way, based on your description it reminded me about other bug I filled some time ago. Do you think it could be connected? It is not a high
#12734: Missed use of solved dictionaries leads to context stack overflow -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): priority bug, but if it's connected maybe it's worth to mention it: #10778 It's not connected, but it's already fixed! I also discovered #12803 in my travels -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12734#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC