If "near-linear" time was a bound it would be, but it's not. HM type inference is exptime-complete. Near-linear here is just "most programs people actually writ

If "near-linear" time was a bound it would be, but it's not. HM type inference is exptime-complete. Near-linear here is just "most programs people actually write type check in something close to linear time".