I was in a lousy mood after the CSL paper got rejected, but holy shit my implementation is actually kinda behaving now, so life is sunshine and unicorns and lollipops again. Except, of course, that I am not kidding about the lollipops.
Which is to say, I succeeded at adapting the LLF miniml-with-refs example with only a couple of hiccups. I found myself extremely perplexed at the very end of the process, with exactly one missing case reported:
tppres.elf:201.23-201.24 Error:
Coverage error --- 1 missing case(s):
{K1:cont} {V1:val} {E1:exp} {W1:final} {T1:tp} {T2:tp} {T3:tp} {P1:w}
{Ex1:exec (K1 ; ([x2:val] return (pair* V1 x2))) (ev E1) W1 P1}
{Ok1:ofk K1 (T1 ** T2) T3} {E2:exp} {Oe1:ofe E2 T2} {Ov1:ofv V1 T1}
{Of1:off W1 T3}
|- tpex P1 (ex_pair1 P1 Ex1) Ok1 (ofi_pair1 Oe1 Ov1) Of1.
val it = ABORT : Twelf.StatusBecause, I mean, how the heck is my code failing at something specific to the second stack-machine instruction of pair-formation? Then I went back and found the bug was a typo in the original code:
ofi_pair1 : ofi (pair1 V1 E2) (T1 ** T2) <- ofv V1 T1 <- ofe V2 T2.
A misnamed free variable (should have been E2) meant that too many stack machine instructions were well-typed, so type preservation was false.
So even though it's not really my code (but rather the pre-existing coverage checking that is not really touching the world equational theory at all) finding that bug, it was a great feeling being able to run the tool over a signature that used linear features and find a error in the theorem being claimed rather than just having bugs and barfing unhandled Match exceptions all over my shoes.