#11379: Solver hits iteration limit in code without recursive constraints -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: highest | Milestone: 8.0.1 Component: Compiler | Version: 8.0.1-rc1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple performance bug | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by bgamari: Old description:

This example (derived from `xmonad-contrib`) failed to compile with `master`,

{{{#!hs {-# LANGUAGE ExistentialQuantification, RankNTypes, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, FlexibleContexts #-}

module XMonad.Layout.MultiToggle where

import Data.Typeable

-- This appears to be the culprit expand :: (HList ts a) => MultiToggleS ts l a -> MultiToggle ts l a expand (MultiToggleS b ts) = resolve ts id (\x mt -> let g = transform' x in mt{ currLayout = g $ currLayout mt }) (MultiToggle (EL b id) ts)

class (Typeable t) => Transformer t a | t -> a where transform :: t -> l a -> (forall l'. l' a -> (l' a -> l a) -> b) -> b

data EL l a = forall l'. EL (l' a) (l' a -> l a)

transform' :: (Transformer t a) => t -> EL l a -> EL l a transform' t (EL l det) = undefined

data MultiToggleS ts l a = MultiToggleS (l a) ts deriving (Read, Show)

data MultiToggle ts l a = MultiToggle{ currLayout :: EL l a, transformers :: ts }

class HList c a where resolve :: c -> b -> (forall t. (Transformer t a) => t -> b) -> b }}}

failing during constraint solving with,,

{{{ XMonad/Layout/MultiToggle.hs:1:1: error: solveWanteds: too many iterations (limit = 4) Unsolved: WC {wc_simple = [D] _ :: Transformer t a (CDictCan) [D] _ :: a_aIoy ~ a (CNonCanonical) [D] _ :: Typeable t (CDictCan) wc_impl = Implic { TcLevel = 7 Skolems = (l :: * -> *) No-eqs = True Status = Unsolved Given = Wanted = WC {wc_simple = [W] $dTransformer_aIoM :: Transformer t a (CDictCan)} Binds = Just EvBindsVar<aIoN> the inferred type of g :: EL l_aIoL a_aIoK -> EL l_aIoL a_aIoK }} New superclasses found Set limit with -fconstraint-solver-iterations=n; n=0 for no limit }}}

Lifting the solver iteration limit just results in a loop.

I suspect the issue may be in the `Typeable` solving logic, as removing the `Typable` constraint from `Transformer`'s head allows compilation to proceed.

New description: This example (derived from `xmonad-contrib`) failed to compile with `master`, {{{#!hs {-# LANGUAGE ExistentialQuantification, RankNTypes, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, FlexibleContexts #-} module XMonad.Layout.MultiToggle where import Data.Typeable -- This appears to be the culprit expand :: (HList ts a) => MultiToggleS ts l a -> MultiToggle ts l a expand (MultiToggleS b ts) = resolve ts id (\x mt -> let g = transform' x in mt{ currLayout = g $ currLayout mt }) (MultiToggle (EL b id) ts) -- Removing the Typeable constraint here allows compilation to finish class (Typeable t) => Transformer t a | t -> a where transform :: t -> l a -> (forall l'. l' a -> (l' a -> l a) -> b) -> b data EL l a = forall l'. EL (l' a) (l' a -> l a) transform' :: (Transformer t a) => t -> EL l a -> EL l a transform' t (EL l det) = undefined data MultiToggleS ts l a = MultiToggleS (l a) ts deriving (Read, Show) data MultiToggle ts l a = MultiToggle{ currLayout :: EL l a, transformers :: ts } class HList c a where resolve :: c -> b -> (forall t. (Transformer t a) => t -> b) -> b }}} failing during constraint solving with,, {{{ XMonad/Layout/MultiToggle.hs:1:1: error: solveWanteds: too many iterations (limit = 4) Unsolved: WC {wc_simple = [D] _ :: Transformer t a (CDictCan) [D] _ :: a_aIoy ~ a (CNonCanonical) [D] _ :: Typeable t (CDictCan) wc_impl = Implic { TcLevel = 7 Skolems = (l :: * -> *) No-eqs = True Status = Unsolved Given = Wanted = WC {wc_simple = [W] $dTransformer_aIoM :: Transformer t a (CDictCan)} Binds = Just EvBindsVar<aIoN> the inferred type of g :: EL l_aIoL a_aIoK -> EL l_aIoL a_aIoK }} New superclasses found Set limit with -fconstraint-solver-iterations=n; n=0 for no limit }}} Lifting the solver iteration limit just results in a loop. I suspect the issue may be in the `Typeable` solving logic, as removing the `Typable` constraint from `Transformer`'s head allows compilation to proceed. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11379#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11379: Solver hits iteration limit in code without recursive constraints -------------------------------------+------------------------------------- Reporter: bgamari | Owner: simonpj Type: bug | Status: new Priority: highest | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple performance bug | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * owner: => simonpj Comment: I'm on this. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11379#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11379: Solver hits iteration limit in code without recursive constraints -------------------------------------+------------------------------------- Reporter: bgamari | Owner: simonpj Type: bug | Status: merge Priority: highest | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple performance bug | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => merge Comment: Actually this ticket #11is fixed by the following commit. I forgot to mention it in the list of fixes in the commit message. The important bit of the patch for #11379 is the new function `TcSMonad.mkShadowCt`, explained by `Note [Keep CDictCan shadows as CDictCan]`. Let's merge this. {{{ commit 9308c736d43b92bf8634babf565048e66e071bd8 Author: Simon Peyton Jones Date: Sat Jan 16 00:37:15 2016 +0000 Fix a number of subtle solver bugs As a result of some other unrelated changes I found that IndTypesPerf was failing, and opened Trac #11408. There's a test in indexed-types/should-compile/T11408. The bug was that a type like forall t. (MT (UL t) (UR t) ~ t) => UL t -> UR t -> Int is in fact unambiguous, but it's a bit subtle to prove that it is unambiguous. In investigating, Dimitrios and I found several subtle bugs in the constraint solver, fixed by this patch * canRewrite was missing a Derived/Derived case. This was lost by accident in Richard's big kind-equality patch. * Interact.interactTyVarEq would discard [D] a ~ ty if there was a [W] a ~ ty in the inert set. But that is wrong because the former can rewrite things that the latter cannot. Fix: a new function eqCanDischarge * In TcSMonad.addInertEq, the process was outright wrong for a Given/Wanted in the (GWModel) case. We were adding a new Derived without kicking out things that it could rewrite. Now the code is simpler (no special GWModel case), and works correctly. * The special case in kickOutRewritable for [W] fsk ~ ty, turns out not to be needed. (We emit a [D] fsk ~ ty which will do the job. I improved comments and documentation, esp in TcSMonad. }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11379#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11379: Solver hits iteration limit in code without recursive constraints -------------------------------------+------------------------------------- Reporter: bgamari | Owner: simonpj Type: bug | Status: closed Priority: highest | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple performance bug | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: merge => closed * resolution: => fixed Comment: This was merged to `ghc-8.0` as 9f466c8841c7ddda84951c9e3470540d25d0bfdb. The test will be merged shortly. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11379#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11379: Solver hits iteration limit in code without recursive constraints -------------------------------------+------------------------------------- Reporter: bgamari | Owner: simonpj Type: bug | Status: closed Priority: highest | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple performance bug | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Neil, thank you. You have found a much more serious and quite unrelated bug, which I've created as #11458. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11379#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler