From the abstract it sounds a bit like <a href="https://brianmckenna.org/blog/type_annotation_cofree" rel="nofollow">https://brianmckenna.org/blog/type_annotation_cofree</a>, which is a great read.
Q: There is not a single occurrence of the word "infer" (and related terms such as "inference") in the whole paper. Did you carefully try to avoid it or did this happen accidentally? Or is it the point of your paper?<p>(I encounter Type Checking only in my IDE when red squiggly lines appear under syntax errors etc. So consider this a layman Q)