`IsString` typeclass isn't actually listed as an instance in `Data.List.Literals`

[rvs314]

I imagine the Data.List.Literals module was intended to allow writing list of characters as string literals (e.g. "foobar" becomes 'f' ∷ 'o' ∷ 'o' ∷ 'b' ∷ 'a' ∷ 'r' ∷ []). However, the IsString instance is never actually listed as an instance, causing the following code to fail:

module Test where

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

theListOfChars : List Char
theListOfChars = "foobar"
-- /home/rvs314/.tmp/Test.agda:10,18-26
-- No instance of type IsString (List Char) 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

However, if the instance is listed explicitly by adding the line instance _ = isString before the declaration of theListOfChars, then it compiles as expected. Is there a reason this instance declaration isn't in Data.List.Literals already? If this isn't intentional, I'd be happy to send a PR with a few tests.

[JacquesCarette]

We segregate instances. In this case, the instance should have been in Data.List.Instances, but it isn't. That is most definitely a bug.

Whether it should also be in here is another matter. I'm not a huge fan of instances but, in this case, I agree that this is surprising. And most likely harmless.

[MatthewDaggitt]

Yes, I think we'd be happy to receive a PR fixing this. Thanks for the report!