Skip to main content
Proof Assistants Beta

Return to Answer

Added hyperlinks.
Source Link
edit approved Mar 28, 2022 at 22:49
Nike Dattani
edit approved Mar 28, 2022 at 22:49
Nike Dattani
  • 1.2k
  • 13
  • 30

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 https://github.com/agda/agda/pull/5608This successful Pull Request which was merged into Master on GitHub) because they were causing performance problems and anyway only save the user a simple eta-expansion.

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 (https://github.com/agda/agda/pull/5608) because they were causing performance problems and anyway only save the user a simple eta-expansion.

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) because they were causing performance problems and anyway only save the user a simple eta-expansion.

Source Link
Jesper
Jesper
  • 506
  • 5
  • 8

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 (https://github.com/agda/agda/pull/5608) because they were causing performance problems and anyway only save the user a simple eta-expansion.