fn check_clause_body(
    context: &Context,
    clause: &Clause<'_>,
    expected_body_ty: &domain::RcType,
) -> Result<core::RcTerm, Diagnostic<FileSpan>> {
    match clause.concrete_body_ty {
        None => check_term(&context, clause.concrete_body, &expected_body_ty),
        Some(concrete_body_ty) => {
            let (body_ty, _) = synth_universe(&context, concrete_body_ty)?;
            let body_ty = context.eval(concrete_body_ty.span(), &body_ty)?;
            let body = check_term(&context, clause.concrete_body, &body_ty)?;
            // TODO: Ensure that this is respecting variance correctly!
            context.expect_subtype(clause.concrete_body.span(), &body_ty, &expected_body_ty)?;
            Ok(body)
        },
    }
}
/// Check that the body of the given clause conforms to they expected type, and
/// elaborate it.
Check that the body of the given clause conforms to they expected type, and
elaborate it.
Check that the body of the given clause conforms to they expected type and elaborate it .
fn check_clause_body(
    context: &Context,
    clause: &Clause<'_>,
    expected_body_ty: &domain::RcType,
) -> Result<core::RcTerm, Diagnostic<FileSpan>> {
    match clause.concrete_body_ty {
        None => check_term(&context, clause.concrete_body, &expected_body_ty),
        Some(concrete_body_ty) => {
            let (body_ty, _) = synth_universe(&context, concrete_body_ty)?;
            let body_ty = context.eval(concrete_body_ty.span(), &body_ty)?;
            let body = check_term(&context, clause.concrete_body, &body_ty)?;
            // TODO: Ensure that this is respecting variance correctly!
            context.expect_subtype(clause.concrete_body.span(), &body_ty, &expected_body_ty)?;
            Ok(body)
        },
    }
}
fn check_clause_body ( context : & Context , clause : & Clause < ' _ > , expected_body_ty : & domain :: RcType , ) -> Result < core :: RcTerm , Diagnostic < FileSpan > > { match clause . concrete_body_ty { None => check_term ( & context , clause . concrete_body , & expected_body_ty ) , Some ( concrete_body_ty ) => { let ( body_ty , _ ) = synth_universe ( & context , concrete_body_ty ) ? ; let body_ty = context . eval ( concrete_body_ty . span ( ) , & body_ty ) ? ; let body = check_term ( & context , clause . concrete_body , & body_ty ) ? ; // TODO: Ensure that this is respecting variance correctly! context . expect_subtype ( clause . concrete_body . span ( ) , & body_ty , & expected_body_ty ) ? ; Ok ( body ) } , } }
Check that the body of the given clause conforms to they expected type, and
elaborate it.
Check that the body of the given clause conforms to they expected type and elaborate it .
context
&Context
clause
&Clause<'_>
expected_body_ty
&domain::RcType