如何在子集类型见证子句中提供非空类型的任意参数值？

我想要定义一个参数化子集类型Bar<T(0)>，要求为其提供一个T类型的见证，基础代码如下：

datatype Foo<T> = Foo(x: T)
type Bar<T(0)> = x: Foo<T> | true witness ???

由于T是非空类型，我认为这个类型应该是可以定义的。

我尝试了几种写法，但都报错了：

• 第一种写法：

type Bar<T(0)> = x: Foo<T> | true witness Foo(*) // 错误提示：closeparen expected

• 第二种写法：

type Bar<T(0)> = x: Foo<T> | true witness Foo(var x: T := *; x) // 错误提示：invalid UnaryExpression

• 第三种写法：

type Bar<T(0)> = x: Foo<T> | true witness Foo(var x: T :| true; x) // 错误提示：to be compilable, the value of a let-such-that expression must be uniquely determined

我还尝试过用函数、函数方法或普通方法来解决这个问题，但都没成功。比如普通方法可以获取任意T类型值：

method Pick<T(0)>() returns (x: T)
{
}

但witness子句要求使用函数方法，ghost witness要求使用函数，在这些结构里尝试获取T类型值时，会出现和上面一样的错误。在方法或函数方法里调用Pick同样不可行。

我知道可以直接写witness *来解决，但这看起来更像是一个临时的权宜之计，而非合适的解决方案。我是否应该接受这种写法？

内容的提问来源于stack exchange，提问作者Tim Rakowski