justified-type-inference An implementation of Compositional type inference in Idris with a complete proof I am now working on a Coq version of this because of a code generation bug in Idris and because typechecking was so slow.