string unification

Stream: lean4

[Colin S. Gordon]

I have been bumping into a seeming confusion with (I presume, perhaps incorrectly) the special status of string literals in Lean. Consider:

class Good (s:String) where
  blah : Unit
instance g1 : Good (String.mk ['1']) where
  blah := ()
def onlyGood (s:String)[Good s] : String := s
-- next line Failed to synthesize instance Good "1"
theorem chk : onlyGood "1" = String.mk ['1'] := by rfl
-- but
theorem but : "1" = String.mk ['1'] := by rfl

In principle all strings are constructed by application of String.mk. In practice, uses of String.mk don't seem to unify with the corresponding literal. Admittedly this is probably not a common use case for Lean. But I have a few different use cases where I really want to be able to unify string literals with strings that are programmatically constructed in some way (either by typeclass instance search, or by manually constructing a string literal via String.mk, List.cons, and so on in a macro. Is there a trick to doing this? or alternatively, if I construct a string in a macro, is there a reasonable way to get the macro to emit a string that will in fact unify with a literal written by hand in the source code?

[Mario Carneiro]

Although "1" = String.mk ['1'] is defeq, this is not provable with only unfolding reducible definitions, which is what instance search does

[Mario Carneiro]

this isn't anything specific to string literals; if you have instance : Good 1 where def one := 1 then Good one won't be found

[Mario Carneiro]

Colin S. Gordon said:

if I construct a string in a macro, is there a reasonable way to get the macro to emit a string that will in fact unify with a literal written by hand in the source code?

Yes, if you have a string s in a macro then quote s is a string literal you can put into the generated term

[Mario Carneiro]

import Lean

macro "my_quote" n:ident : term =>
  let s := n.getId.toString
  `($(Lean.quote s))

#check my_quote hi.mom
-- "hi.mom" : String

class Good (s : String)
instance : Good (my_quote hi.mom) := {}
def onlyGood (s : String) [Good s] : String := s
example : onlyGood "hi.mom" = "hi.mom" := rfl

[Colin S. Gordon]

thanks!