Inlined constrained type using control flow analysis

Some recent features like "String Literals" or "strict null check" in Typescript can be used to shift responsibility of checking the validity of a parameter from function/API developer's side to caller's side. And with control flow analysis, one can start with an discriminated union type and based on the flow of the code, compiler will determine or exclude some specific types. So, code like this-

    function checkResponse(response: String): boolean {
        if (response === null)
            throw new Error("Response cannot be null")

        if (response === "YES")
            return true
        if (response === "NO")
            return false

        throw new Error("Not valid response")
    }

can be converted to-

    function checkResponse(response: "YES"|"NO"): boolean {
        return (response === "YES")
    }

And compiler will ensure the caller will only be able to call the function with appropriate values. This increases integrity of code. (Although, caller should also be using Typescript in these cases, as the checking does not exist in compiler generated javascript code.)

Now, I am proposing a Typescript feature with similar intention/result- shifting the responsibility of validation to upper(caller/consumer) side. What I am trying to propose is best described by an example. Using this feature code like this-

    function squareRoot(num: number): number {
        if (num < 0)
            throw new RangeError("Not valid number")
        var root: number
        // do the calculation
        return root
    }

will become something like-

    function squareRoot(num: number:[_ >= 0]): number {
        var root: number
        // do the calculation
        return root
    }

Here, a constraint is being attached :[_ >= 0] (syntax can be anything else, more fitting with Typescript) with it's parameter, and the range checking is omitted. Now, according the new feature, the compiler will show an error, if during this function call, it cannot be sure whether the parameter value satisfies the constraint or not using control flow analysis. So-

    squareRoot(0) //Ok. For constants, compiler can check validity by itself
    squareRoot(-1) //Error

    var userInput = Number(prompt())
    squareRoot(userInput) //Error, compiler not sure

    if(userInput >= 0 )
        squareRoot(userInput) //Ok

    if(userInput > 1000)
        squareRoot(userInput) //Ok

    if(userInput > -1 )
        squareRoot(userInput) //Error, compiler not sure

    if(userInput < 0)
        return
    squareRoot(userInput) //Ok

And this is not only for range checking numbers. But any (pure- without side effect) function taking an object of type T and returning boolean can be attached to type T. So, checking if some string is a valid email or satisfies a regex pattern, or whether a file is writable or more complex check for a complex type, all are possible within the scope of this proposal.

I am calling this idea Constrained Type- a type with an attached constraint. Most of goals of this proposal can be achieved now in current language, using newly derived types/inheritance. But someone has to derive a child type for each of the constraints they want to check. The constructor in the derived type can then check and prevent invalid objects being created. But it seems doing too much for too little. It is cumbersome for both API developers and callers. And doing this by inheritance hides the base or actual type of the data to the API consumer. That's why we see very few of them. This proposal will make both the base type and the constraint easily visible to the consumer, as the constraint is inlined with the base type. It does not clog the base type, as it is not a part of it. And consumer/caller can then just declare a variable of base type and check to reach constraint satisfaction- a workflow very similar to what is currently practiced.

There are some previous proposals like this- "Tag types" #4895 and "Refinement Types" #7599 (both by @aleksey-bykov). But what I understood from reading them (and I may be wrong), they are trying to track changes of some object to determine whether some condition holds at some point of code. This proposal has nothing to do with tracking states. It just proposes to describe attributes of data with more ease and increase integrity using compiler's ability to analyse control flows.

The issue contains no implementation files, tests, or entry points. Start by reviewing the constrained-type proposal and the related Tag types (#4895) and Refinement Types (#7599) proposals, then define the syntax, control-flow rules, and diagnostics needed for the examples to work.