Plan for linear implicit arguments

[aspiwack]

In order to isolate the OutsideIn part constraint solving from the type-class resolution. Let's start with doing linear implicit arguments.

The steps to try and reach, in order, or how complex we expect them to be are:

1. A function of a linear implicit argument, uses it twice (like return (?x, ?x)). Throws a type error.
2. A function of a linear implicit argument, passes it twice (implicitly) to linear implict argument functions. Throws a type error.
3. A function, returns a linear implicit argument (via a data constructor). Doesn't use. Throws a type error.
4. A function, returns a linear implicit argument. Passes it (implicitly) to a linear implicit argument function. Typeckecks.

[aspiwack]

Some observations from today:

• Constraint solving assumes that there are no duplicate constraints. So there is never a choice between two dictionnaries/implicit arguments. So we don't need multiplicities to inform choice: we only need to check that the only possible solution is correct.
• There is a shadowing semantics, ensuring that the latest solution to a constraint is always preferred. Including for type-classes. Which is exactly what we need to return values.
• Since constraint solving happens “globally”, we need to return, in the typechecker, something which will allow us to check correctness after the fact.

For the last point, I was thinking doing something like piggybacking on the usage environment to produce, at the same time, a formula whose atoms are holes, and connectives are +, sup, scaling, and probably some binding (for deleteUE). We can then use that formula to produce and check a usage environment after the holes have been filled.

[kcsongor]

To expand on your last point, consider this function:

foo :: (?x :: Int) =>. (Int, Int)
foo = (?x, ?x)

The elaborator first replaces the calls to ?x with holes for the evidence which are then yet to be filled in by the constraint solver:

fooElab ::  (?x :: Int) ->. (Int, Int)
fooElab $given = ($wanted1, $wanted2)

The $given is the given evidence that can be used to fill in the holes. I hacked up a quick implementation which records as UsageEnv in the constraint solver that tracks the number of times the $given evidence is used to discharge holes. In this case, the solution generated by the constraint solver is

$wanted1 := $given
$wanted2 := $given

which uses the given evidence twice, and thus fails.

This gets more complicated in the following case:

bar :: (?x :: Int) =>. Bool -> Int
bar b = case b of
  True -> ?x
  False -> ?x

Here, the implicit argument is used correctly in both branches. So, we first generate the holes

barElab:: (?x :: Int) ->. Bool -> Int
barElab $given b = case b of
  True -> $wanted_1
  False -> $wanted_2

which, again, get solved by the constraint solver:

$wanted_1 := $given
$wanted_2 := $given

The constraint solver is completely oblivious to the shape of the program where the constraints originate from, and so the naive check erroneously blows up here.

So, an idea is to come up with a formula during constraint generation that properly records the hierarchy of the term.

[aspiwack]

f :: A -> B
f’ :: A ->. B
h :: A ->. B -> B

g :: (?x :: A) =>. Bool -> B
g True = h ?x (let ?x = a in f ?x)
g False = f’ ?x

Here is an example of something which ought to work but illustrate many of the difficulties.

[aspiwack]

Examples which need to fail:

f :: A -> B
f’ :: A ->. B
h :: A ->. B -> B

g :: (?x :: A) =>. Bool -> B
g _ = f ?x

g' :: (?x :: A) =>. Bool -> B
g' True = f ?x
g' False = f’ ?x