Ticket #3108 (closed bug: fixed)

Opened 4 years ago

Last modified 14 months ago

Do a better job of solving recursive type-class constraints with functional dependencies

Reported by: simonpj Owned by:
Priority: high Milestone: 7.6.1
Component: Compiler (Type checker) Version: 6.10.1
Keywords: Cc: dimitris@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Difficulty: Unknown
Test Case: typecheck/should_compile/T3108.hs Blocked By:
Blocking: Related Tickets:

Description

This ticket is just to track this interesting thread on the Haskell list, concerning recursive type-class constraints:  http://www.haskell.org/pipermail/haskell/2009-March/021115.html. We might want to get back to this when the new constraint solver is in place.

The question concerns the interaction of solving recursive type-class constraints, where it is important to aggressively apply functional dependencies. Here's Tom Schrijvers's analysis of Ralf's example:

"The cyclic dictionaries approach is a bit fragile. The problem appears to be here that GHC alternates exhaustive phases of constraint reduction and functional dependency improvement. The problem is that in your example you need both for detecting a cycle.

This can happen:

        C1 Int
        ==> 3rd C1 inst
        C2 Int y, C1 (y,Bool)
        ==> 1st C1 inst
        C2 Int y, C1 y, C1 Bool
        ==> 2nd C1 inst
        C2 Int y, C1 y
        ==> 3rd C1 inst
        C2 Int y, C2 y z, C1 (z,Bool)
        ==>
        ...

where all the constraint are different because fresh variables are introduced.

What you want to happen is:

        C1 Int
        ==> 3rd C1 inst
        C2 Int y, C1 (y,Bool)
        ==> 1st C1 inst
        C2 Int y, C1 y, C1 Bool
        ==> 2nd C1 inst
        C2 Int y, C1 y
        ==> C2 FD improvement {Int/y}  <<<<
        C2 Int Int, C1 Int
        ==> C1 Int cycle detected
        C2 Int Int
        ==> C2 1st instance
        {}

It seems that you want improvement to happen at a higher priority than GHC does now."

Change History

Changed 3 years ago by igloo

  • milestone changed from 6.12 branch to 6.12.3

Changed 3 years ago by igloo

  • priority changed from normal to low
  • milestone changed from 6.12.3 to 6.14.1

Changed 2 years ago by igloo

  • milestone changed from 7.0.1 to 7.0.2

Changed 2 years ago by igloo

  • milestone changed from 7.0.2 to 7.2.1

Changed 20 months ago by igloo

  • milestone changed from 7.2.1 to 7.4.1

Changed 16 months ago by igloo

  • priority changed from low to lowest
  • milestone changed from 7.4.1 to 7.6.1

Changed 14 months ago by simonpj

  • cc dimitris@… added
  • failure set to None/Unknown
  • priority changed from lowest to high

With the new constraint solver we an ASSERT error for this program:

