@@ -660,9 +660,11 @@ impl<L: Locational> Unifier<'_, '_, '_, L> {
660660 self . sub_unify ( & l, sup) ?;
661661 Ok ( ( ) )
662662 }
663+ // OK: sub: (_: Nat), sup: 0
664+ // ERR: sub: (_: Nat), sup: "a"
663665 ( TyParam :: Erased ( t) , sup) => {
664666 let sup_t = self . ctx . get_tp_t ( sup) ?;
665- if self . ctx . subtype_of ( t, & sup_t) {
667+ if self . ctx . subtype_of ( t, & sup_t. derefine ( ) ) {
666668 Ok ( ( ) )
667669 } else {
668670 Err ( TyCheckErrors :: from ( TyCheckError :: subtyping_error (
@@ -1774,6 +1776,15 @@ impl<L: Locational> Unifier<'_, '_, '_, L> {
17741776 for ( sup_field, sup_ty) in self . ctx . fields ( supe) {
17751777 if let Some ( ( _, sub_ty) ) = sub_fields. get_key_value ( & sup_field) {
17761778 self . sub_unify ( sub_ty, & sup_ty) ?;
1779+ } else if let Some ( sub_ty) =
1780+ self . ctx . coerce ( sub. clone ( ) , & ( ) ) . ok ( ) . and_then ( |coerced| {
1781+ let sub_fields = self . ctx . fields ( & coerced) ;
1782+ let ( _, sub_ty) = sub_fields. get_key_value ( & sup_field) ?;
1783+ Some ( sub_ty. clone ( ) )
1784+ } )
1785+ {
1786+ sub. destructive_coerce ( ) ;
1787+ self . sub_unify ( & sub_ty, & sup_ty) ?;
17771788 } else {
17781789 return Err ( TyCheckErrors :: from ( TyCheckError :: no_attr_error (
17791790 self . ctx . cfg . input . clone ( ) ,
0 commit comments