inferType does not respect ambient transparency

Stream: lean4

[Jannis Limperg]

Due to this withTransparency .default, withTransparency .all $ inferType e does not unfold irreducible constants. Should this be changed (to withAtLeastTransparency .default) or is it important that inferType runs with exactly default transparency?

[Kyle Miller]

Is there an example where inferType needs to unfold constants to succeed? or for your own code to succeed?

I wonder if the reason it's at a specific transparency is for the inferType cache.

[Jannis Limperg]

Indeed it's very possible that this would create a caching issue.

I discovered this when testing an extension of Aesop that allows users to change the transparency used by various rules. One of these rules uses inferType internally and therefore fails on this (synthetic) test case:

@[irreducible] def T := Unit → Empty

example (h : T) (u : Unit) : α := by
  aesop ...

The rule constructs the application h u to derive Empty, but calling inferType on h u fails since it refuses to unfold T in the type of h.

[Kyle Miller]

I see, well at least h u itself fails since T is irreducible. You can't even do with_unfolding_all have := h u, presumably due to the term elaborator using inferType to check if h is a function.

[Kyle Miller]

You can trick it like this: with_unfolding_all have := (id h : Unit → Empty) u (or more generally you can use (id h : (_ : _) → _) u)

[Kyle Miller]

Even though inferType might use a specific transparency, you can always unfold things in the type afterwards.

[Jannis Limperg]

Nice hacks. :D If this behaviour leads to user-facing bugs/inconsistencies involving with_unfolding_all, that seems like an additional argument for change. I imagine it should be possible to address the caching by working with a temporary cache if inferType is used at all transparency.

[Kyle Miller]

Maybe the bug is in this line where inferType does whnf at default transparency.

The reason being is that (I think) the contract for inferType is that it's for terms that pass check, and check does everything at .all transparency. Maybe inferType should use .all in general too?

[Kyle Miller]

I was actually pretty surprised to see the error

function expected
  h u

and wondered whether something was being truncated because it's not the usual one you get, which would be more like

#check true true
/-
function expected at
  true
term has type
  Bool
-/

I doubt we're meant to see it; the elaborator is fine with h u under with_unfolding_all (you can tell because it's the shorter "function expected" error), and I would expect inferType to work for a type correct elaborated term no matter the current reducibility settings.

[Jannis Limperg]

At this point I think we need the core devs to determine whether this is considered a bug. I'll make an issue.

[Jannis Limperg]

lean4#2194