inferInstance not working when instance is assumption

Stream: new members

[Matt Diamond]

Running into a bit of weirdness with inferInstance. Here's a toy example that demonstrates what I'm seeing:

import Mathlib

-- This doesn't work
example {α : Type*} : Subsingleton α ∨ Nontrivial α :=
(subsingleton_or_nontrivial α).imp
  (fun h => inferInstance)
  (fun h => inferInstance)

-- This *does* work
example {α : Type*} : Subsingleton α ∨ Nontrivial α :=
(subsingleton_or_nontrivial α).imp
  (fun h => by have := h; infer_instance)
  (fun h => by have := h; infer_instance)

Why would inferInstance fail in the first case?

[Kyle Miller]

This is due to a limitation with how the local instance cache works. The type of the h's are metavariables, so they're not added as local instances. Giving explicit types makes it work:

example {α : Type*} : Subsingleton α ∨ Nontrivial α :=
(subsingleton_or_nontrivial α).imp
  (fun h : Subsingleton α => inferInstance)
  (fun h : Nontrivial α => inferInstance)

The reason they're metavariables is that subsingleton_or_nontrivial α is the third argument to Or.imp, so it's elaborated after the funs.

[Matt Diamond]

Ah okay, good to know.

[Kyle Miller]

Deferring elaboration of the funs works too:

example {α : Type*} : Subsingleton α ∨ Nontrivial α :=
(subsingleton_or_nontrivial α).imp
  (by exact fun h => inferInstance)
  (by exact fun h => inferInstance)

[Junyan Xu]

Maybe I wasn't seeing this because I always use ‹_› instead of inferInstance in such cases:

example {α : Type*} : Subsingleton α ∨ Nontrivial α :=
  (subsingleton_or_nontrivial α).imp (fun _ ↦ ‹_›) (fun _ ↦ ‹_›)