Um tipo refinado estreita um tipo base com um predicado lógico. O compilador usa um solver SMT (Z3) para verificar que os valores satisfazem o predicado em tempo de compilação, capturando erros de fora-de-faixa antes de o programa rodar.

Sintaxe

type Positive = { x: i32 | x > 0 }
type Percentage = { p: f64 | p >= 0.0 && p <= 100.0 }
type NonEmpty<T> = { arr: [T] | len(arr) > 0 }

O predicado após o | deve ser uma expressão booleana pura sobre a variável vinculada e constantes. O compilador delega isso ao Z3 para verificação de satisfatibilidade.

Usando tipos refinados

fn safe_divide(a: f64, b: { b: f64 | b != 0.0 }) -> f64 {
    a / b
}

fn main() -> i32 with IO {
    let result = safe_divide(10.0, 3.0)   // OK: provado que 3.0 != 0.0
    println(result)

    // safe_divide(10.0, 0.0)  // erro de compilação: não é possível provar 0.0 != 0.0
}

Quando um literal é passado, o solver consegue verificar a restrição imediatamente. Quando uma variável é passada, o solver usa os refinamentos conhecidos da variável a partir do seu ponto de declaração.

Exemplo de dosagem

Tipos refinados são especialmente poderosos em domínios científicos onde restrições físicas importam:

type ValidDose = { dose: mg | dose > 0.0 && dose <= 2000.0 }

fn administer(patient_id: i64, dose: ValidDose) with IO {
    println("Administering dose")
}

fn main() -> i32 with IO {
    let dose: mg = 500.0
    administer(1, dose)     // OK: 500.0 dentro da faixa

    // let bad: mg = 5000.0
    // administer(1, bad)   // erro de compilação: 5000.0 > 2000.0
}

Interação com tipos epistêmicos

Predicados de refinamento se compõem com Knowledge<T>: um Knowledge<ValidDose> carrega tanto o envelope de incerteza quanto a restrição de refinamento. O compilador verifica os dois de forma independente — o refinamento vale sobre o valor nominal, e a propagação de confiança rastreia a incerteza de medição.

Onde a verificação de refinamentos vive

Verificação de tipos refinados: self-hosted/check/refinements.sio
Integração com SMT: compiler/src/smt/ (bindings do Z3, requer a feature flag smt)
O artefato nativo verificado (souc-linux-x86_64) tem o SMT desabilitado; a verificação de refinamentos fica disponível ao compilar com --features smt

Limitações atuais

A integração com o Z3 requer a feature flag smt em tempo de build.
Nem toda forma de predicado é suportada — o solver lida com comparações aritméticas, conectivos booleanos e restrições de comprimento de array. Chamadas de função personalizadas dentro de predicados ainda não são suportadas.
Um fallback de asserção em tempo de execução está disponível para predicados que não podem ser verificados estaticamente.

Tipos Refinados (Refinement Types)