Global implicits

At the moment, we can fill implicit arguments using meta-variables that are solved by local constraint resolution. If this resolution fails, the program is incomplete and an error should be reported. To achieve a mechanism similar to that of Scala, we could fall back to a global implicit inference instead. That is, if there is a hole a? : Δ → A that cannot be solved locally and where the type A is a global type, we can try to find a definition a : A to solve the meta-variable by a? = \ Δ ⇒ a. This is especially useful for modeling type classes.

Consider, e.g., the record ...

record Functor (F : Type → Type) : Type where
  case map : { this : Functor F } → { A B : Type } → (f : A → B) → (a : F A) → F B

... and the following use-case (where the holes are explicitly named here):

define double : List Natural = 
  map { F? } { this? } { A? } { B? } (mul two) single

While A?, B? and F? can all be solved thanks to the application of the two explicit arguments, this? cannot be solved as it is not used by the remaining arguments. However, when we define ...

define listF : Functor List where
  case map { listF } f Nil ⇒ Nil
  case map { listF } f (Cons head tail) ⇒ Cons (f head) (map { listF } f tail)  

... and search for a definition of type Functor F? (which is Functor List), we can fill in this definition as a solution to the meta-variable this?. Of course, we also have to deal with ambiguous definitions just like Scala. To reduce the solution space, we could also introduce a keyword implicit and mark definitions such as listF to extend the solution space in a controlled manner.