Implicit solving only works for applications

[hmac]

Consider this example:

type Show a = Show { show : a -> String }

showInt : Show Int
showInt = Show { show = $showInt }

showList : Show a => Show [a]
showList = (Show d) => Show { show = ... }

We have Show instances for Int and [], and the latter is parameterised by an implicit Show a. The problem arises when we try to use showList.

main = putLine (show [1,2,3])

First, note that Kite can't currently infer function calls as implicit solutions, e.g. it can't automatically insert showList showInt : Show [Int]. We need to help it out a bit by providing the showList call:

main = let showListInt : Show [Int]
           showListInt = showList
        in putLine (show [1,2,3])

Kite should solve the implicit argument to showList, producing showList showInt, but it doesn't. This is because implicits are only solved in applications, and showList on its own is not an application.

We need to fix this to make implicits a bit more usable.

[hmac]

Changing how we represent implicits might help with this. Say we represent both implicit arguments and parameters using the syntax {{ x }}.

Implicit functions are then normal functions with implicit arguments, and implicit applications similar.

f : {{ Show Int }} -> Int -> String
f = {{ s }} -> n -> "n is #{s n}"

main = putLine (f {{ $showInt }} 5)

When typechecking an implicit function application we go as usual, comparing actual to expected type. If the actual type can be converted to the expected type by inserting some implicit arguments then we do that.

This works fine even if there are explicit applications or implicits present, because we typecheck from the outside in and the expected type will evolve as we traverse inside the application.