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.

Similar posts