doc: elabissues from reid visit

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.
+-/

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]

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`.
+-/

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.
+-/