Type class instance comparison with/-out naming, with/-out include

instance_comparison.lean

/-
First, we add the necessary preliminary declarations:
-/

import data.list
open list

variable {A : Type}

/-
In the following section, we use `insert` without the required `decidable_eq A`
instance.
-/

section errors1
check λ(a : A) (l : list A), insert a l              -- error: failed to synthesize placeholder: decidable_eq A
example (a : A) (l : list A) : list A := insert a l  -- error: failed to synthesize placeholder: decidable_eq A
end errors1

/-
The errors make sense. Since there is no instance, the placeholder cannot be
synthesized.

In the next section, we add that instance with a `variable` declaration.
-/

section no_errors1
variable [decidable_eq A]
check λ(a : A) (l : list A), insert a l
example (a : A) (l : list A) : list A := insert a l
end no_errors1

/-
This instance appears to be used throughout the `section`, resolving the
missing placeholder.

In the next section, we give that instance a name.
-/

section errors2
variable [H : decidable_eq A]
check λ(a : A) (l : list A), insert a l
example (a : A) (l : list A) : list A := insert a l  -- error: failed to synthesize placeholder: decidable_eq A
end errors2

/-
Now, something strange has happened. The instance appears to be available to
the `check` command but not to the `example`. But the only difference between
`no_errors1` and `errors2` is that we added a name.

In the next section, we `include` the named instance.
-/

section no_errors2
variable [H : decidable_eq A]
check λ(a : A) (l : list A), insert a l
include H
example (a : A) (l : list A) : list A := insert a l
end no_errors2

/-
We have resolved the error in `errors2`. But it's strange that the `include` is
necessary for the `example` and not for the `check`.

The difference between the use of the named instance in `check` and `example`
caused me some difficulty in trying to figure out why my proof was getting an
error.

In the last section, we use the named instance explicitly.
-/

section no_errors3
variable [H : decidable_eq A]
check λ(a : A) (l : list A), insert a l
example (a : A) (l : list A) : list A := @insert _ H a l
end no_errors3

/-
Except for the lack of error in the `check`, this fits a model of consistency
for variables:

1. All named variables, including instances, in a section are treated
   identically. That is, each variable is prepended to each of the following
   definitions in which that variable is mentioned.

2. Since instances, as an exception, do not necessarily need mentioning, they
   also do not need naming. So, each unnamed instance will be associated with
   each definition in which the instance variables are used.

3. As a an additional level of control that avoids the automated route, named
   instances can be explicitly `include`d and `omit`ted.
-/

Mailing list thread