Add instances of IsString (List Char)

[rvs314]

As discussed in #2745, adds instances of IsString (List Char) to Data.List.Instances and Data.List.Literals. If these changes need tests I can add some.

There's a small potential for confusion in the current configuration, however. The Constraint field of List Char's isString is the constant function λ _ → ⊤, so an instance of ⊤ must be in scope. This means that a user which includes Data.List.Instances but does not have tt defined will get an error.

For example,

open import Data.List.Base
open import Data.Char.Base
open import Data.List.Literals
open import Agda.Builtin.FromString

theListOfChars : List Char
theListOfChars = "foobar"

{- No instance of type isString .IsString.Constraint "foobar" was
   found in scope.
   when checking that "foobar" is a valid argument to a function of
   type
   {a : Agda.Primitive.Level} {A : Set a} ⦃ r : IsString A ⦄
   (s : Agda.Builtin.String.String) ⦃ _ : r .IsString.Constraint s ⦄ →
   A -}

[rvs314]

Additionally, the HACKING.md file mentions that related modules should have parallel updates when reasonable. It seems like adding similar instance declarations for something like Data.List.NonEmpty, Data.Vec, or Codata.Sized.Colist would fit that bill, but no IsString instances are defined in those modules. I'd be happy to add those instances as well, if the court would look favorably upon it.

[JacquesCarette]

I would think those would be worth a parallel PR. And it might not be bad to wait a day, so see what comments come in on this one.

[JacquesCarette]

So I think this is backwards (unfortunately). We want instances declared in Data.List.Instances so that people who don't want them can avoid them entirely.

We do want isString defined here - just not as an instance.

[rvs314]

Sorry - I misinterpreted the response to the issue. I've removed the instance declaration from that module.

[jamesmckinna]

You'll also need CHANGELOG entries to record the additions...

[rvs314]

You'll also need CHANGELOG entries to record the additions...

Thanks for catching this. I've added the change under "Minor Improvements".

[jamesmckinna]

You'll also need CHANGELOG entries to record the additions...

Thanks for catching this. I've added the change under "Minor Improvements".

Actually: you need to do this under Additions to existing modules... Sorry not to have been more explicit ;-)

[rvs314]

Actually: you need to do this under Additions to existing modules... Sorry not to have been more explicit ;-)

No worries; I just amended the commit.

[JacquesCarette]

There's a whitespace problem that will need fixed.

[rvs314]

Sorry, didn't see that! It should be fixed now (or, at least, the tool gives no complaints)

[jamesmckinna]

For some reason, your example at the top of not having tt in scope didn't display?

I was curious to look at it, not least because my (probably faulty!) impression is that no explicit use of tt need ever appear in stdlib, because it is uniquely inferrable (as the single constructor of a record with eta) from _. And that it's thus inferrable even when Data.Unit.Base.⊤ has not explicitly been brought into scope (this is perhaps where I'm mistaken?). Happy to be corrected on this!

[jamesmckinna]

I'm happy to take this off the docket and merge it now for v2.3,unless there are violent objections!?