In a scenario like this, I want a single expression to resolve to multiple instances:
Inductive SR: Prop := Sen | Inf.
Parameter CA S: Prop.
Parameter X: SR -> CA -> Prop -> Prop.
Parameter X': SR -> CA -> Prop -> Set.
Parameter XP: SR -> CA -> Prop -> Type.
Definition iX' (t:bool): SR -> CA -> Prop -> Type := if t then X' else XP.
Context `{b:bool}`{c:bool}`{d:bool}`{s:SR}`{t:SR}`{u:SR}`{k:CA}`{l:CA}`{m:CA}`{o:Prop}`{p:Prop}`{q:Prop}.
Parameter foo: iX' b s k o.
Parameter foo'': iX' d u m q.
Parameter ss: S.
Class CON (f:bool) := an: if f then iX' b s k o -> iX' c t l p -> iX' d u m q else S -> S -> S.
Instance coni: CON true := fun (_:iX' b s k o) (_:iX' c t l p) => foo''.
Instance conj: CON false := fun (_:S) (_:S) => ss.
Check (_: CON false) ss.
Check (_: CON true) foo.
Check (_: CON _) ss.
Check (_: CON _) foo. (*Error: The term "foo" has type "iX' b s k o" while it is expected to have type "S".*)
Is there a way to make the instance resolution work w/ both (_: CON _) foo and (_: CON _) ss? If not, try to succeed in a scenario where the class and/or instances are different, while ... in Check ... ss and Check ... foo is identical, and resolves to functions fun (_:S) (_:S) => ss and fun (_:iX' b s k o) (_:iX' c t l p) => foo'', resp.
Is there any reason to restrict yourself to instances here? If you're already doing this much hackery, you might as well go a bit further and use tactics in terms in notations.
Ltac mkcon arg :=
match constr:(Set) with
| _ => exact ((_ : CON false) arg)
| _ => exact ((_ : CON true) arg)
end.
Notation CON_ arg := ltac:(mkcon arg) (only parsing).
Check (_: CON false) ss.
Check (_: CON true) foo.
Check CON_ ss.
Check CON_ foo.