# How to set defaults for implicit arguments when they can't be inferred?

If I had a module declared as follows in file A.v:

Section A.
Context {𝒳 : Set}.
Inductive abt := Abt_leaf (x : 𝒳) | Abt_node.
End A.


And in another file, B.v, I had:

Require Import A.
Definition 𝒳 := nat.
Inductive typ := Tpe_num | Typ_str.
Definition typ_to_abt (t : typ) : abt (* @abt 𝒳 *) := Abt_node.


The implicit arguments in abt when defining typ_of_abt can't be inferred.
How could I let Coq know I always want abt to be @abt 𝒳 in B.v? The intent is to avoid explicitly specifying them using @.

• Can you share any concrete example where the problem occurs? Mar 10 at 4:23
• Updated the question. Thanks @Bubbler Mar 10 at 14:04
• Let abt := @abt 𝒳.? Mar 11 at 1:46
• @MikeShulman It is a solution. I think Notation also works. But both need to be repeated for every definition such as abt (when there are many) in A.v. I wonder if there's a more concise solution. Mar 12 at 1:26
• Ah. I don't know a better solution in Coq -- I think in Agda you can do that by passing a parameter to a module. You could conceivably do that in Coq too, but Coq's modules are more heavyweight, and you might run into issues with generativity. Mar 13 at 16:41

Not sure how robust that is, but you can do something quite nice using typeclasses.

Section A.
Class leaf_type := X : Type.
Context {L : leaf_type}.
Inductive abt := Abt_leaf (x : X) | Abt_node.

End A.

Section B.
#[local] Instance nat_leaf : leaf_type := nat.

Inductive typ := Tpe_num | Typ_str.
Definition typ_to_abt (t : typ) : abt := Abt_node.

End B.


To elaborate on what is happening here, we are first declaring a class leaf_type, that Coq will try to infer on its own automatically whenever it can, and abt makes use of that typeclass. In section B, we put this to work: we declare nat as a #[local] instance, so that whenever an implicit argument of type leaf_type is encountered in that section, Coq will find the local instance nat` and be happy with it. Once you close the section, the instance is gone and you can declare another one later on.