Implement proper bidirectional type inference

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

Trac metadata

Trac field	Value
Version	7.10.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture