Thanks @soronpo for trying my rough prototype and for sharing your examples. It really helps to have real-world use-cases to guide the discussion.
A general question: it looks to me that type parameters that could be instantiated to singleton types only and that could appear only once look similar in purpose to term-reference types (x.type) which do exactly that: give you a singleton type for a given parameter.
For example, positive could be defined as (currently buggy but will work after https://github.com/lampepfl/dotty/pull/15759 is merged):
type Positive2[T <: Int] = ITE[IsConst[T], T > 0, true] =:= true
def positive2(arg: Int)(using Positive2[arg.type]): Unit = assert(arg > 0)
id could also be typed as:
def id2(arg : Any): arg.type = arg
So how do term-references compare to @precise type parameters? In which situation are @precise type parameters needed and term-references can not be used?