Deriving Inhabited

Stream: lean4

[Bolton Bailey]

I have this error below. What is the Deriving Inhabited line doing? I thought it basically either does what the commented out part does, or else errors. How can I see what instance it creates?

import Mathlib.LinearAlgebra.Lagrange

structure SparseMatrix (u v α : Type) where
  (k : ℕ)
  (row : Fin k -> u)
  (col : Fin k -> v)
  (val : Fin k -> α)
deriving Inhabited -- Doesn't work with this

-- -- Works fine with this uncommented
-- instance : Inhabited (SparseMatrix u v α) where
--   default := {
--     k := 0
--     row := Fin.elim0
--     col := Fin.elim0
--     val := Fin.elim0
--   }

def R1CSStmt (F : Type) (n_stmt n_wit rows : ℕ) :=
  (SparseMatrix (Fin rows) (Fin (n_stmt + n_wit)) F)
  × (Fin n_stmt -> F)

def SquareR1CSStmt (F : Type) (n_stmt n_wit : ℕ) := R1CSStmt F n_stmt n_wit (n_stmt + n_wit)

instance [Inhabited F] : Inhabited (SquareR1CSStmt F n_stmt n_wit) where
  default := {
    fst := default -- failed to synthesize instance Inhabited (SparseMatrix
    snd := default
  }

[Floris van Doorn]

whatsnew in <command> gives you a list of all the things <command> does to the environment.

[Floris van Doorn]

so you can write whatsnew in structure ...

[Bolton Bailey]

That's awesome, seems like what's happening is that the derived instance requires Inhabited of u,v,a, which makes sense in retrospect. Thanks!

[Joachim Breitner]

TIL! I was pondering asking for such a command just earlier today :-)

[Kim Morrison]

Yes, whatsnew should move up to Std or Core. PRs doing so welcome. :-)

[Mario Carneiro]

I don't like whatsnew's implementation, it is very inefficient. If we upstream it I would prefer to get some tools in core to have better first class support for this

[Sebastian Ullrich]

It's not quite near-term but work on parallelism will necessarily make it easier to track what was added to the environment by a command

[Mario Carneiro]

I'm hoping for something more like lean 3's "environment modifications" list

[Mario Carneiro]

this is problematic for lean4lean as well, because we lose track of the order in which declarations are added

[Mario Carneiro]

and there was some bug in environment extensions related to this as well IIRC

[Jannis Limperg]

(Aesop could also use this. :))

[Patrick Massot]

I am surprised that deriving Inhabited does not use the default values, is this expected?

structure foo where
  bar : String := "baz"
  deriving Inhabited


#eval (default : foo).bar  -- returns  ""

[Bolton Bailey]

Well, I suppose I would expect it to use the default value rather than the default value. That is, I would expect the derived Inhabited instance of the structure to come from the Inhabited instance of the fields, just like I would expect a derived AddCommMonoid instance to be derived from AddCommMonoid instances of the fields.