Prop-valued instances in terms of non-canonical instances

Stream: mathlib4

[Yaël Dillies]

Oh no! Eric is right :scream:

class Foo

class Bar [Foo]

instance canonicalFoo : Foo where

instance barAboutCanonicalFoo : Bar where

def noncanonicalFoo : Foo where

attribute [local instance] noncanonicalFoo in
instance barAboutNoncanonicalFoo : Bar where

#synth Foo -- canonicalFoo
#synth Bar -- barAboutNoncanonicalFoo

[Yaël Dillies]

This is actually terrible. I've been going around in PRs telling people their instances about non-instances are fine to have!

[Eric Wieser]

Your example isn't enough to cause an issue by itself

[Andrew Yang]

Yaël Dillies said:

Oh no! Eric is right :scream:

What's the problem with this snippet?

[Yaël Dillies]

The last line, which I was expecting to be #synth Bar -- barAboutCanonicalFoo

[Yaël Dillies]

Eric Wieser said:

Your example isn't enough to cause an issue by itself

Well it is causing an issue(?)

[Anne Baanen]

Maybe the issue in Yaël's code is that all Foos unify anyway? Since #synth @Bar canonicalFoo still returns barAboutNoncanonicalFoo.

[Yaël Dillies]

I agree I am not raising an issue exactly relevant to Kevin's case

[Andrew Yang]

class Foo where val : Nat

class Bar [Foo]

instance canonicalFoo : Foo where val := 0

instance barAboutCanonicalFoo : Bar where

def noncanonicalFoo : Foo where val := 1

attribute [local instance] noncanonicalFoo in
instance barAboutNoncanonicalFoo : Bar where

#synth Foo -- canonicalFoo
#synth Bar -- barAboutCanonicalFoo

This works fine

[Anne Baanen]

Yeah, this all seems to work as expected if Foo isn't a syntactically trivial type:

class Foo where
  canonical : Bool

class Bar [Foo]

instance canonicalFoo : Foo where
  canonical := True

instance barAboutCanonicalFoo : Bar where

def noncanonicalFoo : Foo where
  canonical := False

attribute [local instance] noncanonicalFoo in
instance barAboutNoncanonicalFoo : Bar where

#synth Foo -- canonicalFoo
#synth Bar -- barAboutCanonicalFoo
#synth @Bar canonicalFoo -- barAboutCanonicalFoo
#synth @Bar noncanonicalFoo -- barAboutNoncanonicalFoo

[Notification Bot]

13 messages were moved here from #mathlib4 > A tensor B is an A-algebra and a B-algebra by Eric Wieser.