Move exhaustiveness checking to type solving phase with solve tests

This commit is contained in:
Ayaz Hafiz 2022-04-22 10:22:49 -04:00
parent 9602b3634c
commit 356616d834
No known key found for this signature in database
GPG key ID: 0E2A37416A25EF58
13 changed files with 678 additions and 42 deletions

View file

@ -5,6 +5,7 @@ use crate::pattern::{constrain_pattern, PatternState};
use roc_can::annotation::IntroducedVariables;
use roc_can::constraint::{Constraint, Constraints};
use roc_can::def::{Declaration, Def};
use roc_can::exhaustive::{sketch_rows, ExhaustiveContext};
use roc_can::expected::Expected::{self, *};
use roc_can::expected::PExpected;
use roc_can::expr::Expr::{self, *};
@ -718,6 +719,11 @@ pub fn constrain_expr(
// total_cons.push(expr_con);
pattern_cons.push(expr_con);
let sketched_rows = sketch_rows(cond_var, branches_region, &branches);
let exhaustiveness_constraint =
constraints.exhaustive(sketched_rows, ExhaustiveContext::BadCase);
pattern_cons.push(exhaustiveness_constraint);
// Solve all the pattern constraints together, introducing variables in the pattern as
// need be before solving the bodies.
let pattern_constraints = constraints.and_constraint(pattern_cons);