[klibertp]

My understanding is that you get a type error when the type checker cannot prove the result of an operation conforms to a refined type. For constants, it's easy: `(Nat 5) - (Nat 3)` is Nat while `(Nat 5) - (Nat 6)` is a type error. For values coming from elsewhere, you need to give the type-checker some guarantee yourself:

    let x = Nat 5;
    let y = read_nat();
    assert y < x;  // without this, the following would fail to type check
    x - y

(you need occurrence typing, too, in this example)

In terms of numbers, what you can expect from refinement types is similar to what you get with CLP(FD) in Prolog.

[tubthumper8]

Right, but what happens if the Assert isn't true? Does the program crash/abort? If so, is there a stack trace or how do you troubleshoot it?

[dietr1ch]

I guess the only natural way would be to have operations send you back to the Base type, and then have a `TryInto(v: Base) -> Result<Refined>` function that would verify the predicate and allow you getting back into the refined type.

Maybe some operations can be proved to stay within the refined type, like adding natural numbers, but that's something that the used would need to provide as a function allowing that under assertions or some proof that the compiler can verify and trust.

[klibertp]

It's a standard assert, so whatever happens on assertion failure normally happens here, too. This is orthogonal to refinement types - they are concerned with whether the check is made or not (ie. with them you cannot accidentally forget to write that assert). The check failing is a runtime concern (similar to dynamic cast failure), the type system has nothing to do with that.