Promoting free variables in type terms to implicit function arguments

Question

In order for my question to be meaningful, I must provide some background.

---

I think it would be useful to have a dependently typed language that can infer the existence and type of an argument a for a function whose other parameters and/or return value have types that depend on a. Consider the following snippet in a language I am designing:

(* Backticks are used for infix functions *)
def Cat (`~>` : ob -> ob -> Type) :=
  sig
    exs id   : a ~> a
    exs `.`  : b ~> c -> a ~> b -> a ~> c
    exs lid  : id . f = f
    exs rid  : f . id = f
    exs asso : (h . g) . f = h . (g . f)
  end

If we make two (admittedly, unwarranted) assumptions:

1. No dependencies must exist that cannot be inferred from explicitly provided information.
2. Every free variable must be converted into an implicit argument of the last identifier introduced using def or exs.

We can interpret the above snippet as being equivalent to the following one:

def Cat {ob} (`~>` : ob -> ob -> Type) :=
  sig
    exs id   : all {a} -> a ~> a
    exs `.`  : all {a b c} -> b ~> c -> a ~> b -> a ~> c
    exs lid  : all {a b} {f : a ~> b} -> id . f = f
    exs rid  : all {a b} {f : a ~> b} -> f . id = f
    exs asso : all {a b c d} {f : a ~> b} {g} {h : c ~> d}
                 -> (h . g) . f = h . (g . f)
  end

Which is more or less the same as the following Agda snippet:

record Cat {ob : Set} (_⇒_ : ob → ob → Set) : Set₁ where
  field
    id   : ∀ {a} → a ⇒ a
    _∙_  : ∀ {a b c} → b ⇒ c → a ⇒ b → a ⇒ c
    lid  : ∀ {a b} {f : a ⇒ b} → id ∙ f ≡ f
    rid  : ∀ {a b} {f : a ⇒ b} → f ∙ id ≡ f
    asso : ∀ {a b c d} {f : a ⇒ b} {g} {h : c ⇒ d} → (h ∙ g) ∙ f ≡ h ∙ (g ∙ f)

Clearly, two unwarranted assumptions have saved us a lot of typing!

Note: Of course, this mechanism only works as long as the original assumptions hold. For example, we cannot correctly infer the implicit arguments of the dependent function composition operator:

(* Only infers (?2 -> ?3) -> (?1 -> ?2) -> (?1 -> ?3) *)
def `.` g f x := g (f x)

In this case, we have to explicitly provide some additional information:

(* If we omitted {x}, it would become an implicit argument of `.` *)
def `.` (g : all {x} (y : B x) -> C y) (f : all x -> B x) x := g (f x)

Which can be expanded into the following:

def `.` {A} {B : A -> Type} {C : all {x} -> B x -> Type}
        (g : all {x} (y : B x) -> C y) (f : all x -> B x) x := g (f x)

Here is the equivalent Agda definition, for comparison:

_∘_ : ∀ {A : Set} {B : A → Set} {C : ∀ {x} → B x → Set}
      (g : ∀ {x} (y : B x) → C y) (f : ∀ x → B x) x → C (f x)
(g ∘ f) x = g (f x)

End of Note

---

Is the mechanism described above feasible? Even better, is there any language that implements something resembling this mechanism?

Answer 1

This sounds like implicit generalization in Coq.