Two `noncomputable` errors

Stream: lean4

[Kevin Buzzard]

There are two ways that Lean can tell you "you should have made this noncomputable". One is the nice error

failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Classical.choose', and it does not have executable code

but there's a much messier one where you get something like

compiler IR check failed at '_example._rarg', error: unknown declaration 'MvPolynomial.instCommRingMvPolynomial'

which people occasionally ask about on the Zulip (because it's not clear how to fix this unless you know the trick). Can someone tell me how to trigger this error with a simple example?

[Henrik Böving]

The second error is not an error the user made but the fact that it wasn't caught earlier is a bug. If this message shows up it means you are already several steps into code generation and something went wrong along the way so these should not occur in a bug free compiler. And then you can silence them by using noncomputable because that disables code generation. But really whenever this happens this should be reported as a bug to core.

[Kevin Buzzard]

I want to test the conjecture that if a file in a project has an example which throws that error then if you lake build twice, the second time there is no error reported. Sounds unlikely but I'm trying to figure out what happened to me earlier when I thought a build was compiling but it was actually failing because of an example throwing that error.

[Kevin Buzzard]

Here's an example using mathlib (due to Antoine Chambert-Loir):

import Mathlib.Algebra.RingQuot
import Mathlib.RingTheory.Ideal.QuotientOperations
import Mathlib.Data.MvPolynomial.CommRing

inductive r (R : Type) [CommSemiring R] (M : Type) : (MvPolynomial M R) → (MvPolynomial M R) → Prop

variable (R : Type) [CommRing R] (M : Type)

instance foo : CommRing (RingQuot (r R M)) :=
  RingQuot.instCommRingRingQuotToSemiringToCommSemiring (r R M)
/-
compiler IR check failed at 'foo._rarg', error: unknown declaration 'MvPolynomial.instCommRingMvPolynomial'
-/

but I'm having trouble minimising. Here's an attempt:

noncomputable def MvP (α : Type) : Type := Prod α $ Fin $ Classical.choose (⟨37, rfl⟩ : ∃ (x : Nat), x = x)

class Rng (α : Type) where
  n : Nat

noncomputable instance MvP.instCommRingMvPolynomial (α : Type) [Rng α] : Rng (MvP α) where
  n := Classical.choose (⟨37, rfl⟩ : ∃ (x : Nat), x = x)

instance Rng.instCommRingRingQuotToSemiringToCommSemiring (α : Type) [Rng α] (r : α → α → Prop) : Rng (Quot r) where
  n := 42

inductive r α : MvP α → MvP α → Prop

instance foo (α : Type) [Rng α] : Rng (Quot (r α)) :=
  Rng.instCommRingRingQuotToSemiringToCommSemiring (MvP α) (r α)

but it doesn't work. I'm wondering whether it doesn't work because I am not very good at making things which the compiler can see are actually noncomputable. In Lean 3 you would get an error if you marked something computable as noncomputable, but I'm just realising that Lean 4 doesn't do this (for example I thought MvP was noncomputable but now I realise it's not). I wonder whether actually making these things noncomputable would make my example work.

[Kevin Buzzard]

def MvP (α : Type) : Type := Classical.choose (⟨Nat, rfl⟩ : (∃ X : Type, 1=1)). How can that be computable? How do I make a noncomputable type?

[Henrik Böving]

Terms of type Sort u don't have a (meaningful) runtime representation for all u so there is no way to make them noncomputable.

[Henrik Böving]

You basically have to think of it like this: If the type checker already confirms to us that the code is valid there is no reason to keep types around at runtime, no matter how funkily computed they are, we already have a proof (via the type checker) that the code is not going to behave in ways that do not interact properly with the data that it is given.

[Henrik Böving]

In addition to this we can also erase all proofs since propositions are subsingletons so there is no reason to keep them around either. Both of these properties allow us to write code that uses a lot of dependent types and proofs with very little cost as we can strip all of this away after the fact and quite often the generated code ends up looking at least very closed to the code you would've written if you had just not involved proofs. A good example of this is a subtype val : {x : Nat // P x} val will have the same runtime representation as val' : Nat.

[Mario Carneiro]

minimized:

class More (R : Type) extends Mul R, Add R

def Foo (R : Type) [Sub R] := R

noncomputable instance bar {R} [Sub R] : More (Foo R) := sorry

instance foo {R} [Sub R] : Add (Foo R) := inferInstance
-- compiler IR check failed at 'foo._rarg', error: unknown declaration 'bar'

[Scott Morrison]

I think this is essentially a duplicate of https://github.com/leanprover/lean4/issues/1785. I'll add Mario's minimization to that issue.

[Matthew Ballard]

    compilation 89.7s
    compilation new 397ms

I like the new compiler :)

[Mario Carneiro]

to be fair, the new compiler isn't done yet