Agda: my code doesn't type check (how to get implicit arguments right?)

Question

"checkSimple" gets u, an element of the universe U, and checks if (nat 1) can be converted to a agda type given u. The result of the conversion is returned.

Now I try to write a console program and get "someU" from the command line.

Therefore I changed the type of "checkSimple" to include a (u: Maybe U) as parameter (maybe because the input from the console can be 'nothing'). However I can't get the code to type check.

module CheckMain where


open import Prelude

-- Install Prelude
---- clone this git repo:
---- https://github.com/fkettelhoit/agda-prelude

-- Configure Prelude
--- press Meta/Alt and the letter X together
--- type "customize-group" (i.e. in the mini buffer)
--- type "agda2"
--- expand the Entry "Agda2 Include Dirs:"
--- add the directory 



data S : Set where
  nat  : (n : ℕ) → S
  nil  : S

sToℕ : S → Maybe ℕ
sToℕ (nat n) = just n
sToℕ _       = nothing


data U : Set where
  nat     : U

El : U → Set
El nat = ℕ


sToStat : (u : U) → S → Maybe (El u)
sToStat nat           s = sToℕ s


-- Basic Test
test1 : Maybe ℕ
test1 = sToStat nat (nat 1)


{- THIS WORKS -}

checkSimple : (u : U) → Maybe (El u)
checkSimple someU = sToStat someU (nat 1)



{- HERE IS THE ERROR -}

-- in contrast to checkSimple we only get a (Maybe U) as a parameter
-- (e.g. from console input)

check : {u : U} (u1 : Maybe U) → Maybe (El u)
check (just someU) = sToStat someU (nat 1)
check _ = nothing


{- HER IS THE ERROR MESSAGE -}

{- 
someU != .u of type U
when checking that the expression sToStat someU (nat 1) has type
Maybe (El .u)
-}

Answer 1

The issue is quite simple in nature: the resulting type of sToStat depends on the value of its first argument (u : U in your code); when you later use sToStat inside check, you want the return type to depend on someU - but check promises that its return type depends on the implicit u : U instead!

---

Now, let's imagine this does typecheck, I'll show you few issues that would arise.

What if u1 is nothing? Well, in that case we would like to return nothing as well. nothing of what type? Maybe (El u) you might say, but here's the thing - u is marked as an implicit argument, which means the compiler will try to infer it for us from other context. But there's no other context that would pin down the value of u!

Agda will most likely complain about unsolved metavariables whenever you try to use check, which means you have to write the value of u everywhere you use check, thus defeating the point of marking u implicit in the first place. In case you didn't know, Agda gives us a way to provide implicit arguments:

check {u = nat} {- ... -}

but I digress.

Another issue becomes apparent if you extend U with more constructors:

data U : Set where
    nat char : U

for example. We'll also have to account for this extra case in few other functions, but for the purpose of this example, let's just have:

El : U → Set
El nat  = ℕ
El char = Char

Now, what is check {u = char} (just nat)? sToStat someU (nat 1) is Maybe ℕ, but El u is Char!

---

And now for the possible solution. We need to make the result type of check depend on u1 somehow. If we had some kind of unJust function, we could write

check : (u1 : Maybe U) → Maybe (El (unJust u1))

You should see the problem with this code right away - nothing guarantees us that u1 is just. Even though we are going to return nothing, we must still provide a correct type!

First off, we need to pick some type for the nothing case. Let's say I would like to extend U later, so I need to pick something neutral. Maybe ⊤ sounds pretty reasonable (just a quick reminder, ⊤ is what () is in Haskell - the unit type).

How can we make check return Maybe ℕ in some cases and Maybe ⊤ in others? Ah, we could use a function!

Maybe-El : Maybe U → Set
Maybe-El nothing  = Maybe ⊤
Maybe-El (just u) = Maybe (El u)

That's exactly what we needed! Now check simply becomes:

check : (u : Maybe U) → Maybe-El u
check (just someU) = sToStat someU (nat 1)
check nothing      = nothing

---

Also, this is the perfect opportunity to mention the reduction behaviour of these functions. Maybe-El is very suboptimal in that regard, let's have a look at another implementation and do a bit of comparing.

Maybe-El₂ : Maybe U → Set
Maybe-El₂ = Maybe ∘ helper
  where
    helper : Maybe U → Set
    helper nothing  = ⊤
    helper (just u) = El u

Or perhaps we could save us some typing and write:

Maybe-El₂ : Maybe U → Set
Maybe-El₂ = Maybe ∘ maybe El ⊤

Alright, the previous Maybe-El and the new Maybe-El₂ are equivalent in the sense that they give same answers for same inputs. That is, ∀ x → Maybe-El x ≡ Maybe-El₂ x. But there's one huge difference. What can we tell about Maybe-El x without looking at what x is? That's right, we can't tell anything. Both function cases need to know something about x before continuing.

But what about Maybe-El₂? Let's try the same: we start with Maybe-El₂ x, but this time, we can apply (the only) function case. Unrolling few definitions, we arrive at:

Maybe-El₂ x ⟶ (Maybe ∘ helper) x ⟶ Maybe (helper x)

And now we are stuck, because to reduce helper x we need to know what x is. But look, we got much, much farther than with Maybe-El. Does it make a difference?

Consider this very silly function:

discard : {A : Set} → Maybe A → Maybe ⊤
discard _ = nothing

Naturally, we would expect the following function to typecheck.

discard₂ : Maybe U → Maybe ⊤
discard₂ = discard ∘ check

check is producing Maybe y for some y, right? Ah, here comes the problem - we know that check x : Maybe-El x, but we don't know anything about x, so we can't assume Maybe-El x reduces to Maybe y either!

On the Maybe-El₂ side, the situation is completly different. We know that Maybe-El₂ x reduces to Maybe y, so the discard₂ now typechecks!