error: don't know how to synthesize placeholder

Stream: general

[Bernd Losert]

import tactic
import order.filter.partial
import algebra.support

noncomputable theory
open set filter classical option function open category_theory
open_locale classical filter

constant envelope : ∀ (G X : Type*), G × X → G × X → Prop

namespace envelope
variables {G X : Type*}
constant pure : ∀ (x : X), quot (envelope G X)
end envelope

variables {G X : Type*}
def weakly_adh_restrictive : Prop := ∀ {ℱ : filter X}, (ℱ.map envelope.pure) = (ℱ.map envelope.pure)

When I run this through Lean, it says:

test.lean:17:86: error: don't know how to synthesize placeholder
context:
X : Type u_2,
ℱ : filter X
⊢ Type ?

I'm not sure how to fix this. Which placeholder is it talking about?

[Kevin Buzzard]

I guess G. Lean can't work out G from what you've given it.

[Kevin Buzzard]

def weakly_adh_restrictive : Prop := ∀ {ℱ : filter X}, (ℱ.map (@envelope.pure G _)) = (ℱ.map (@envelope.pure G _))

[Bernd Losert]

Ah, yeah. That makes sense actually.

[Kevin Buzzard]

It can work out X from ℱ but you didn't give it enough clues for G.

[Bernd Losert]

Indeed. Thank you. Hmm... now I need to figure out how many _ to put in the real code when I use @envelope.pure.

[Bernd Losert]

Maybe I should just change the definition of envelope.pure to take G instead of this hackery.