Skip to content

GHCi hangs when type checking

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.

Trac metadata
Trac field Value
Version 6.6
Type Bug
TypeOfFailure OtherFailure
Priority normal
Resolution Unresolved
Component GHCi
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information