# Implicit arguments can trip you

Implicit arguments are very useful. Without them the type declarations could get very noisy. Though they may produce errors that take a while to solve.

## A tip about export modifiers

Before we start, lets add the module definition, this way this is a small literate file. There's something I want to show you there though.

`module Cantrip`

`%default total`

`%access public export`

These are the ways to change the default export modifiers.
Sometimes it's useful to drop `total`

because sometimes
the totality checker trips when you're still working on the program.
Other times I'd prefer this was inverted and I should declare things
`partial`

if I want to disable totality checking.

The `public export`

is the broadest export modifier
and exports everything you write into the module.
I tend to use this because I keep my Idris code in two files when I work on it.
When I get something done I move it into the another file.
This helps a bit with the slow type checker.

Exposing content of proofs outside the module
allows other modules depend on them,
meaning things can break on distance when you change the module next time.
This is why Idris `export`

exposes declarations without their definition.

## Injective functions (again)

Here's a definition of injectivity again.

`Injective : {t,u:Type} -> (t -> u) -> Type`

`Injective f {t} = (x,y:t) -> (f x = f y) -> (x = y)`

There is an implicit. It sows the seed for what we are about to experience.

## List indices and content definitions

First I am going to introduce some more familiar structures.
First we are getting indices of a list.
We also need to know that `XS`

is injective function,
though it is trivial because all constructors are injective.

`data Nth : (xs : List a) -> Type where`

`XZ : Nth (x :: xs)`

`XS : Nth xs -> Nth (x :: xs)`

`XS_inj : Injective XS`

`XS_inj x x Refl = Refl`

The next one is a proposition stating that item is in a list.
This is a bit shorter and easier to handle
than similar structures produced from `Nth`

.

`data In : a -> (xs : List a) -> Type where`

`Here : In x (x :: xs)`

`There : In y xs -> In y (x :: xs)`

In each containment proof there appear to be an index as well.
The `index_of`

function is injective.

`index_of : In x xs -> Nth xs`

`index_of Here = XZ`

`index_of (There k) = XS (index_of k)`

`index_of_inj : Injective Cantrip.index_of`

`index_of_inj Here Here pf = Refl`

`index_of_inj Here (There k) Refl impossible`

`index_of_inj (There k) Here Refl impossible`

`index_of_inj (There k) (There j) pf =`

`cong (index_of_inj k j (XS_inj (index_of k) (index_of j) pf))`

If you try to use the injectivity, you may find out you're in trouble:

`usecase : (f:{v:a} -> In v xs -> In v ys) -> Injective f`

`-> (x:In v xs) -> (y:In w xs) -> (index_of (f x) = index_of (f y)) -> x = y`

`usecase f f_inj x y prf = let`

`test = index_of_inj (f x) (f y) prf`

`in ?usecase_rhs`

You likely get this kind of an error.

`*Sets> :load Cantrip.idr`

`Type checking ./Cantrip.idr`

`Cantrip.idr:38:10-37:`

`|`

`38 | test = index_of_inj (f x) (f y) prf`

`| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~`

`When checking right hand side of usecase with expected type`

`x = y`

`Type mismatch between`

`In w xs`

`and`

`In v xs`

`Holes: Cantrip.usecase`

The implicit variable within the `Injective Cantrip.index_of`

is not entirely filled up, and it is being filled up from the context.
Therefore the `index_of_inj`

only proves that the containment proofs with
same index are same,
when we know that list contains the same variable in that point.

We have to prove this, although it is trivial:

`same_variable : (x:In a xs) -> (y:In b xs)`

`-> (index_of x = index_of y) -> (a = b)`

`same_variable Here Here prf = Refl`

`same_variable Here (There _) Refl impossible`

`same_variable (There _) Here Refl impossible`

`same_variable (There k1) (There k2) prf1 = let`

`prf1 = XS_inj (index_of k1) (index_of k2) prf1`

`in same_variable k1 k2 prf2`

Next going to conclude in the usecase that it's the same variable:

`usecase : (f:{v:a} -> In v xs -> In v ys) -> Injective f`

`-> (x:In v xs) -> (y:In w xs) -> (index_of (f x) = index_of (f y)) -> x = y`

`usecase f f_inj x y prf1 = case same_variable (f x) (f y) prf1 of`

`Refl => let`

`prf2 = index_of_inj (f x) (f y) prf1`

`in f_inj x y prf2`

But we have an another implicit that needs treatment:

`Type checking ./Cantrip.idr`

`Cantrip.idr:45:8-21:`

`|`

`45 | in f_inj x y prf2`

`| ~~~~~~~~~~~~~~`

`When checking right hand side of Cantrip.case block in usecase at Cantrip.idr:42:33-62 with expected type`

`x = y`

`When checking an application of f_inj:`

`Type mismatch between`

`f w x = f w y (Type of prf2)`

`and`

`f v6 x = f v6 y (Expected type)`

`Specifically:`

`Type mismatch between`

`f w y`

`and`

`f v6 y`

`Holes: Cantrip.usecase`

It doesn't let you to fill it up directly, for some reason it thinks that you fill up non-implicit arguments as well:

`Cantrip.idr:40:56-74:`

`|`

`40 | usecase : (f:{v:a} -> In v xs -> In v ys) -> ((q:a) -> Injective (f {v=q}))`

`| ~~~~~~~~~~~~~~~~~~~`

`When checking type of Cantrip.usecase:`

`When checking an application of Cantrip.Injective:`

`Type mismatch between`

`In a v6 ys (Type of f v6 _)`

`and`

`t -> u (Is f v6 _ applied to too many arguments?)`

`Specifically:`

`Type mismatch between`

`In a v6`

`and`

`\uv => t -> uv`

Passing it in at the argument of the `Injective`

works though.

`usecase : (f:{v:a} -> In v xs -> In v ys)`

`-> ((q:a) -> Injective f {t=In q xs})`

`-> (x:In v xs) -> (y:In w xs)`

`-> (index_of (f x) = index_of (f y)) -> x = y`

`usecase f f_inj {v} x y prf1 = case same_variable (f x) (f y) prf1 of`

`Refl => let`

`prf2 = index_of_inj (f x) (f y) prf1`

`in f_inj v x y prf2`

The errors due to implicits tend to happen frequently. They will surprise you because they can point out mismatches between variables that you have already forgotten you had, or that you think should just match up. It can take a while to figure it out when you meet an error where implicit variables do not match up.

I'm not sure how would I improve the type declarations I presented here. But anyway I'm finished with the post for today.