pub fn check_subtype(level: VarLevel, ty1: &RcType, ty2: &RcType) -> Result<bool, NbeError> {
    match (&ty1.as_ref(), &ty2.as_ref()) {
        (&Value::Neutral(head1, spine1), &Value::Neutral(head2, spine2)) => {
            let term1 = read_back_neutral(level, *head1, spine1)?;
            let term2 = read_back_neutral(level, *head2, spine2)?;

            Ok(Term::alpha_eq(&term1, &term2))
        },
        (&Value::LiteralType(literal_ty1), &Value::LiteralType(literal_ty2)) => {
            Ok(literal_ty1 == literal_ty2)
        },
        (
            &Value::FunType(app_mode1, param_ty1, body_ty1),
            &Value::FunType(app_mode2, param_ty2, body_ty2),
        ) if app_mode1 == app_mode2 => {
            let param = RcValue::var(level);

            Ok(check_subtype(level, param_ty2, param_ty1)? && {
                let body_ty1 = do_closure_app(body_ty1, param.clone())?;
                let body_ty2 = do_closure_app(body_ty2, param)?;
                check_subtype(level + 1, &body_ty1, &body_ty2)?
            })
        },
        (
            &Value::RecordTypeExtend(_, label1, term_ty1, rest_ty1),
            &Value::RecordTypeExtend(_, label2, term_ty2, rest_ty2),
        ) => {
            let term = RcValue::var(level);

            Ok(
                // FIXME: Could stack overflow here?
                label1 == label2 && check_subtype(level, term_ty1, term_ty2)? && {
                    let rest_ty1 = do_closure_app(rest_ty1, term.clone())?;
                    let rest_ty2 = do_closure_app(rest_ty2, term)?;
                    check_subtype(level + 1, &rest_ty1, &rest_ty2)?
                },
            )
        },
        (&Value::RecordTypeEmpty, &Value::RecordTypeEmpty) => Ok(true),
        (&Value::Universe(level1), &Value::Universe(level2)) => Ok(level1 <= level2),
        _ => Ok(false),
    }
}
/// Check whether a semantic type is a subtype of another
Check whether a semantic type is a subtype of another
Check whether a semantic type is a subtype of another
pub fn check_subtype(level: VarLevel, ty1: &RcType, ty2: &RcType) -> Result<bool, NbeError> {
    match (&ty1.as_ref(), &ty2.as_ref()) {
        (&Value::Neutral(head1, spine1), &Value::Neutral(head2, spine2)) => {
            let term1 = read_back_neutral(level, *head1, spine1)?;
            let term2 = read_back_neutral(level, *head2, spine2)?;
            Ok(Term::alpha_eq(&term1, &term2))
        },
        (&Value::LiteralType(literal_ty1), &Value::LiteralType(literal_ty2)) => {
            Ok(literal_ty1 == literal_ty2)
        },
        (
            &Value::FunType(app_mode1, param_ty1, body_ty1),
            &Value::FunType(app_mode2, param_ty2, body_ty2),
        ) if app_mode1 == app_mode2 => {
            let param = RcValue::var(level);
            Ok(check_subtype(level, param_ty2, param_ty1)? && {
                let body_ty1 = do_closure_app(body_ty1, param.clone())?;
                let body_ty2 = do_closure_app(body_ty2, param)?;
                check_subtype(level + 1, &body_ty1, &body_ty2)?
            })
        },
        (
            &Value::RecordTypeExtend(_, label1, term_ty1, rest_ty1),
            &Value::RecordTypeExtend(_, label2, term_ty2, rest_ty2),
        ) => {
            let term = RcValue::var(level);
            Ok(
                // FIXME: Could stack overflow here?
                label1 == label2 && check_subtype(level, term_ty1, term_ty2)? && {
                    let rest_ty1 = do_closure_app(rest_ty1, term.clone())?;
                    let rest_ty2 = do_closure_app(rest_ty2, term)?;
                    check_subtype(level + 1, &rest_ty1, &rest_ty2)?
                },
            )
        },
        (&Value::RecordTypeEmpty, &Value::RecordTypeEmpty) => Ok(true),
        (&Value::Universe(level1), &Value::Universe(level2)) => Ok(level1 <= level2),
        _ => Ok(false),
    }
}
pub fn check_subtype ( level : VarLevel , ty1 : & RcType , ty2 : & RcType ) -> Result < bool , NbeError > { match ( & ty1 . as_ref ( ) , & ty2 . as_ref ( ) ) { ( & Value :: Neutral ( head1 , spine1 ) , & Value :: Neutral ( head2 , spine2 ) ) => { let term1 = read_back_neutral ( level , * head1 , spine1 ) ? ; let term2 = read_back_neutral ( level , * head2 , spine2 ) ? ; Ok ( Term :: alpha_eq ( & term1 , & term2 ) ) } , ( & Value :: LiteralType ( literal_ty1 ) , & Value :: LiteralType ( literal_ty2 ) ) => { Ok ( literal_ty1 == literal_ty2 ) } , ( & Value :: FunType ( app_mode1 , param_ty1 , body_ty1 ) , & Value :: FunType ( app_mode2 , param_ty2 , body_ty2 ) , ) if app_mode1 == app_mode2 => { let param = RcValue :: var ( level ) ; Ok ( check_subtype ( level , param_ty2 , param_ty1 ) ? && { let body_ty1 = do_closure_app ( body_ty1 , param . clone ( ) ) ? ; let body_ty2 = do_closure_app ( body_ty2 , param ) ? ; check_subtype ( level + 1 , & body_ty1 , & body_ty2 ) ? } ) } , ( & Value :: RecordTypeExtend ( _ , label1 , term_ty1 , rest_ty1 ) , & Value :: RecordTypeExtend ( _ , label2 , term_ty2 , rest_ty2 ) , ) => { let term = RcValue :: var ( level ) ; Ok ( // FIXME: Could stack overflow here? label1 == label2 && check_subtype ( level , term_ty1 , term_ty2 ) ? && { let rest_ty1 = do_closure_app ( rest_ty1 , term . clone ( ) ) ? ; let rest_ty2 = do_closure_app ( rest_ty2 , term ) ? ; check_subtype ( level + 1 , & rest_ty1 , & rest_ty2 ) ? } , ) } , ( & Value :: RecordTypeEmpty , & Value :: RecordTypeEmpty ) => Ok ( true ) , ( & Value :: Universe ( level1 ) , & Value :: Universe ( level2 ) ) => Ok ( level1 <= level2 ) , _ => Ok ( false ) , } }
Check whether a semantic type is a subtype of another
Check whether a semantic type is a subtype of another
level
VarLevel
ty1
&RcType
ty2
&RcType