{-# LANGUAGE OverlappingInstances, UndecidableInstances, MultiParamTypeClasses, 
             FunctionalDependencies, FlexibleInstances #-}

module T3108 where

-- Direct recursion terminates (typechecking-wise)

class C0 x
 where
 m0 :: x -> ()
 m0 = const undefined

instance (C0 x, C0 y) => C0 (x,y)
instance C0 Bool
instance C0 (x,Bool) => C0 x

foo :: ()
foo = m0 (1::Int)


-- Indirect recursion does not terminate (typechecking-wise)

class C1 x
 where
 m1 :: x -> ()
 m1 = const undefined

instance (C1 x, C1 y) => C1 (x,y)
instance C1 Bool
instance (C2 x y, C1 (y,Bool)) => C1 x

class C2 x y | x -> y
instance C2 Int Int

-- It is this declaration that causes nontermination of typechecking.
bar :: ()
bar = m1 (1::Int)

Thus:

simonpj@cam-05-unx:~/tmp$ ~/5builds/HEAD/inplace/bin/ghc-stage1 -c T3108.hs -dcore-lint -fforce-recomp
setEvBind
    Cycle in evidence binds, evvar = $dC1{v aep} [lid]
    {$dC1{v adw} [lid]
       = main:T3108.$fC1x{v r1} [lidx[DFunId(nt)]] @[ghc-prim:GHC.Types.Int{(w) tc 3J},
                                                     y{tv aej} [tcs]]
                                                   [$dC2{v aek} [lid], $dC1{v ael} [lid]],
     $dC2{v aek} [lid]
       = $dC2{v aeo} [lid] `cast` (main:T3108.C2{tc r7}
                                     <ghc-prim:GHC.Types.Int{(w) tc 3J}> (Sym cobox{v aen} [lid])),
     $dC1{v ael} [lid]
       = $dC1{v aep} [lid] `cast` (main:T3108.C1{tc r9}
                                     (Sym cobox{v aen} [lid],
                                      <ghc-prim:GHC.Types.Bool{(w) tc 3c}>)),
     cobox{v aen} [lid] = CO <ghc-prim:GHC.Types.Int{(w) tc 3J}>,
     $dC2{v aeo} [lid]
       = main:T3108.$fC2IntInt{v r0} [lidx[DFunId]] @[] [],
     $dC1{v aep} [lid]
       = main:T3108.$fC1(,){v r3} [lidx[DFunId(nt)]] @[ghc-prim:GHC.Types.Int{(w) tc 3J},
                                                       ghc-prim:GHC.Types.Bool{(w) tc 3c}]
                                                     [$dC1{v adw} [lid], $dC1{v aeq} [lid]]}
setEvBind
    Cycle in evidence binds, evvar = $dC0{v aer} [lid]
    {$dC1{v adw} [lid]
       = main:T3108.$fC1x{v r1} [lidx[DFunId(nt)]] @[ghc-prim:GHC.Types.Int{(w) tc 3J},
                                                     y{tv aej} [tcs]]
                                                   [$dC2{v aek} [lid], $dC1{v ael} [lid]],
     $dC0{v ady} [lid]
       = main:T3108.$fC0x{v r4} [lidx[DFunId(nt)]] @[ghc-prim:GHC.Types.Int{(w) tc 3J}]
                                                   [$dC0{v aer} [lid]],
     $dC2{v aek} [lid]
       = $dC2{v aeo} [lid] `cast` (main:T3108.C2{tc r7}
                                     <ghc-prim:GHC.Types.Int{(w) tc 3J}> (Sym cobox{v aen} [lid])),
     $dC1{v ael} [lid]
       = $dC1{v aep} [lid] `cast` (main:T3108.C1{tc r9}
                                     (Sym cobox{v aen} [lid],
                                      <ghc-prim:GHC.Types.Bool{(w) tc 3c}>)),
     cobox{v aen} [lid] = CO <ghc-prim:GHC.Types.Int{(w) tc 3J}>,
     $dC2{v aeo} [lid]
       = main:T3108.$fC2IntInt{v r0} [lidx[DFunId]] @[] [],
     $dC1{v aep} [lid]
       = main:T3108.$fC1(,){v r3} [lidx[DFunId(nt)]] @[ghc-prim:GHC.Types.Int{(w) tc 3J},
                                                       ghc-prim:GHC.Types.Bool{(w) tc 3c}]
                                                     [$dC1{v adw} [lid], $dC1{v aeq} [lid]],
     $dC1{v aeq} [lid]
       = main:T3108.$fC1Bool{v r2} [lidx[DFunId(nt)]] @[] [],
     $dC0{v aer} [lid]
       = main:T3108.$fC0(,){v r6} [lidx[DFunId(nt)]] @[ghc-prim:GHC.Types.Int{(w) tc 3J},
                                                       ghc-prim:GHC.Types.Bool{(w) tc 3c}]
                                                     [$dC0{v ady} [lid], $dC0{v aes} [lid]]}
simonpj@cam-05-unx:~/tmp$ ~/5builds/HEAD/inplace/bin/ghc-stage1 -c T3108.hs -dcore-lint -fforce-recomp
setEvBind
    Cycle in evidence binds, evvar = $dC1{v aep} [lid]
    {$dC1{v adw} [lid]
       = main:T3108.$fC1x{v r1} [lidx[DFunId(nt)]] @[ghc-prim:GHC.Types.Int{(w) tc 3J},
                                                     y{tv aej} [tcs]]
                                                   [$dC2{v aek} [lid], $dC1{v ael} [lid]],
     $dC2{v aek} [lid]
       = $dC2{v aeo} [lid] `cast` (main:T3108.C2{tc r7}
                                     <ghc-prim:GHC.Types.Int{(w) tc 3J}> (Sym cobox{v aen} [lid])),
     $dC1{v ael} [lid]
       = $dC1{v aep} [lid] `cast` (main:T3108.C1{tc r9}
                                     (Sym cobox{v aen} [lid],
                                      <ghc-prim:GHC.Types.Bool{(w) tc 3c}>)),
     cobox{v aen} [lid] = CO <ghc-prim:GHC.Types.Int{(w) tc 3J}>,
     $dC2{v aeo} [lid]
       = main:T3108.$fC2IntInt{v r0} [lidx[DFunId]] @[] [],
     $dC1{v aep} [lid]
       = main:T3108.$fC1(,){v r3} [lidx[DFunId(nt)]] @[ghc-prim:GHC.Types.Int{(w) tc 3J},
                                                       ghc-prim:GHC.Types.Bool{(w) tc 3c}]
                                                     [$dC1{v adw} [lid], $dC1{v aeq} [lid]]}
setEvBind
    Cycle in evidence binds, evvar = $dC0{v aer} [lid]
    {$dC1{v adw} [lid]
       = main:T3108.$fC1x{v r1} [lidx[DFunId(nt)]] @[ghc-prim:GHC.Types.Int{(w) tc 3J},
                                                     y{tv aej} [tcs]]
                                                   [$dC2{v aek} [lid], $dC1{v ael} [lid]],
     $dC0{v ady} [lid]
       = main:T3108.$fC0x{v r4} [lidx[DFunId(nt)]] @[ghc-prim:GHC.Types.Int{(w) tc 3J}]
                                                   [$dC0{v aer} [lid]],
     $dC2{v aek} [lid]
       = $dC2{v aeo} [lid] `cast` (main:T3108.C2{tc r7}
                                     <ghc-prim:GHC.Types.Int{(w) tc 3J}> (Sym cobox{v aen} [lid])),
     $dC1{v ael} [lid]
       = $dC1{v aep} [lid] `cast` (main:T3108.C1{tc r9}
                                     (Sym cobox{v aen} [lid],
                                      <ghc-prim:GHC.Types.Bool{(w) tc 3c}>)),
     cobox{v aen} [lid] = CO <ghc-prim:GHC.Types.Int{(w) tc 3J}>,
     $dC2{v aeo} [lid]
       = main:T3108.$fC2IntInt{v r0} [lidx[DFunId]] @[] [],
     $dC1{v aep} [lid]
       = main:T3108.$fC1(,){v r3} [lidx[DFunId(nt)]] @[ghc-prim:GHC.Types.Int{(w) tc 3J},
                                                       ghc-prim:GHC.Types.Bool{(w) tc 3c}]
                                                     [$dC1{v adw} [lid], $dC1{v aeq} [lid]],
     $dC1{v aeq} [lid]
       = main:T3108.$fC1Bool{v r2} [lidx[DFunId(nt)]] @[] [],
     $dC0{v aer} [lid]
       = main:T3108.$fC0(,){v r6} [lidx[DFunId(nt)]] @[ghc-prim:GHC.Types.Int{(w) tc 3J},
                                                       ghc-prim:GHC.Types.Bool{(w) tc 3c}]
                                                     [$dC0{v ady} [lid], $dC0{v aes} [lid]]}

Changed 14 months ago by simonpj

Turns out that the new constraint solver is doing the Right Thing; but it has a pprTrace that emits messages when it should not.

Dimitrios, can you

  • Commit the fix to pprTrace?
  • Add the above program to the testsuite, in typecheck/should_compile?

Thanks

Simon

Changed 14 months ago by dimitris

  • testcase set to typecheck/should_compile/T3108.hs

Done, part of the bigger commit: f15977c24f2ec96ea324cc7e8122f17ffe8b931c Also test added in typecheck/should_compile.

Changed 14 months ago by simonmar

dimitris: you left the ticket open, should it be closed now?

Changed 14 months ago by dimitris

  • status changed from new to closed
  • resolution set to fixed

Yes, fixed. Sorry.

Note: See TracTickets for help on using tickets.