From 06b1bf46ce031b4b0d99d71c181ec682e83d174f Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Mon, 21 Oct 2019 11:47:56 -0700 Subject: [PATCH 1/2] doc: elabissues from reid visit --- .../typeclasses_with_emetavariables.lean | 40 +++++++++++++ .../typeclasses_with_preconditions.lean | 60 +++++++++++++++++++ .../typeclasses_with_umetavariables.lean | 41 +++++++++++++ 3 files changed, 141 insertions(+) create mode 100644 tests/elabissues/typeclasses_with_emetavariables.lean create mode 100644 tests/elabissues/typeclasses_with_preconditions.lean create mode 100644 tests/elabissues/typeclasses_with_umetavariables.lean diff --git a/tests/elabissues/typeclasses_with_emetavariables.lean b/tests/elabissues/typeclasses_with_emetavariables.lean new file mode 100644 index 000000000000..1a12542bef6d --- /dev/null +++ b/tests/elabissues/typeclasses_with_emetavariables.lean @@ -0,0 +1,40 @@ +/- +The current plan is to allow typeclass resolution to be triggered when there are still +expression metavariables in the goal. + +It will return: + +success: it succeeded without needing to unify a regular metavar with anything +fail: it failed without even getting a chance to unify a regular metavar with anything +wait: it would have needed to unify a regular metavar with something + +If it returns `wait`, the elaborator may try again later after learning more about the goal. + +Note: this only applies to expression metavariables. +See typeclasses_with_umetavariables.lean for a discussion of universe metavariables. +-/ + +class Foo (b : Bool) +class Bar (b : Bool) +class Rig (b : Bool) + +@[instance] axiom FooTrue : Foo true +@[instance] axiom FooToBar (b : Bool) : HasCoe (Foo b) (Bar b) + +/- [success] In the following example, `Foo.mk _ : Foo ?m₁` would coerce to `Bar ?m₁`, +since resolution would succeed without ever needing to unify `?m₁`. -/ +noncomputable def tcSuccess := +[Bar.mk _, Foo.mk _, Bar.mk true] + +/- [failure] In this example, since there is no coercion from `Foo` to `Rig`, +resolution would fail immediately without bothering to wait.-/ +noncomputable def tcFail := +[Rig.mk _, Foo.mk _] + + +@[instance] axiom FooToRig : HasCoe (Foo true) (Rig true) + +/- [wait] In this example, the coercion from `Foo.mk _ : Foo ?m₁` to `Rig ?m₁` +would wait, but then be queried again later and succeed.-/ +noncomputable def tcWait := +[Rig.mk _, Foo.mk _, Rig.mk true] diff --git a/tests/elabissues/typeclasses_with_preconditions.lean b/tests/elabissues/typeclasses_with_preconditions.lean new file mode 100644 index 000000000000..9a68937b4818 --- /dev/null +++ b/tests/elabissues/typeclasses_with_preconditions.lean @@ -0,0 +1,60 @@ +/- +The current plan is to allow instances to have preconditions with registered tactics. +Typeclass resolution will delay these proof obligations, effectively assuming that they will succeed. +If typeclass resolution succeeds, it will return a list of (mvar, lctx) pairs to the elaborator, +which will try to synthesize the proofs and throw a good error message if it fails. +-/ + +class Foo (b : Bool) : Type + +class FooTrue (b : Bool) extends Foo b : Type := +(H : b = true) + +/- This requires the tactic framework and auto_param. -/ +-- @[instance] axiom CoeFooFooTrue (b : Bool) (H : b = true . refl) : HasCoe (Foo b) (FooTrue b) + +instance BoolToFoo (b : Bool) : Foo b := Foo.mk b + +def forceFooTrue (b : Bool) (fooTrue : FooTrue b) : Bool := b + +/- Should succeed (once CoeFooFooTrue can be written) -/ +#check forceFooTrue true (Foo.mk true) + +/- Should fail (even after CoeFooFooTrue can be written -/ +#check forceFooTrue false (Foo.mk false) + +/- +This plan has one limitation, that has so far been deemed acceptable: +it will not support classes with different instances depending on the provability of preconditions. +The classic example is multiplying two elements of `ℤ/nℤ` where `n` is not prime. +Here is a toy version of this problem: + +<< +@[class] axiom Prime (p : Nat) : Prop + +@[instance] axiom p2 : Prime 2 +@[instance] axiom p3 : Prime 3 + +@[class] axiom Field : Type → Type +@[class] axiom Ring : Type → Type + +@[instance] axiom FieldToHasDiv (α : Type) [Field α] : HasDiv α +@[instance] axiom FieldToHasMul (α : Type) [Field α] : HasMul α +@[instance] axiom RingToHasMul (α : Type) [Ring α] : HasMul α + +axiom mkType : Nat → Type + +@[instance] axiom PrimeField (n : Nat) (Hp : Prime n . provePrimality) : Field (mkType n) +@[instance] axiom NonPrimeRing (n : Nat) : Ring (mkType n) + +example (α β : mkType 4) : α * β = β * α +>> + +The issue is that (depending on the order the instances are tried), +the instance involving `FieldToHasMul` will succeed in typeclass resolution, +but the proof will fail later on. + +I (@dselsam) still thinks this plan is a good compromise. +For examples like this, the definition in question (i.e. `Prime`) can be made a class instead +and taken as an inst-implicit argument to `PrimeField`. +-/ diff --git a/tests/elabissues/typeclasses_with_umetavariables.lean b/tests/elabissues/typeclasses_with_umetavariables.lean new file mode 100644 index 000000000000..e61d4d44cb9c --- /dev/null +++ b/tests/elabissues/typeclasses_with_umetavariables.lean @@ -0,0 +1,41 @@ +/- +In constrast to expression metavariables (see: typeclasses_with_emetavariables.lean), +typeclass resolution is not stalled due to the presence of universe metavariables. + +In the current C++ implementation, some (but not all) universe metavariables appearing +in typeclass goals are converted to temporary metavariables. +-/ + +class Foo.{u, v} (α : Type.{u}) : Type.{v} +class Bar.{u} (α : Type) : Type.{u} + +@[instance] axiom foo5 : Foo.{0, 5} Unit + +def synthFoo {X : Type} [inst : Foo X] : Foo X := inst + +set_option trace.class_instances true +set_option pp.all true + +/- +Currently, universe variables in the level params of the *outer-most head symbol* +of the class are converted to temporary metavariables.-/ +noncomputable def f1 : Foo Unit := synthFoo + +def synthFooBar.{u, v} {X : Type*} [inst : Foo.{u, v} (Bar.{u} X)] : Foo.{u, v} (Bar.{u} X) := inst +@[instance] axiom fooBar5.{u} : Foo.{5, u} (Bar.{5} Unit) + +/- +This *nested* universe parameter is not converted into a temporary metavariable, and so this fails.-/ +noncomputable def f2 : Foo (Bar Unit) := synthFooBar + +/- +Here is the trace: +<< +[class_instances] (0) ?x_0 : Foo.{?u_0 ?u_1} (Bar.{?l__fresh.4.77} Unit) := fooBar5.{?u_2} +failed is_def_eq +[class_instances] (0) ?x_0 : Foo.{?u_0 ?u_1} (Bar.{?l__fresh.4.77} Unit) := foo5 +failed is_def_eq +>> + +Note that the universe metavariable in question is converted to a temporary metavariable in only one of the two occurrences. +-/ From 8cff4e82f46ae878ae2f2c651038e0528e142cae Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Mon, 21 Oct 2019 12:07:55 -0700 Subject: [PATCH 2/2] doc: elabissue for bind with existential types --- .../bind_with_existential_types.lean | 55 +++++++++++++++++++ 1 file changed, 55 insertions(+) create mode 100644 tests/elabissues/bind_with_existential_types.lean diff --git a/tests/elabissues/bind_with_existential_types.lean b/tests/elabissues/bind_with_existential_types.lean new file mode 100644 index 000000000000..6e571d962271 --- /dev/null +++ b/tests/elabissues/bind_with_existential_types.lean @@ -0,0 +1,55 @@ +/- +Problem: existential types do not play well with monads. + +``` +class HasBind (m : Type u → Type v) := +(bind : ∀ {α β : Type u}, m α → (α → m β) → m β) +``` + +Even if we fix a universe-polymorphic monad M.{u v} : Type u -> Type v, +the bind operator forces the universes of the two applications of M to be the same. +So, we can not naively write: +-/ + +universes u v +axiom Foo : Type u → Type v +@[instance] axiom fooMonad : Monad Foo + +noncomputable def doesNotWork : Foo Unit := do +x ← pure (5 : Nat); +y ← pure $ x + 3; +Z ← pure (Nat : Type); +pure () + +/- It yields the following error: + +<< +bind_with_existential_types.lean:18:18: error: type mismatch at application + pure Nat +term + Nat +has type + Type : Type 1 +but is expected to have type + ?m_1 : Type +>> +-/ + +/- We can make it work by adding a bunch of ups and downs: -/ + +noncomputable def moreTedious : Foo Unit := ULift.down <$> do + x ← pure $ ULift.up (5 : Nat); + y ← pure $ ULift.up (ULift.down x + 5); + z ← pure (Nat : Type); + pure $ ULift.up () + +/- +Without special elaborator support to insert all the ups and downs, +it would be highly annoying to write State monad code that uses an existential type, +e.g. a structure that simulates a Coq/ML module by bundling a type and a map API on the type. + +Note that one cannot vary universes at all in generic monadic combinators, +no matter how many lifts and downlifts you are willing to perform, +since only definitions can be universe polymorphic. +If a definition takes a monad as an argument, its universe is already fixed. +-/