[Agda] Re: Do we really want special case casts?

[Samuel Gélineau]

On Mon, Oct 19, 2009 at 6:12 PM, Nils Anders Danielsson
<nad at cs.nott.ac.uk> wrote:
> [...] The key point
> is that it should always be possible to compile Agda's pattern matching
> down to well-typed case trees (where every case does pattern matching on
> a single variable, and every pattern consists of a single constructor
> applied to variables).

Sorry for being so thick-skulled, but I still don't understand.

I assume that the case trees for the functions involved are as follows, right?

≅⇒≡₁ : ∀ {A B}{a : A}{b : B}
     → a ≅ b
     → A ≡₁ B
≅⇒≡₁ prf =          -- goal is (_≡₁_ {Set} A B)
 case prf of        -- case argument has type (_≅_ {A} a {B} b)
   refl {X} {x} ->  -- case argument has type (_≅_ {X} x {X} x)
     refl {Set} {X} -- goal is (_≡₁_ {Set} X X)
pass : {A : Set}{B : A → Set}
     → {x₁ : A}{y₁ : B x₁}
     → {x₂ : A}{y₂ : B x₂}
     → x₁ ≅ x₂
     → y₁ ≅ y₂
     → y₁ ≅ y₂
pass prf-x prf-y =    -- goal is (_≅_ {B x₁} y₁ {B x₂} y₂)
 case prf-x of        -- case argument has type (_≅_ {A} x₁ {A} x₂)
   refl {A} {x} ->    -- case argument has type (_≅_ {A} x {A} x)
                      -- goal is (_≅_ {B x} y₁ {B x} y₂)
   case prf-y of      -- case argument has type (_≅_ {B x} y₁ {B x} y₂)
     refl {Bx} {y} -> -- case argument has type (_≅_ {Bx} y {Bx} y)
       refl {Bx} {y}  -- goal is (_≅_ {Bx} y {Bx} y)


At each step, I assume the goal is rewritten to use the variables
introduced in the case tree, otherwise the pattern-matching doesn't
gain us much. But to my eyes, the following case tree and rewriting
for fail seems just as reasonable as the one for pass:

fail : {A : Set}{B : A → Set}
     → {x₁ : A}{y₁ : B x₁}
     → {x₂ : A}{y₂ : B x₂}
     → y₁ ≅ y₂
     → x₁ ≅ x₂
     → y₁ ≅ y₂
fail prf-y prf-x =      -- goal is (_≅_ {B x₁} y₁ {B x₂} y₂)
  case prf-y of         -- case argument has type (_≅_ {B x₁} y₁ {B x₂} y₂)
    refl {Bx} {y} ->    -- case argument has type (_≅_ {Bx} y {Bx} y)
                        -- goal is (_≅_ {Bx} y {Bx} y)
      case prf-x of     -- case argument has type (_≅_ {A} x₁ {A} x₂)
        refl {A} {x} -> -- case argument has type (_≅_ {A} x {A} x)
          refl {Bx} {y} -- goal is (_≅_ {Bx} y {Bx} y)


As a consequence, I really don't understand why the fact that Agda's
pattern matching is compiled down to case trees should prevent
functions like fail to type-check.

On the other hand, I am totally prepared to accept that Agda can't
type-check functions like fail, since it's easy to work around that
restriction. I just want to make sure I understand why.

– Samuel