Opened 2 years ago

Closed 2 years ago

Last modified 23 months ago

#11379 closed bug (fixed)

Solver hits iteration limit in code without recursive constraints

Reported by: bgamari Owned by: simonpj
Priority: highest Milestone: 8.0.1
Component: Compiler (Type checker) Version: 8.0.1-rc1
Keywords: Cc: hvr, simonpj, slyfox, ndmitchell
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Compile-time performance bug Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by bgamari)

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

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

Change History (10)

comment:1 Changed 2 years ago by bgamari

Summary: New superclass solver fails to compileSolver hits iteration limit in code without recursive constraints

comment:2 Changed 2 years ago by bgamari

Description: modified (diff)

comment:3 Changed 2 years ago by hvr

Cc: hvr simonpj added
Component: CompilerCompiler (Type checker)

comment:4 Changed 2 years ago by simonpj

Owner: set to simonpj

I'm on this.

comment:5 Changed 2 years ago by slyfox

Cc: slyfox added

comment:6 Changed 2 years ago by simonpj

Status: newmerge

Actually this ticket #11379 is 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 <simonpj@microsoft.com>
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.
Last edited 2 years ago by simonpj (previous) (diff)

comment:7 Changed 2 years ago by Simon Peyton Jones <simonpj@…>

In 8e50301f/ghc:

Test Trac #11379

comment:8 Changed 2 years ago by bgamari

Resolution: fixed
Status: mergeclosed

This was merged to ghc-8.0 as 9f466c8841c7ddda84951c9e3470540d25d0bfdb.

The test will be merged shortly.

comment:9 Changed 2 years ago by NeilMitchell

Cc: ndmitchell added

For info, I found a similar bug while trying Shake with GHC 8.0-rc1 provided by hvr (8.0.0.20160111+git.0.497454f). Chopping out the relevant bit leaves:

-- optIntArg :: (Ord a0, Read a0, Show a0) => a0 -> [Char] -> t0 -> (Maybe a0 -> t2) -> Maybe String -> Either [Char] ([t1], t2)
optIntArg mn flag a f = maybe (Right ([], f Nothing)) $ \x -> case reads x of
    [(i,"")] | i >= mn -> Right ([],f $ Just i)
    _ -> Left $ "the `--" ++ flag ++ "' option requires a number, " ++ show mn ++ " or above"

Uncommenting the type signature makes it work. Without, it fails with:

    solveWanteds: too many iterations (limit = 4)
      Unsolved: WC {wc_simple =
                      [D] _ :: Eq a (CDictCan)
                      [D] _ :: Ord a (CDictCan)
                      [D] _ :: Read a (CDictCan)
                      [D] _ :: Show a (CDictCan)
                      [W] hole{a5xW} :: a ~ a (CNonCanonical)
                      [D] _ :: Eq a (CDictCan)}
      New superclasses found
      Set limit with -fconstraint-solver-iterations=n; n=0 for no limit]

Given the size of the code fragment that triggers it, and the fact a number of bugs were found, this might be another useful test case.

Tweaking to give:

optIntArg mn flag a f = maybe (Right ([], f Nothing)) $ \x -> case reads x of
    [(i,"")] | i == mn -> Right ([],f $ Just i)
    _ -> Left $ "the `--" ++ flag ++ "' option requires a number, or above"

I end up with a very different error:

src\Demo.hs:5:41: error:
    * Couldn't match type `a' with `a1'
        because type variable `a1' would escape its scope
      This (rigid, skolem) type variable is bound by
        a type expected by the context:
          Maybe a1
        at src\Demo.hs:5:37-46
      Expected type: Maybe a1
        Actual type: Maybe a

This code compiles fine with GHC 7.10, so seems like a different bug, or different manifestation of the same bug.

comment:10 Changed 23 months ago by simonpj

Neil, thank you. You have found a much more serious and quite unrelated bug, which I've created as #11458.

Simon

Note: See TracTickets for help on using tickets.