Application type mismatch

Stream: lean4

[Kaushik Chakraborty]

Hi, I am having difficulty getting this compiled. Something I am doing wrong.

  def f (x: Sum Nat String) :=
   match x with
    | Sum.inl _ => Nat
    | _ => String

  /-
  failed to synthesize instance
    Inhabited (f s)
 -/
  #reduce (fun (s: Sum Nat String) (xs: Array (f s)) => xs.get! 0) (Sum.inr "") #["1"]

I want to get the Array type inferred based on the type function application at term level.

[Alexander Bentkamp]

The Array.get! function works only on types that are registered as Inhabited:

instance : Inhabited (f s) := by
cases s
all_goals
  simp only [f]
  infer_instance

[Siddhartha Gadgil]

(deleted)

[Kaushik Chakraborty]

So if I want to have have a type level function to determine Array's type and then dispatch the right function at term level how can I achieve that. I want to resolve at type level whether the argument is of type Array Nat or Array String and then at term level want to map the same array and deal with Nat or String values within it as required. Hope my explanation make sense

[Mario Carneiro]

I think Alexander Bentkamp 's code should be sufficient to get your code to work. (However, it's generally not a good idea to have types that change their representation like that, because it does not optimize well.)

You can also use #eval instead of #reduce, although you have to either say the reduced target type or implement Eval (f s) as well, along similar lines to the proof of Inhabited

instance : Inhabited (f s) := by
cases s
all_goals
  simp only [f]
  infer_instance

#eval show String from (fun (s: Sum Nat String) (xs: Array (f s)) => xs.get! 0) (Sum.inr "") #["1"]