Options #

Configurable options for the typeclass generalization linter.

inductive GeneralizationLinter.SplitPolicy :

Controls whether typeclass weakenings that would involve splitting a single hypothesis into two weaker ones should be suggested. Suggested weakenings that split typeclass hypotheses can violate diamond coherence. Measures are in place to significantly reduce the frequency of such false positives, but they do not eliminate them, which is why this option is set to .forbid by default.

forbid : SplitPolicy
Forbid weakenings that would split a typeclass hypothesis up.
allow : SplitPolicy
Allow weakenings that would split a typeclass hypothesis up. However, if a different weakening is available which would not split up the typeclass hypothesis, choose that weakening instead (even if it is technically less general).
prefer : SplitPolicy
Always suggest the most general weakening, even if that means suggesting a split where a less general non-splitting weakening would be available.

Instances For

source

@[implicit_reducible]

instance GeneralizationLinter.instInhabitedSplitPolicy :

Inhabited SplitPolicy

Equations

GeneralizationLinter.instInhabitedSplitPolicy = { default := GeneralizationLinter.instInhabitedSplitPolicy.default }

source

structure GeneralizationLinter.LinterConfig :

Type

Configuration for the typeclass generalization linter.

absencePolicy : Digraph.Condensation.AbsencePolicy
Establishes how classes that are not vertices of the class graph should be handled.
perDeclHeartbeats : Nat
How many heartbeats the linter may spend analyzing a single declaration. Set this to 0 to remove this limit. The default value is 4_000_000 (4 million), which should suffice for around 88% of emissions. Higher values increase both maximum latency and coverage; for example, a value of 20_000_000 should suffice for around 98% of emissions.
splitPolicy : SplitPolicy
Controls whether typeclass weakenings that would involve splitting a single hypothesis into two weaker ones should be suggested.
Setting this option to .allow will make the linter suggest splitting a typeclass hypothesis only if it could not be weakened otherwise. Setting this option to .prefer will make the linter always suggest the most general weakening, even if that means suggesting a split where a less general non-splitting weakening would be available.
Note: Suggested weakenings that split typeclass hypotheses can violate diamond coherence.
Note: The user can set this property via set_option generalizeTypeclasses.split "…", where … is forbid, allow, or prefer (note: no dot in front).
verify : Bool
subsumption : Bool
conclusionGuard : Bool
vacuityGuard : Bool