#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