Opened 8 years ago

Closed 8 years ago

#1353 closed bug (invalid)

GHCi hangs when type checking

Reported by: matthew@… Owned by:
Priority: normal Milestone:
Component: GHCi Version: 6.6
Keywords: Cc:
Operating System: Linux Architecture: x86
Type of failure: Test Case:
Blocked By: Blocking:
Related Tickets: Differential Revisions:

Description

Firstly, apologies for posting such a lot of code.

roconnor on #haskell said that the use of Mu might be giving grief to ghc due to inlining but then that looks like it's a compilation rather than a type checking issue.

Just to give you some context, the code is an implementation of session types in haskell. The implementation of recursion is operationally broken, but I just wanted it to type check.

The behaviour is interesting (this is on GHC 6.6):

*Session> :t let p1 = Proc $ mkLoop (recvLog >~> returnS ()) in p1
let p1 = Proc $ mkLoop (recvLog >~> returnS ()) in p1 :: (UnrollLoop (SessionSpec (Loop (SessionSpec il)))
            (SessionSpec (SessT t (Loop (SessionSpec il)))),
 UnrollLoop (SessionSpec (Loop (SessionSpec ol)))
            (SessionSpec (Loop (SessionSpec ol))),
 UnrollLoop (SessionSpec (Loop (SessionSpec s)))
            (SessionSpec (RecvT t (Loop (SessionSpec s)))),
 Show t,
 JustSendsRecvs (SessionSpec (RecvT t (Loop (SessionSpec s))))
                (SessionSpec (Loop (SessionSpec ol)))
                (SessionSpec (SessT t (Loop (SessionSpec il)))),
 JustSendsRecvs (SessionSpec (Loop (SessionSpec s)))
                (SessionSpec (Loop (SessionSpec ol)))
                (SessionSpec (Loop (SessionSpec il))),
 ZeroOrMoreSteps (SessionSpec (Loop (SessionSpec s)))
                 (SessionSpec EndT)) =>
Proc (SessionSpec (Loop (SessionSpec s)))
     (SessionSpec EndT)
     (Loop (SessionSpec ol))
     EndT
     (Loop (SessionSpec il))
     EndT

and

*Session> :t let p2 = Proc $ mkLoop (sendLog 'c') in p2
let p2 = Proc $ mkLoop (sendLog 'c') in p2 :: (UnrollLoop (SessionSpec (Loop (SessionSpec il)))
            (SessionSpec (Loop (SessionSpec il))),
 UnrollLoop (SessionSpec (Loop (SessionSpec ol)))
            (SessionSpec (SessT Char (Loop (SessionSpec ol)))),
 UnrollLoop (SessionSpec (Loop (SessionSpec s)))
            (SessionSpec (SendT Char (Loop (SessionSpec s)))),
 JustSendsRecvs (SessionSpec (SendT Char (Loop (SessionSpec s))))
                (SessionSpec (SessT Char (Loop (SessionSpec ol))))
                (SessionSpec (Loop (SessionSpec il))),
 JustSendsRecvs (SessionSpec (Loop (SessionSpec s)))
                (SessionSpec (Loop (SessionSpec ol)))
                (SessionSpec (Loop (SessionSpec il))),
 ZeroOrMoreSteps (SessionSpec (Loop (SessionSpec s)))
                 (SessionSpec EndT)) =>
Proc (SessionSpec (Loop (SessionSpec s)))
     (SessionSpec EndT)
     (Loop (SessionSpec ol))
     EndT
     (Loop (SessionSpec il))
     EndT

but then

*Session> :t let p1 = Proc $ mkLoop (recvLog >~> returnS ()); p2 = Proc $ mkLoop (sendLog 'c') in 1
...endless hang which eats RAM...

allow-undecidable-instances is on and it's been suggested that it's that, but there's no blow up of the context-stack. I'm not sure I see why p1 and p2 are decidable on their own but not together.

However, on today's HEAD (20070514), all of these cases hang GHCi.

Ultimately, the following should typecheck:

*Session> :t runSessionWithProcs (mkLoopS (RecvS CharS)) (Proc $ mkLoop (recvLog >~> returnS ())) (Proc $ mkLoop (sendLog 'c'))

which again, currently causes a hang with both 6.6 and HEAD.

Attachments (3)

Session.hs (18.7 KB) - added by matthew@… 8 years ago.
The Magic Code
SessionWithList.hs (18.3 KB) - added by matthew@… 8 years ago.
No Mu, no recursive ADT but an infinite list.
SessionPruned.hs (9.2 KB) - added by matthew@… 8 years ago.
Starting to get it smaller…

Download all attachments as: .zip

Change History (9)

Changed 8 years ago by matthew@…

The Magic Code

comment:1 Changed 8 years ago by simonpj

I don't have time to look at the details today (perhaps someone can boil down to a smaller test case), but it smells as though your bug may be another instance of this:
http://www.haskell.org/ghc/docs/latest/html/users_guide/bugs.html#bugs-ghc
(third bullet).

Simon

comment:2 Changed 8 years ago by matthew@…

Condensing it is going to be painful. I'll work through it tonight and replace the Mu with standard recursive data types and see if that makes it go away.

comment:3 Changed 8 years ago by matthew@…

I've taken out the Mu. I then tried with a standard recursive data type and that produced no joy. I then replaced that with an infinite list (version attached).

GHC 6.6:

