The current subtyping rules that Agda uses are for sized types (when `--sized-types` is enabled) and cumulativity (when `--cumulativity` is enabled). Currently neither of these options are allowed under the `--safe` flag, so with `--safe` there is no subtyping in Agda.

There used to be subtyping rules for irrelevant and erased function types as well, but these were removed recently (see [This successful Pull Request which was merged into Master on GitHub](https://github.com/agda/agda/pull/5608)) because they were causing performance problems and anyway only save the user a simple eta-expansion.