[Agda] A puzzle with "with"

[James McKinna]

Dear Agda list,

We have a puzzle concerning the use, semantics, and implementation of "with" in Agda. 

Please find attached a source file with holes, which we cannot fill. We think the problem lies in the fact that in pattern matching clauses, the typechecker is either doing to much reduction, or else not enough, to make "obvious" conversions between types OK. 

Context:

We (myself and Cezary Kaliszyk) are trying to prove some easy things about
insertion sorting.

We have the usual three-way comparison type and a record signature for sorting
which says that the things we wish to sort fit well with the comparison
function.

Now we write "insert" in the usual way ... with a "with" on the
call to the comparison function.

We've tried this both with and without the use of "inspect".
In every case we get complaints from the type-checker, either
that it can't refine the type, or that a feature is not implemented
yet, or that pattern-matching instantiates the wrong part of the type.

In the attached file,
 in sorted_insert, at hole { }0 we need a term of type
    Sorted(x::y::ys), in order to construct one we need
    the result of "comp" (in order to apply sorted_cons2)
    but without "inspect" we do not have it.
 in sorted_insert2, at hole { }3 we used inspect, but
    instead, the type fails to reduce to Sorted(x::y::ys).
 in sorted_insert3 we tried to combine the two "with"s,
    but the expected type and the type of "p" are
    mismatched up to the equality p. Pattern-matching
    has instantiated the type on the lhs but not on the rhs.
 in sorted_insert4 if we try to use "subst" on the missing
    equation, we get
    "Not implemented: type checking of with application".

So, we are now very confused about the implementation and
semantics of "with" in Agda. Can you please explain
how one might solve such a problem and learn how to avoid it in the future.

Regards,

Cezary and James.

-------------- next part --------------
module ulf where 

open import Data.List
open import Data.Bool
open import Relation.Binary.PropositionalEquality

data Compare : Set where
  Lt : Compare
  Eq : Compare
  Gt : Compare

infixl 71 _<->_

data _<->_ (A B : Set) : Set where
  biimply : (A -> B) -> (B -> A) -> (A <-> B)

biimply_fwd : {A B : Set} -> (A <-> B) -> (A -> B)
biimply_fwd (biimply f _) = f

record Order : Set1 where
  field
    A : Set
    Comp : A -> A -> Set
    comp : A -> A -> Compare
    isLtComp : (a b : A) -> (comp a b ≡ Lt) <-> Comp a b
    isEqComp : (a b : A) -> (comp a b ≡ Eq) <-> (a ≡ b)
    isGtComp : (a b : A) -> (comp b a ≡ Gt) <-> Comp a b
    isTrans : {a b c : A} -> Comp a b -> Comp b c -> Comp a c

module Sort (o : Order) where
  A = Order.A o

  insert : A -> List A -> List A
  insert x [] = x ∷ []
  insert x (y ∷ ys) with (Order.comp o x y)
  ...              | Lt = x ∷ (y ∷ ys)
  ...              | Eq = y ∷ (insert x ys)
  ...              | Gt = y ∷ (insert x ys)

  sort : List A -> List A
  sort []        = []
  sort (x ∷ xs) = insert x (sort xs)

  data Sorted : List A -> Set where
    sorted_nil : Sorted []
    sorted_cons : (x : A) -> Sorted (x ∷ [])
    sorted_cons2 : (x y : A) -> (ys : List A) -> Sorted (y ∷ ys) -> (Order.Comp o x y) -> Sorted (x ∷ (y ∷ ys))

  insert_lt : (x y : A) -> (ys : List A) -> Sorted (y ∷ ys) -> (Order.comp o x y ≡ Lt) -> Sorted (x ∷ (y ∷ ys))
  insert_lt x y ys yysp xyp = sorted x cons2 y ys yysp (biimply_fwd (Order.isLtComp o x y) xyp)

  sorted_insert : (x : A) -> (xs : List A) -> Sorted xs -> Sorted (insert x xs)
  sorted_insert x [] _ = sorted_cons x
  sorted_insert x (y ∷ ys) prf with Order.comp o x y
  sorted_insert x (y ∷ ys) prf | Lt = {!  !}
  sorted_insert x (y ∷ ys) prf | Eq = {! !}
  sorted_insert x (y ∷ ys) prf | Gt = {! !}

  sorted_insert2 : (x : A) -> (xs : List A) -> Sorted xs -> Sorted (insert x xs)
  sorted_insert2 x [] _ = sorted_cons x
  sorted_insert2 x (y ∷ ys) prf with inspect (Order.comp o x y)
  sorted_insert2 x (y ∷ ys) prf | Lt with-≡ p = {! !}
  sorted_insert2 x (y ∷ ys) prf | Eq with-≡ p = {! !}
  sorted_insert2 x (y ∷ ys) prf | Gt with-≡ p = {! !}

  sorted_insert3 : (x : A) -> (xs : List A) -> Sorted xs -> Sorted (insert x xs)
  sorted_insert3 x [] _ = sorted_cons x
  sorted_insert3 x (y ∷ ys) prf with inspect (Order.comp o x y)
  sorted_insert3 x (y ∷ ys) prf | Lt with-≡ p with Order.comp o x y
  sorted_insert3 x (y ∷ ys) prf | Lt with-≡ p | Lt = insert_lt x y ys prf {! p!}
  sorted_insert3 x (y ∷ ys) prf | Lt with-≡ p | Eq = {! !}
  sorted_insert3 x (y ∷ ys) prf | Lt with-≡ p | Gt = {! !}
  sorted_insert3 x (y ∷ ys) prf | Eq with-≡ p = {! !}
  sorted_insert3 x (y ∷ ys) prf | Gt with-≡ p = {! !}

  sorted_insert4 : (x : A) -> (xs : List A) -> Sorted xs -> Sorted (insert x xs)
  sorted_insert4 x [] _ = sorted_cons x
  sorted_insert4 x (y ∷ ys) prf with inspect (Order.comp o x y)
  sorted_insert4 x (y ∷ ys) prf | Lt with-≡ p = {! subst (Sorted (insert x (y ∷ ys) | Lt)) (Sorted (insert x (y ∷ ys) | Order.comp o x y)) (sym p) ? !}
  sorted_insert4 x (y ∷ ys) prf | Eq with-≡ p = {! !}
  sorted_insert4 x (y ∷ ys) prf | Gt with-≡ p = {! !}



  sorted_sort : (x : List A) -> Sorted (sort x)
  sorted_sort [] = sorted_nil
  sorted_sort (x ∷ []) = sorted_cons x
  sorted_sort (x ∷ (y ∷ ys)) with (sorted_sort (y ∷ ys))
  sorted_sort (x ∷ (y ∷ [])) | sorted_cons .y = sorted_insert x (y ∷ []) sorted y cons
  sorted_sort (x ∷ (y ∷ (z ∷ zs))) | w = sorted_insert x (insert y (insert z (sort zs))) w