What's the goal of the new work-in-progress typechecker in comparison to the current one?

[karl-police]

I am concerned about some things about the new WIP typechecker. But since it's still WIP, it doesn't mean that it's final.
But I also don't know what the aim of the final version, is supposed to be.

So here's a summary of the things that I am wondering about.

Will the new typechecker...

• still support the same things the old typechecker did, in terms of auto suggestion/completion and --! modes?
• support free generic types's old features
  • e.g. default a, b, c
  • things assigned through <> without it being assigned to a function argument, (free generic type)
• support the same return types?
  • e.g. typeof(table.clone()) returns {- -} in old, and {+ +} in new. But {+ +} has no auto suggestion.
• support a lot of nested unification and with typeof()?

[aatxe]

The goals of the new type system are, in no particular order,

• to improve the accuracy of inferred types
• to improve the expressiveness of the type system (to support e.g. typing for operator overloading)
• to eliminate a significant class of type inference bugs caused by the old architecture (which was intrinsically greedy, causing lots of spurious type errors)
• to separate, architecturally, the task of type inference from the task of type checking (which allows us to reduce the amount of work needed to power both error reporting and autocomplete simultaneously, especially for users of non-strict mode)
• to clarify and ultimately simplify the behavior of non-strict mode in particular (rather than just inferring any most of the time, it uses the same inference result, but a new strategy for type checking to only report errors for code that we can prove will always blow up at runtime)
• to pay down a lot of existing technical debt with the old solver, and build up a lot of technical credit by making architectural changes that enable us to ship new type system features more easily going forward

This is not necessarily a comprehensive list, and there may be other goals that we're targeting that I have not enumerated here, but hopefully this helps with understanding what we're trying to accomplish better.

To try to directly answer you questions,

• We experientially want autocomplete to be no worse, and ideally better, than what you get from the old solver, and that's a core design goal.
• We will continue to support both a strict mode and a non-strict mode typechecker, with a single consistent type inference pass for both of them.
• Free types are not generic types, and I am confused as to what you're asking about because of the conflation of the two. However, free types were not ever intended to be a user-visible thing in inference results. They're a mechanical detail of how a type inference system works, and any instance where they were arising as a user-visible thing was a bug in the old solver, some of which would've been very difficult to fix, and any instance in which they arise as a user-visible thing in the new solver will also be treated as a bug.
• For generic types, we do not expect a major change in their behavior right now, but one of the new features that the new solver's technical credit will be used for is expanding the expressivity of generics by adding support for bounds on generic types.
• Built-in APIs may have changes to their type signatures if we feel that changes we've made to the type system can allow us to express a more accurate type for those built-in APIs.
• You should reasonably expect changes around the various table states, but I can't promise exactly what they will be. One thing we changed is, notationally, sealed tables are now written { x: number, y: number } and unsealed tables are {| x:number, y: number |} since, like free types, unsealed types are an implementation detail that we don't expect to surface to users in inference results. Further, generic tables, written {+ +}, are deprecated and will go away entirely. I'm unsure of where free tables (written {- -}) will land, but if they do continue to exist, they should also be an implementation detail and not something surfaced to users as part of any type signature. In general, a lot of this was less-than-ideal solutions to the limitations of the old architecture, and now that we're solving that, we can clean up the complexity a lot.
• Regrettably, typeof in type positions is here to stay, and the only real change there is that it will be more explicit about providing the type of the given expression at that point in the program. This is because the new solver supports a feature called typestate that allows the type of a binding to change in response to assignments from the user (which addresses a common user complaint about code like arg = arg or "some default value" at the top of their function bodies not working unless you make a new binding).
• I am not sure what you're asking about with "support a lot of nested unification" but the new type inference system is more general than the old one and capable of inferring unified common types (like unions) that might've otherwise (without annotation) led to type errors in the old solver.

[karl-police]

with nested unification I mean generic types mixed with & Generic_Type_1 & typeof(something) etc. moving on further, to combine Base Class with a Class for instance, and give it autocompletion, but also that what was combined, combined with even more, and etc.

typestate sounds interesting, not sure if that means that if I do

local test = {}
local a: typeof(test)

test.a = "something"

that the type at that time will only be an empty table?