Last active
April 19, 2022 13:05
-
-
Save alreadydone/1b52f7ea9edf00b7a1fb83f90efd8a33 to your computer and use it in GitHub Desktop.
Unification during typeclass inference leads to exponential blowup.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| --set_option trace.class_instances true | |
| --set_option trace.type_context.is_def_eq_detail true | |
| class comm_ring (n : ℕ) := (ucr : unit) | |
| variable (n : ℕ) | |
| class field extends comm_ring n := (e : empty) | |
| class dvr [comm_ring n] := (u : unit) | |
| instance [c : comm_ring n] : comm_ring n.succ := ⟨id^[19] c.ucr⟩ | |
| instance [field n] : dvr n.succ := ⟨()⟩ | |
| example [comm_ring 0] : dvr 1 := by apply_instance /- (deterministic) timeout (Lean 3 only) -/ |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment