[Agda] dimly recalled strings?

[Dan Licata]

Hi Conor, 

On Feb28, Conor McBride wrote:
> Hi folks
> 
> Is there a handy String type I can get hold of by importing
> something or invoking some pragma. I have some dim memory
> of seeing such a thing, but perhaps it was another place,
> another system...

The string module in the library shows how to do this:

http://www.cs.nott.ac.uk/~nad/listings/lib/Data.String.html
  
> Of course, this does rather raise the question of what a
> good presentation of / library for String (or indeed List)
> might be. It may be comforting to duplicate Haskell's
> libraries, but it's inadequate. (I'm not saying "don't
> copy Haskell", I'm saying "expect to bang your head" and
> "keep thinking about it" and "don't standardize too
> early".) Let me phrase this question more concretely: what
> is a good library of *evidence-producing* tests and
> decompositions for lists? how might we write a parser as a
> view, exposing how a string is given by choosing a layout
> for some structured data? But I digress...

Along these lines, in some code I'm hacking on now, I really need the
following:

eq-refl    : (D : String) -> Check (primStringEquality D D)
certify-eq : {D1 D2 : String} -> Check (primStrinEquality D1 D2) -> Id D1 D2

However, I couldn't figure out how to prove these for the builtin
strings---and because I want to run code that uses these, I can't add
them as postulates.  Does anyone know a way to prove these inside Agda?
I couldn't figure out a way, essentially because you can't enumerate all
strings.

My workaround was to explicitly define an enumeration, which is annoying
because certify-eq has a quadratic number of cases.  I guess I could
have used Nat instead, but I kind of want the elements of the
enumeration to be named.

-Dan