noncomputable checker regression

Stream: lean4

[Tomas Skrivan]

While bumping a project to v4.20.1 I encountered that this code does not compile anymore

import Mathlib

structure Foo where
  spec : Erased Nat
  data : Nat

def foo : Foo where
  spec := Erased.mk (Erased.mk 0).out
  data := 0

with the error

failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Erased.out', which is 'noncomputable'

It used to work on previous versions e.g. v4.16.0, not exactly when the breaking change happened though.

[Yaël Dillies]

This is known. The new compiler is around the corner though, so don't expect this to be fixed (or rather expect it to be fixed by the arrival of the new compiler)

[Tomas Skrivan]

I see, isn't it exactly because the new compiler is enabled already? (I have no idea if it is or not)

[Yaël Dillies]

(at least I believe not)

[Tomas Skrivan]

I see, I just commented out those parts of the code giving me trouble right now and hopefully I will be able to recover it once this is fixed.

[Kyle Miller]

Setting set_option compiler.enableNew true, it looks like it stops at the toMono pass and reports the same "failed to compile definition" error.

[Cameron Zwarich]

The new_codegen branch has some noncomputable fixes for the new compiler that are not yet on master (and I probably wouldn't recommend trying compiler.enableNew without a stage0 update, since lots of things break). With those fixes, the following works as expected:

universe u

def Erased (α : Sort u) : Sort max 1 u :=
  { s : α → Prop // ∃ a, (a = ·) = s }

def Erased.mk {α} (a : α) : Erased α :=
  ⟨fun b => a = b, a, rfl⟩

noncomputable def Erased.out {α} : Erased α → α
  | ⟨_, h⟩ => Classical.choose h

structure Foo where
  spec : Erased Nat
  data : Nat

def foo : Foo where
  spec := Erased.mk (Erased.mk 0).out
  data := 0

[Mario Carneiro]

@Cameron Zwarich If you are looking at Erased, can I just take the opportunity to earnestly ask you to build native support for Erased into the compiler? The above construction doesn't work, not really, at least in the old compiler. I would much prefer Erased was just a structure wrapper which magically had a switched out representation and a noncomputable .out projection. It would also be nice if the construction given works, but that means ensuring that subtypes of erased things are erased and pi types with erased codomain are erased.

[Mario Carneiro]

You should just be able to make things erased as a kind of annotation, rather than hardcoding it to types and proofs. (People want a type system around that but that sounds much farther from reality than an extensible mechanism for erasure via annotation)

[Mario Carneiro]

It's unclear to me if Erased can be an identity function, which would make it even more annotation-like, similar to outParam

[Cameron Zwarich]

This construction does work with the new compiler (and a version of it is checked in as a test now), giving this IR:

[Compiler.IR] [result]
    def Erased.mk (x_1 : ◾) (x_2 : @& obj) : ◾ :=
      ret ◾
    def Erased.mk._boxed (x_1 : obj) (x_2 : obj) : obj :=
      let x_3 : ◾ := Erased.mk x_1 x_2;
      dec x_2;
      ret x_3
[Compiler.IR] [result]
    def foo._closed_0 : obj :=
      let x_1 : obj := 0;
      let x_2 : obj := ctor_0[Foo.mk] x_1;
      ret x_2
    def foo : obj :=
      let x_1 : obj := foo._closed_0;
      ret x_1

I'm actually not immediately sure why the trivial structure optimization isn't kicking in here for Foo.