#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/Impredicativ... impredicativity]. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10585#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler