Keyed filters: substitute into filter predicate

[amosr]

When we insert keys, we change the type of all the stream folds from x : a to x : (Option Key, a). Everywhere that mentions the keys needs to be substituted x => snd x. But we weren't performing this substitution in the filter predicates, just the stream parts: so filter x never became filter (snd x).

This looks like a reasonable fix and I'm fairly confident that it's correct, but I'm not sure why or how it worked before. I don't remember changing the key parts recently. The only part of translation I changed were groups, distincts, and double primitives. None of those should affect this test case. I'll look through to see what changed.

I also modified the Core typechecking errors to include the let-binding name when it's inside a definition, and for application errors print the expected vs actual type rather than the whole function type:

        In let-binding simp-8
        Application type mismatch:
          Fun: fst#
          Arg: conv-4
          Expected: (Int, (Sum Error { dollarydoos : Int, transaction_id : Int }, Time))
          Actual:   (Option (Sum Error Int), (Int, (Sum Error { dollarydoos : Int, transaction_id : Int }, Time)))

! @jystic @tranma /jury approved @jystic

[amosr]

Actually: I remember adding the Core typechecking to Source fairly recently. Before that, ill-typed Core programs were being simplified away by accident. So is it possible that the payload version is silently dropping these features?

[jacobstanley]

👍 cool, makes sense

[jacobstanley]

I'm going to merge this so I can try it

[tranma]

Ok, I don't think anything was using keys before, that's why. Definitely my fault when writing this, I thought the tests did generate random expressions to be used as keys though.

[tranma]

Perhaps that was the problem. They were too random?