Typechecking without Minimum Types: Finite Bases and Backward Checking for $F_{<:}^{\top }$

Mingkun Xiao, Yixuan Sun

System $F_{<:}^{\top }$ has decidable subtyping but lacks minimum types. We prove that typechecking is decidable for arbitrary explicitly annotated terms with unrestricted subsumpti…