[GHC] #10585: Implement proper bidirectional type inference

[GHC]

#10585: Implement proper bidirectional type inference
-------------------------------------+-------------------------------------
        Reporter:  goldfire          |                   Owner:  goldfire
            Type:  bug               |                  Status:  new
        Priority:  normal            |               Milestone:
       Component:  Compiler (Type    |                 Version:  7.10.1
  checker)                           |                Keywords:
      Resolution:                    |            Architecture:
Operating System:  Unknown/Multiple  |  Unknown/Multiple
 Type of failure:  None/Unknown      |               Test Case:
      Blocked By:                    |                Blocking:
 Related Tickets:                    |  Differential Revisions:
-------------------------------------+-------------------------------------

Comment (by goldfire):

 Replying to [comment:2 simonpj]:
 > 1.  Even if we had two `tcExpr` functions (one for "up" and one for
 "down") why would that structurally remove the possibility of bugs?
 Presumably each expression form occurs in one but not the other, and you
 could get that wrong, just as now.  In the current code, that's like
 missing out a subsumption check, which is a bug to be sure.

 Good point. Right now, the "up" rules should end in a `tcWrapResult`, and
 contain a `deeplyInstantiate` if there's a possibility the inference will
 yield a polytype. My proposed refactoring would mean these checks would
 happen in one place, instead of scattered throughout the rules. But it
 would still be very easy for a syntactic form to be mentioned in the wrong
 `tcExpr`, or perhaps in both. So my claim to eliminating problems
 structurally is overstated.

 >
 > 2.  I think that GHC does a mixture of up and down in one blow. Consider
 > {{{
 >         tcExpr ((\y x. (x True, x 'x')) 3)
 >                (forall a. a->a) -> (Bool, Char))
 > }}}
 >   This is an APP; so we must infer the argument type of the function;
 but know the result type of the function, and THAT can be useful, as here.
 So recursively calling
 > {{{
 >         tcExpr (\y x. (x True, x 'x'))
 >                (alpha -> (forall a. a->a) -> (Bool, Char)))
 > }}}
 >   is good. Here `alpha` is the `ReturnTv` that is filled in by
 inference.
 >
 >   Admittedly none of this is described in the paper!

 Great example! Except that GHC doesn't do what you want: this fails in
 7.10.1, and this is no surprise, looking at the code. `tcApp` calls
 `tcInferFun`, which doesn't propagate any "down" type information. It
 looks like you can profitably propagate information in your example, but I
 think writing inference rules for this propagation would require including
 unification variables in the rules. This would mean that the
 implementation would diverge even more from any specification you could
 write.

 >
 > 3. Lastly we need to revisit all this when we talk about
 [https://ghc.haskell.org/trac/ghc/wiki/ImpredicativePolymorphism/Impredicative-2015
 impredicativity].

 Indeed.

 I'm still in favor of this refactoring (though I don't have any
 understanding of how issue (3) affects us, and so could change my mind
 with more information there). If we decide to accommodate (2), we could
 easily do so by having the "App" rule in both `tcExpr`s. If we do this, we
 should make sure that sections are treated like applications.

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