The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

A probably not so helpful and late reply:

AFAIK there is no way to do an instance local.  Also AFAIK, when a local variable is generalized at the end of the section, then the instances get generalized too, in your case having the effect of converting the instance local_foo into a "default" instance.  A default instance is a "catch all" instance, which in your case triggers because z is a definition, and there is no instance for z.

My 2 late ct.

Best,
Beta

On Tue, Jul 29, 2014 at 12:48 AM, Jason Gross <jasongross9 AT gmail.com> wrote:

Hi,

Is it possible to make a canonical structure instance local?  I can't use the [Local] prefix, as I get the error "Error: This command does not support the "Local" prefix.".  However, I want to trigger the instance that I have when a projection matches a section variable, and if I leave the instance in, I get unrelated canonical structure failures (and the occasional anomaly), such as the following:

Structure foo := { bar : Type; baz : bar }.

Canonical Structure foon := {| bar := nat ; baz := 0 |}.

Definition qux := nat.

Definition z : qux := 0.

Check (eq_refl : baz _ = z).

Section x.

  Variable b : Type.

  Variable p : b.

  Canonical Structure local_foo (bad : False) := {| bar := b ; baz := p |}.

End x.

Goal True.

pose (eq_refl : baz _ = z). (* Error: Cannot infer an internal placeholder of type "False". *)

Thanks,

Jason