Suppose I have a code with a lot of modules and sections. In some of them there are polymorphic definitions.
Module MyModule.
Section MyDefs.
(* Implicit. *)
Context {T: Type}.
Inductive myIndType: Type :=
| C : T -> myIndType.
End MyDefs.
End MyModule.
Module AnotherModule.
Section AnotherSection.
Context {T: Type}.
Variable P: Type -> Prop.
(* ↓↓ ↓↓ - It's pretty annoying. *)
Lemma lemma: P (@myIndType T).
End AnotherSection.
End AnotherModule.
Usually Coq can infer the type, but often I still get typing error. In such cases, you have to explicitly specify the implicit type with @, which spoils the readability.
Cannot infer the implicit parameter _ of _ whose type is "Type".
Is there a way to avoid this? Is it possible to specify something like default parameters, which will be substituted every time Coq cannot guess a type?