[GHC] #14963: ghci -fdefer-type-errors can't run IO action from another module

[GHC]

#14963: ghci -fdefer-type-errors can't run IO action from another module
-------------------------------------+-------------------------------------
        Reporter:  elaforge          |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  high              |            Milestone:  8.4.2
       Component:  GHCi              |              Version:  8.4.1
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 It took me quite a while to find out what was going on here.

 I started with a file containing only
 {{{
 test :: IO Bool
 test = return True
 }}}
 Then load into GHCi, with `-fdefer-type-errors`
 {{{
 ghc --interactive -fdefer-type-errors Foo.hs
 }}}
 Now just evaluate `test`. Here's what I see from `-ddump-tc -ddump-ds`
 with a little extra debug tracing, when evaluating `test` at the GHCi
 prompt:
 {{{
 Typechecked expr do it_a1PP <- {>>=: GHC.Base.bindIO @ Bool
                                      @ [()]{let {EvBinds{[W] $dShow_a1Qg =
 GHC.Show.$fShowBool}} <>, <>}
                                            {<> |> <IO [()]>_R}
                                 fail: "noSyntaxExpr"{}{<>}} /\(@ a_a1Q5).
                                                             let
 {EvBinds{[W] $dGHCiSandboxIO_a1Q7
 = GHC.GHCi.$fGHCiSandboxIOIO}}
 GHC.GHCi.ghciStepIO @ IO
 $dGHCiSandboxIO_a1Q7
                                                             @ a_a1Q5 ::

   ic_tythings:
   ic_insts:
   ic_rn_gbl_env (LocalDef) [Foo.test defined at Foo.hs:11:1]
 newTcEvBinds unique = a1Ql
 checkSatisfiability { {}
 checkSatisfiability } {}
 unflattenGivens []
 ds BindStmt
     /\(@ a_a1Q5).
     let {EvBinds{[W] $dGHCiSandboxIO_a1Q7 = $fGHCiSandboxIOIO}}
     ghciStepIO @ IO $dGHCiSandboxIO_a1Q7 @ a_a1Q5 ::
       forall a_a1PO. IO a_a1PO -> IO a_a1PO
   @ Bool
     test
     |> <IO Bool>_R
   ---
   (\ (@ a_a1Q5) ->
      let {
        $dGHCiSandboxIO_a1Q7 :: GHCiSandboxIO IO
        [LclId]
        $dGHCiSandboxIO_a1Q7 = $fGHCiSandboxIOIO } in
      ghciStepIO @ IO $dGHCiSandboxIO_a1Q7 @ a_a1Q5)
     @ Bool test
 *** Core Lint errors : in result of desugar expression ***
 <no location info>: warning:
     In the expression: print @ Bool $dShow_a1Qg it_a1PP
     $dShow_a1Qg :: Show Bool
     [LclId] is out of scope
 *** Offending Program ***
 bindIO
   @ Bool
   @ [()]
   (let {
      $dShow_a1Qg :: Show Bool      <----- Right binding, wrongly scoped!
      [LclId]
      $dShow_a1Qg = $fShowBool } in
    (\ (@ a_a1Q5) ->
       let {
         $dGHCiSandboxIO_a1Q7 :: GHCiSandboxIO IO
         [LclId]
         $dGHCiSandboxIO_a1Q7 = $fGHCiSandboxIOIO } in
       ghciStepIO @ IO $dGHCiSandboxIO_a1Q7 @ a_a1Q5)
      @ Bool test)
   (\ (it_a1PP :: Bool) ->
      thenIO
        @ ()
        @ [()]
        (print @ Bool $dShow_a1Qg it_a1PP)
        (returnIO
           @ [()]
           (: @ ()
              (unsafeCoerce# @ 'LiftedRep @ 'LiftedRep @ Bool @ () it_a1PP)
              ([] @ ()))))
 *** End of Offense ***
 }}}

 Here's the deal.

 * When you type `ghci> test` to the GHCi prompt, GHC typechecks (roughly)
 {{{
 do { it <- sandbox test
    ; print it
    ; return () }
 }}}
   This is Plan A in TcRnDriver.tcUserStmt.

 * When typechecking the initial `BindStmt` of the `do` block, we end up
 invoking `tcSyntaxOp` in `TcMatches.TcDoStmt`

 * Bizarrely, we then typecheck the rest of the `do` block inside the
 `thing_inside` argument to `tcSyntaxOp`.

 * `TcExpr.tcSyntaxOp` ends up calling `tcSyntaxArgE`, which calls
 `tcSkolemize`, which builds an implication constraint.

 * This implication constraint gets wrapped around the first argument of
 the bind, namely `sandbox test`.  But since the `thing_inside` includes
 the `Show` constraint arising from `print it`, the `Show` dictionary lands
 up in the evidence bindings for the implication, and hence gets wrapped
 around the `sandbox test` RHS only. Utterly bogus.

 * All this happens always, I think.  Usually `TcUnify.implicationNeeded`
 ends up being false, so we don't actually create an implication, and so
 the evidence bindings don't end up in the wrong place.  But in the special
 case of GHCi with `-fdefer-type-errors` we (unusually) you'll see that
 `implicationNeeded` returns True.  And that's why the bug manifest only in
 GHCi, and even then only with `-fdefer-type-errors`.

 Blimey.

 --------------------------------
 All of this is a result of the impenetrable code in `tcSyntaxOp`, which
 Richard introduced in
 {{{
 commit 00cbbab3362578df44851442408a8b91a2a769fa
 Author: Richard Eisenberg <eir at cis.upenn.edu>
 Date:   Wed Jan 13 23:29:17 2016 -0500

 ...

     In addition, this patch does a significant reworking of
     RebindableSyntax, allowing much more freedom in the types
     of the rebindable operators. For example, we can now have
     `negate :: Int -> Bool` and
     `(>>=) :: m a -> (forall x. a x -> m b) -> m b`. The magic
     is in tcSyntaxOp.
 }}}
 To me it seems Utterly And Completely Wrong for `tcSyntaxOp` to take the
 continuation as a `thing_inside` argument. Not only is it extremely
 complicated, but it's also plain wrong.

 Why can't it just decompose the function type to produce a bunch of types
 to use as the expected types for the aguments?  No Notes explain.  The
 code makes my head spin.

 Richard, can't this all be radically simplified?

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14963#comment:8>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler