[GHC] #10585: Implement proper bidirectional type inference

[GHC]

#10585: Implement proper bidirectional type inference
-------------------------------------+-------------------------------------
              Reporter:  goldfire    |             Owner:
                  Type:  bug         |            Status:  new
              Priority:  normal      |         Milestone:
             Component:  Compiler    |           Version:  7.10.1
  (Type checker)                     |  Operating System:  Unknown/Multiple
              Keywords:              |   Type of failure:  None/Unknown
          Architecture:              |        Blocked By:
  Unknown/Multiple                   |   Related Tickets:
             Test Case:              |
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------
 The [http://research.microsoft.com/en-us/um/people/simonpj/papers/higher-
 rank/putting.pdf Practical Type Inference paper] (JFP '07) lays out a
 nice, relatively straightforward bidirectional type inference algorithm
 for GHC.

 The problem is that there is not great hygiene practiced around
 transitions between "down" checking and "up" checking, neither in the
 paper nor in the implementation. Examine Figure 8 of the paper, which
 presents the bidirectional typing rules. There are several syntactic forms
 which are fundamentally "up" forms -- forms that cannot gain any benefit
 from any type information being propagated downwards. Examples include
 App, Var, and Annot. Other forms propagate the very direction they are
 operated in, such as Let. And then some forms depend somewhat delicately
 on direction, such as the Abs rules.

 I propose changing these rules to be more in the style of Figure 4 from
 Dunfield & Krishnaswami's ICFP'13 paper [http://arxiv.org/pdf/1306.6032v1
 here]. The particular rule I'm interested in is DeclSub, paraphrased here:

 {{{
 G |-up e : s1
 s1 <= s2
 ---------------
 G |-down e : s2
 }}}

 (I'm not advocating other aspects of their approach, just the general idea
 around this rule being the only transition between down and up.)

 In GHC, mediating between "down" checking and "up" checking is done in an
 ad-hoc manner, made even more difficult by the fact that it takes two
 separate steps to pull off properly: we must first `deeplyInstantiate` the
 "up" type that we get and then call `tcSubType` (or one of its variants).
 And, because this has to be done for each "up" expression form (forms that
 cannot use down-propagated type information), it's easy to miss a case. As
 a case in point, consider the following code:

 {{{
 foo :: forall b. b -> (Int -> Int) -> b
 foo = undefined

 bar :: ((forall a. a -> a) -> Int) -> Int
 bar = undefined

 baz = bar (foo 3)
 bum = bar (3 `foo`)
 }}}

 In 7.10.1, `baz` is accepted, while `bum` is not. This is because the code
 for left-sections doesn't ever call `tcSubType` -- it uses `unifyType`.

 While that one case is easy enough to fix, I advocate a redesign of
 `tcExpr` to break it into two functions: one for "down" forms and one for
 "up" forms. These would, of course, be mutually recursive in order so that
 both can handle all expression forms. But these transitions could then be
 policed more easily.

 I don't actually think this would entail all that much work, and it would
 structurally remove the possibility of bugs such as the one above.

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