んもー

natRight : {a : Nat} {b : Nat} -> a NatPair b -> Nat
natRight (a natPair b) = b

getNatRight : {a : Nat} {b : Nat} -> a NatPair b -> Val b
getNatRight (a natPair b) = val b

valNat : (a : Nat) -> Val a
valNat a = val a

body : (length (filter p xs')) NatPair (length xs')
body = filterproof {X} {p} { xs'}

right : Val (length xs')
right = getNatRight body

これだと良いのに

right' : Nat
right' = natRight body -- body = filterproof
right : Val (length xs')
right = valNat right'

これだとダメだなんて・・・。

しんきんぐたーいむ

これはエラーとしては

natRight filterproof != length xs' of type Nat
when checking that the expression valNat (natRight body) has type
Val (length xs')

というのが出てて、
body = filterproofだというのはそうで、

right' = natRight body = natRight filterproof

とみると、valNatの定義から

right : Val (natRight filterproof)

で自明じゃないので、確かにそうなりますっていう。

しかしながら気持ちとしては

right' = natRight body

から

right' が length xs'であって欲しい

と思っていて、そうすると

right = val right'

でunify可能だよなーとか。

ただそれは、「値の話」なので「実行されて」はじめて分かる事で、そうするとやっぱり型だけで片付けられないと困るんですけど、上のだとガチガチなのでうーんとか。

少なくとも構成物のうちにリテラルが含まれている場合は、それはどうも実行してくれて型レベルのパラメタに活かしてる気がしますけど。勘て感じです。
まぁガンガンad-hocに書いていってみるかな。