#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/Impredicativ... 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