Re: [GHC] #11379: Solver hits iteration limit in code without recursive constraints

8 Jan 2016

      #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