How do I force an instance of a typeclass to be used in lean4?

Question

I was trying to learn lean and I accidentaly left the concatenate_junk type input as ˋStringˋ instead of ˋaˋ.

class ConcatenateJunk (a: Type u) where
  concatenate_junk: String -> String

instance: ConcatenateJunk String where
  concatenate_junk := λ x => x

instance: ConcatenateJunk Nat where
  concatenate_junk := λ x => "junk" ++ toString x

#eval ConcatenateJunk.concatenate_junk 42

THis led me think: how can I call ConcatenateJunk.concatenate_junk for the Nat instantiation? Since there's no type argument in the ˋconcatenate_junkˋ, the compiler does not know which instance to pick.

How do I select?

Answer 1

I think you meant:

class ConcatenateJunk (a: Type u) where
  concatenate_junk: a -> String  -- this line has changed

instance: ConcatenateJunk String where
  concatenate_junk := λ x => x

instance: ConcatenateJunk Nat where
  concatenate_junk := λ x => "junk" ++ toString x

#eval ConcatenateJunk.concatenate_junk 42

Your first String should have been an a.

Answer 2

Lean detects that a is not constrained by the type of concatenate_junk and, rather than making it be an implicit argument like usual, it makes it be explicit. You can see this here:

class ConcatenateJunk (a: Type u) where
  concatenate_junk: String -> String

#check ConcatenateJunk.concatenate_junk
/-
ConcatenateJunk.concatenate_junk.{u} (a : Type u) [self : ConcatenateJunk a] (a✝ : String) : String
-/

And so, in this case to select one or the other, you can just pass a as the first argument.

#eval ConcatenateJunk.concatenate_junk String "hi"
-- "hi"

#eval ConcatenateJunk.concatenate_junk Nat "hi"
-- "junkhi"

In general, you can use keyword arguments:

#eval ConcatenateJunk.concatenate_junk (a := String) "hi"
-- "hi"