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 |