[PhilipRoman]

The "value" in this case is symbolic, sort of like defining an array with variable length arr[x] and having the compiler verify that arr[x+5] is always out of bounds before knowing the actual value of x. If the type system is not powerful to prove correctness of some expression, you will need to insert a runtime check that lets the compiler to trust the value at compile time.

[reuben364]

You still need a way of normalizing expressions that is consistent with your runtime. To say that types ((x: bool) => F<true && x>) and ((x: bool) => F<false || x>) are the same, wrt judgemental equality, requires normalizing both to ((x: bool) => F<x>).