The Calculated Typer

Very good question! Funnily enough, it was indeed a conscious decision to avoid mentioning "inference", because then people might expect that we're doing polymorphism with type variables/or maybe that we're deriving a Hindley-Milner inference system.

We're not doing these things, so we figured it would be safer this way, but absolutely you could call what we're doing "type inference".

That being said, we've got some ideas for a follow-up paper to revisit this and derive something more worthy of being called "inference".

The more complicated a type system is, the harder it is to make inference work.

Global type inference typically works well in Haskell without any hand-holding, but when you pack more features into the type system (e.g. in Idris), the programmer needs to explicitly write out more type signatures.

This type system looks "next-level complicated", so inference is probably way out of the question, e.g. if you saw the expression 2 + 3, maybe the types are:

  2 :: Head<Filter<IsPositive,[-1,-3,2,4]>>
  3 :: Head<Drop<4,Fibonnaci>>

If you were type-checking, you could start on the RHS, end up with the LHS, and then confirm that these two sub-expressions can be added. But with inference you're trying to figure out the most appropriate RHS from the LHS.