is abbrev supposed to break type positivity checking?

Stream: new members

[JJ]

The following code fails to compile:

import Lean.Data.AssocList
abbrev Dict := Lean.AssocList

inductive Expr where
| abs (name : String) (body : Expr)
| app (func arg : Expr)
| var (name : String)

inductive Value where
| clos (name : String) (body : Expr) (env : Dict String Value)

The error message is very scary and bad (https://github.com/leanprover/lean4/issues/8960) but what's important to know is that Lean takes a problem with the (env : Dict String Value) in the inductive Value declaration. It does not take a problem, however, if the env is written as (env : Lean.AssocList String Value), and indeed that code compiles fine.

Is this expected behavior? I am confused about why Lean cannot infer that Value is a well-founded inductive type when the Dict abbreviation is present, because I would expect it to function exactly as an abbreviation. Thanks for any help in understanding.

[JJ]

I might open this as a bug then, if this looks weird to other people.

[Niels Voss]

abbrevs are the same thing as reducible, inline definitions. The kernel doesn't actually know about what reducible means, so my best guess is that the kernel just sees Dict as a regular definition (although I'm not completely sure the kernel is actually involved here). I think if we wanted to get the kernel to accept this definition, we would either have to modify the kernel to reduce all expressions, which is likely a bad idea, or reduce it before sending it to the kernel, which means that if you do #check Value.clos you will see Lean.AssocList instead of Dict.

[Niels Voss]

I think the way that you get "true" abbreviations is by using notation or macro

[Aaron Liu]

abbrevs also do something to the kernel I think

[Aaron Liu]

Kyle Miller said:

(I just checked the kernel code: abbrev only affects tie-breaking when you have f x1 ... xn =?= g y1 ... yn and something needs to be unfolded. Normally, regular definitions use the heuristic that the more-or-less newer definition gets unfolded. Using abbrev causes the definition to be "newer" than even definitions that haven't been defined yet. There are definitely cases where this is the wrong heuristic, but that doesn't mean that abbrev itself is incorrect. It's worth getting some examples to see what's going on.)

[Kyle Miller]

The behavior is expected (I remember some discussions a couple years ago about how nested inductives be nested through definitions), but I'm not sure if it needs to be a necessary restriction for some reason.

The positivity check itself unfolds definitions. For example, using

abbrev Dict (k : Type) (v : Type) := k → v

is OK.

Looking at the source code, the nested inductive type elimination process doesn't unfold anything. (When there are nested inductive types, the kernel creates a new equivalent recursive inductive type and checks that instead.) This is lean::elim_nested_inductive_fn in src/kernel/inductive.cpp.

[JJ]

Hm, okay. Sorry Kyle, but I don't think I understand what you said... :smile:

[JJ]

Niels Voss said:

abbrevs are the same thing as reducible, inline definitions.

Well, I've had a bit of a question about this, actually. Why are abbrevs disallowed in mutual declarations? Just by virtue of no one implementing them or would this cause other issues?