[Agda] non-constructor indices

[Dan Licata]

Hi Agda hackers,

I have a question about inductive families that use non-constructor
indices.  For example:

   data Nat : Set where
     Z : Nat
     S : Nat -> Nat
   
   plus : Nat -> Nat -> Nat
   plus Z n = n
   plus (S m) n = S (plus m n)
   
   data Indexed : Nat -> Set where
     B : Indexed Z
     I : {n m : Nat} -> Indexed n -> Indexed m -> Indexed (plus n m)

Say I want to defined a recursive function over Indexed Z, a
specialization of the index, such as: 

  height : Indexed Z -> Nat

If I try to do this directly, I run into trouble:

  {- Version 1:
  height : Indexed Z -> Nat
  height B = Z 

  /afs/cs.cmu.edu/user/drl/rsh/progind/code/agda/Bug.agda:17,1-13
  Panic: failed to split: CantSplit Bug.I
  when checking the definition of height
  -}

  {-
  -- Version 2: use identity

  data Id : Nat -> Nat -> Set where
    Refl : {n : Nat} -> Id n n
  
  subst : {n m : Nat} (P : Nat -> Set) -> Id n m -> P n -> P m
  subst P Refl x = x
  
  invert-plus-z-2 : {n m : Nat} -> Id (plus n m) Z -> Id m Z 
  invert-plus-z-2 {Z} id = id
  invert-plus-z-2 {S _} ()

  height : {n : Nat} -> Id n Z -> Indexed n -> Nat
  -- can't write (same Panic as above): 
  --  height {Z} Refl B = Z
  --  height {Z} id   B = Z
  -- same thing happens if you make the 1st arg explicit

  -- this version type-checks but has unsolved metas:
  height id B = Z
  height id (I i1 i2) = height {_} (invert-plus-z-2 id) i2
  -}

The only way I've been able to successfully write the code is by using
identity in the datatype itself:

  data Indexed : Nat -> Set where
    B : Indexed Z
    I : {n m k : Nat} -> Indexed n -> Indexed m -> Id (plus n m) k -> Indexed k

And, to avoid termination problems, I have to use identity in the
theorem as well:
  
  {-
  -- termination problems:
  height : Indexed Z -> Nat 
  height B = Z
  height (I {n} {m} p1 p2 id) = height (subst Indexed (invert-plus-z-2 {n} {m} id) p2)
  -}

  -- OK!
  height2 : {n : Nat} -> Indexed n -> Id n Z -> Nat 
  height2 B Refl = Z
  height2 (I {n} {m} p1 p2 id) Refl = height2 p2 (invert-plus-z-2 {n} {m} id)

My question: does anyone know of any better solutions than what I've
come up with here?

Thanks!
-Dan