How to infer arg types in application (meta)

Stream: lean4

[Tomás Díaz]

I was trying to infer the types of arguments in an application during elaboration but inferType returns the expected types. I was wondering if there is a way to obtain the real types of arguments and not the expected ones. For instance, in the following application: (fun x : Bool => x) 1, I would expect 1 to have type Nat, but inferType returns Bool.

I had the following elaboration procedure (silly example):

elab "≪" t:term "≫" : term => do
  let elabT <- elabTerm t none
  if isApp elabT then
    let fn := getAppFn elabT
    let args := getAppArgs elabT
    let argTypes <- args.mapM (fun arg => inferType arg)
    ... -- extra things  where types/terms are fixed

#reduce ≪ (fun x : Bool => x) 1 ≫
-- 1
-- failed to synthesize instance
--  OfNat Bool 1

and argTypes indeed returns the types that fn expects.
Is there a way to obtain the real types? Am I missing something obvious, or some other more idiomatic way to do it, etc?

[Henrik Böving]

There is no " the real types" here, before you are finished with elaboration it is completely unclear what type which piece of syntax has, that is...well literally the job of the elaborator to determine and turn the syntax into core expressions here.

Also 1 doesn't have to have type Nat. As your elaborator correctly demonstrates numeric literals in Lean are polymorphic through the OfNat type class so you could very much declare instances that allow you to turn 0 into false and 1 into true and thus make this thing type check

[Tomás Díaz]

Ty.
Maybe my wording of "the real types" wasn't the best, but I'm still wondering if there is a way to a base type for a given term, regardless of context? As in, if you do #check 1 you do get type 1 : Nat and not 1 : Bool. In an application, you can look at an argument by its own and say that it has a certain type regardless of where it's being used, no?

[Tomas Skrivan]

What you want is likely possible in a roundabout way but this sounds like XY problem. What are you actually trying to achieve and do you have a more complicated example that does not involve numerical constants?

[Tomás Díaz]

I'm trying to insert a cast operator, from a source type to a target type, ie. (fun x : Bool => x) (<Bool <= Nat > 1)

[Tomas Skrivan]

And do you have a more complicated example not involving numerical constants?

[Tomás Díaz]

Sorry, I’m no longer in my pc to write something more elaborate. I guess you could simply use any other inductive type, list A and option. Do you think numerical constants might introduce other things that other types don’t or have a different treatment as literals ? (As in some implicit coercions, etc)

[Tomas Skrivan]

Yes, if you elaborate plain 1 you get

@OfNat.ofNat.{?u.3} ?m.2 1 ?m.4

where ?m.2 is a hole/meta variable for the type of 1 and ?m.4 is a hole/meta variable for the instance OfNat ?m.2 1 which provides the actual value. So the type of 1 is in fact an undetermined type ?m.2.

The type ?m.2 is usually determined from the context, e.g. if you apply 1 to fun x : bool => x than Lean determines that ?m.2 has to be Bool. You can force Lean to fill ?m.2 without a context and you get Nat because there is an instance OfNat Nat .. with default_instance attribute.

---

You can play around with this using this meta code:

import Lean

set_option pp.all true in
open Lean Meta Elab Term in
#eval show TermElabM Unit from do
  let one ← elabTerm (← `(1)) none
  IO.println (← ppExpr one)
  synthesizeSyntheticMVarsNoPostponing
  IO.println (← ppExpr one)

which prints

@OfNat.ofNat.{?u.3} ?m.2 1 ?m.4
@OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)

---

For other types, the elaborator usually adds the expected cast

#check (fun x : Option Bool => x) true

prints

(fun x => x) (some true) : Option Bool

[Tomás Díaz]

Mmmhhhhhh interesting, thank you very much!