[mrkeen]

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.