*Session> :t mkLoop (recvLog >~> returnS ())
mkLoop (recvLog >~> returnS ()) :: (Show t,
 JustSendsRecvs (SessionSpec (Loop (SessionSpec s)))
                (SessionSpec (Loop (SessionSpec ol)))
                (SessionSpec (Loop (SessionSpec il))),
 JustSendsRecvs (SessionSpec (RecvT t (Loop (SessionSpec s))))
                (SessionSpec (Loop (SessionSpec ol)))
                (SessionSpec (SessT t (Loop (SessionSpec il)))),
 UnrollLoop (SessionSpec (Loop (SessionSpec il)))
            (SessionSpec (SessT t (Loop (SessionSpec il)))),
 UnrollLoop (SessionSpec (Loop (SessionSpec ol)))
            (SessionSpec (Loop (SessionSpec ol))),
 UnrollLoop (SessionSpec (Loop (SessionSpec s)))
            (SessionSpec (RecvT t (Loop (SessionSpec s))))) =>
SessionState (SessionSpec (Loop (SessionSpec s)))
             (Loop (SessionSpec ol))
             (Loop (SessionSpec il))
-> IO ((), SessionState (SessionSpec EndT) EndT EndT)

ghc 20070514:

*Session> :t mkLoop (recvLog >~> returnS ())
mkLoop (recvLog >~> returnS ()) :: (ReplaceLoopEnd
                                      (SessionSpec il)
                                      (SessionSpec (Loop (SessionSpec il)))
                                      (SessionSpec (SessT t (Loop (SessionSpec il)))),
                                    ReplaceLoopEnd
                                      (SessionSpec ol)
                                      (SessionSpec (Loop (SessionSpec ol)))
                                      (SessionSpec [SessionSpec ol]),
                                    ReplaceLoopEnd
                                      (SessionSpec s)
                                      (SessionSpec (Loop (SessionSpec s)))
                                      (SessionSpec (RecvT t (Loop (SessionSpec s)))),
                                    Show t,
                                    JustSendsRecvs (SessionSpec s) (SessionSpec ol) (SessionSpec il)) =>
                                   SessionState
                                     (SessionSpec (Loop (SessionSpec s)))
                                     (Loop (SessionSpec ol))
                                     (Loop (SessionSpec il))
                                   -> IO ((), SessionState (SessionSpec EndT) EndT EndT)

so the new one is expanding the UnrollLoop into ReplaceLoopEnd... but now, ghc 6.6:

*Session> :t Proc $ mkLoop (recvLog >~> returnS ())
Proc $ mkLoop (recvLog >~> returnS ()) :: (ZeroOrMoreSteps (SessionSpec (Loop (SessionSpec s)))
                 (SessionSpec EndT),
 Show t,
 JustSendsRecvs (SessionSpec (Loop (SessionSpec s)))
                (SessionSpec (Loop (SessionSpec ol)))
                (SessionSpec (Loop (SessionSpec il))),
 JustSendsRecvs (SessionSpec (RecvT t (Loop (SessionSpec s))))
                (SessionSpec (Loop (SessionSpec ol)))
                (SessionSpec (SessT t (Loop (SessionSpec il)))),
 UnrollLoop (SessionSpec (Loop (SessionSpec il)))
            (SessionSpec (SessT t (Loop (SessionSpec il)))),
 UnrollLoop (SessionSpec (Loop (SessionSpec ol)))
            (SessionSpec (Loop (SessionSpec ol))),
 UnrollLoop (SessionSpec (Loop (SessionSpec s)))
            (SessionSpec (RecvT t (Loop (SessionSpec s))))) =>
Proc (SessionSpec (Loop (SessionSpec s)))
     (SessionSpec EndT)
     (Loop (SessionSpec ol))
     EndT
     (Loop (SessionSpec il))
     EndT

but ghc 20070514:

*Session> :t Proc $ mkLoop (recvLog >~> returnS ())
...hang...

Changed 8 years ago by matthew@…

No Mu, no recursive ADT but an infinite list.

comment:4 Changed 8 years ago by matthew@…

I've managed to halve the size of the source to 200 lines and still get the hang. SessionPruned.hs is as stripped down as I can (immediately) think of. I'll keep trying to get it smaller though.

So now in ghc 6.6 I have:

*Session> :t Proc $ mkLoop (returnS ())
blah blah - fine, no problem
*Session> :t let p1 = Proc $ mkLoop (returnS ()); p2 = Proc $ mkLoop (returnS ()) in p2
hung
*Session> :t let p1 = Proc $ mkLoop (returnS ()); p2 = Proc $ mkLoop (returnS ()) in p1
hung

In ghc 20070514 I have:

*Session> :t mkLoop (returnS ())
blah blah - fine, no problem
*Session> :t Proc $ mkLoop (returnS ())
hung

and the let versions hang in HEAD too. I do realise how crappy it is to post a bug report with a 200 line source, I'll try and prune it down further.

Changed 8 years ago by matthew@…

Starting to get it smaller...

comment:5 Changed 8 years ago by matthew@…

Actually, feel free to ignore this whole thing. I've finally realised that I wasn't using the recursive stuff at all so I hacked it out and replaced it with simple non-recursive stuff and the type checker's fine, even on ghc HEAD. So I guess it could well have been the inliner as you suggested Simon.

comment:6 Changed 8 years ago by simonpj

  • Resolution set to invalid
  • Status changed from new to closed

You are using -fallow-undecidable-instances, and that flag means that you are taking responsibility for making sure that type inference doesn't get into a loop. Maybe the flag should be -fif-type-inference-loops-its-my-fault.

Sure enough, it does. I traced it far enough to see that there was a cycle in which some improvement happens, and then some context reduction, and then more improvement. It's not impossible that there's a bug in GHC, but I didn't look further.

Admittedly, the manual does not specify just what your proof obligations are if you use -fallow-undecidable-instances. The best place to start is our paper Understanding functional dependencies using CHRs.

So I'm closing this one as 'invalid'.

Simon

Note: See TracTickets for help on using tickets.