[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 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.

 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!

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

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