with-pattern result not visible

Question

I am trying to see how to branch into "safely-typed" code. For example, below is meant to call tail only on the safe path - i.e. if the list on input is non-empty. There would be an easy way, of course, to just pattern-match the list, but the idea is to reconcile the result of a function (null) and its use on the right-hand side:

data Void : Set where

data _==_ {A : Set} (x : A) : A -> Set where
  refl : x == x

data Bool : Set where
  True : Bool
  False : Bool

data List (A : Set) : Set where
  nil  : List A
  _::_ : A -> List A -> List A

null : forall {A} -> List A -> Bool
null nil         = True
null (x :: xs)   = False

non-null : forall {A} -> List A -> Set
non-null nil = Void
non-null (x :: xs) = (x :: xs) == (x :: xs)

tail : forall {A} -> (xs : List A) -> {p : non-null xs} -> List A
tail (_ :: xs) = xs
tail nil      {p = ()}

prove-non-null : forall {A} -> (xs : List A) -> (null xs == False) -> non-null xs
prove-non-null nil         ()
prove-non-null (x :: xs)   refl = refl

compileme : forall {A} -> List A -> List A
compileme xs with null xs
...             | True    = xs
...             | False   = tail xs {prove-non-null xs refl}

On the last line agda complains that refl cannot be proven to be of type null xs == False. Why can't it see with-clause has just witnessed null xs is False?

What's the right way about it? How to "extract" the dependency from a seemingly non-dependent results, like Bool type is not dependent on the list xs, but in the context it is?

user3237465 user3237465 · Accepted Answer · 2015-05-02T00:38:03

That's about the inspect idiom. Check the original thread and this stackoverflow question. The current version of inspect in the standard library is from this thread (there are also some explanations).

If you delete the definition of _==_, then you can define compileme as

open import Relation.Binary.PropositionalEquality renaming (_≡_ to _==_)

...

compileme : forall {A} -> List A -> List A
compileme xs with null xs | inspect null xs
...             | True    | [ _ ] = xs
...             | False   | [ p ] = tail xs {prove-non-null xs p}

BTW, what is (x :: xs) == (x :: xs) supposed to mean? It's just

open import Data.Unit
...
non-null (x :: xs) = ⊤

BTW2, you can define type-safe tail as I defined type-safe pred in this answer.

with-pattern result not visible

1 Answers