CoercibleStrings toy GHC extension

I'm trying to write a small GHC extension to get my hands on GHC hacking. As suggested by the GHC gitlab wiki, I started off by having a look at this article by SPJ and SM to get a feel for GHC's architecture.

I now have an idea for what I think would be a relatively small GHC extension that I would like to have a crack at as a first attempt at actually modifying GHC's source code: CoercibleStrings. The outcome would be similar in spirit to that of the existing OverloadedStrings GHC extension, however, the latter I believe "only" infers the type (Data.String.IsString a) => a for a string literal l during type checking and then desugars them to fromString l, where fromString :: (Data.String.IsString a) => String -> a is from the typeclass Data.String.IsString.

This comes in handy when using libraries that make frequent use of alternatives to Haskell's standard String type, particularly if we frequently wish to pass in arguments represented as string literals, e.g. libraries used for terminal IO. For instance, consider the logging library simple-logger, which makes frequent use of Data.Text.Text, and contains the function logError :: (?callStack :: CallStack) => MonadIO m => Text -> m ().

Rather than writing something like:

import qualified Data.Text as T
import Control.Logger.Simple

...

    logError . T.pack $ "Some error occured."

Using the OverloadedStrings GHC extension, the last line can be replaced with:

    logError $ "Some error occured."

As Data.Text.Text is an instance of the typeclass IsString, this type checks and desugars to something like:

    ($) logError (fromString "Some error occured.")

This can result in fairly significantly less cluttered code due to these conversions being elided, however, in a fairly similar and common case, where operations applied to the string literal force it to be typed as a String, this benefit is lost. For example, consider:

import qualified Data.Text as T
import Control.Logger.Simple

...

    logError . T.pack $ "Some error occured @ " ++ (show locus) 

Where locus is bound in the enclosing context and has a type that is an instance of the typeclass Show.

Now, due to the type of the concatenation operator, (++) :: [a] -> [a] -> [a], the result of evaluating the expression "Some error occured @ " ++ (show locus) must be of type [a], where a is such that [a] is an instance of the typeclass IsString, i.e. String.

Therefore, in this case, the OverloadedStrings extensions does not help us. To remedy this, I propose the CoercibleStrings GHC extension, which would:

1. Allow the type checker to unify the type String with any instance of the typeclass IsString.
2. During desugaring, insert an application of the function fromString where these coercions are necessary.

Although the architecture of such an extension would be quite different from that of the OverloadedStrings extension, the idea seems quite straightforward, while providing, I would argue, a fairly large advantage over it. This brings me to the question of why it has yet to be implemented.

There seem to me to be a few potential problems with such an extension that I can think of. The first is that, given that String is an instance of the typeclass IsString, a type inference rule of the form

∀a ∈ IsString. Γ ⊢ e :: String => Γ ⊢ e :: a

can be applied to an expression of type String an unbounded number of times. So it may not be possible to modify GHC's type inference algorithm in such a way as to guarantee termination of type checking given the addition of such a rule. I think however that this issue can be prevented by requiring that a is not String and only allowing GHC to apply this rule if no other rules apply.

The second is from point 2) above, which is where to insert the applications of fromString. The simplest answer I guess would be to apply it to every expression of type String and given that the definition of fromString for String is simply id, any unnecessary applications would likely be optimised away. This may of course lengthen compilation times somewhat. I believe however that this could be targeted better given information from the type checker.

The third is that this type of implicit coercion goes against the philosophy of strongly typed languages such as Haskell, or indeed that these implicit coercions may introduce extra run-time costs that will be invisible to the programmer.

The second and third points are not existential issues that would prevent the extension from being written, however, I am unsure if the solution that I am suggesting to the first point actually works/is reasonably implementable within the existing GHC infrastructure/does not interact badly with other existing extensions.

I'd welcome any comment on these points or any pointers to up-to-date information on GHC's type checking algorithm. Thank you!