synthesizing implicits

Stream: new members

[Quinn]

variable {X : Type}

inductive A : Type :=
| a1 : X -> A

def f' (_ : A) : Bool := True -- don't know how to synthesize implicit argument
def f'' (_ : A Bool) : Bool := False -- A is not a function

def f (_ : @A Bool) : Bool := False --works

I'm finding myself disappointed that I can't do more programming before supplying the concrete instantiations of variables like X. My brain is still in the coq world