Why? This was my also my understanding, you either have some inference (even if not everywhere), or absolutely none. What am I missing?
This Tweet is from a suspended account. Learn more
Conversation
This Tweet is from a suspended account. Learn more
I suspect you will allow some form of reconstruction of of types, but you'll choose not to call it inference.
4
8
It seems like people use the term 'synthesis' to describe this when talking about bidirectional type checking. It was confusing to me looking back at earlier work, because the term 'inference' was also used for this process, but the distinction seems to be useful!