Zulip Chat Archive

Stream: general

Topic: instance not working

Frederick Pu (Jan 27 2026 at 00:56):

The last instance in the following isn't working. Does anyone know why?

@[reducible]
def NDMatrix (α : Type u) : List Nat → Type u
| [] => α
| (a::l) => Fin a → NDMatrix α l

instance {α : Type u} [Nonempty α] {shape : List Nat} : Nonempty (NDMatrix α shape) := sorry

instance {α : Type u} [Sub α] {shape : (List Nat)} : Sub (NDMatrix α shape) := sorry
/-
failed to synthesize
  Sub (NDMatrix α [0])

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
-/
instance{α : Type u} [Sub α] : Sub (NDMatrix α [0]) := by infer_instance

Aaron Liu (Jan 27 2026 at 01:01):

@[reducible]
def NDMatrix (α : Type u) : List Nat → Type u
| [] => α
| (a::l) => Fin a → NDMatrix α l

instance {α : Type u} [Nonempty α] {shape : List Nat} : Nonempty (NDMatrix α shape) := sorry

instance {α : Type u} [Sub α] {shape : (List Nat)} : Sub (NDMatrix α shape) := sorry

-- Sub (NDMatrix _ _)
#discr_tree_key instSubNDMatrix
-- Sub (∀  (Fin 0))
#discr_tree_key Sub (NDMatrix _ [0])

Aaron Liu (Jan 27 2026 at 01:02):

discrimination tree doesn't match

Eric Wieser (Jan 27 2026 at 02:12):

The good news is that you can import mathlib and it works:

import Mathlib

@[reducible]
def NDMatrix (α : Type u) : List Nat → Type u
| [] => α
| (a::l) => Fin a → NDMatrix α l

instance instNonempty {α : Type u} [Nonempty α] : (shape : List Nat) → Nonempty (NDMatrix α shape)
  | [] => inferInstance
  | _ :: shape => letI := instNonempty (α := α) shape; inferInstance

instance instSub {α : Type u} [Sub α] : (shape : List Nat) → Sub (NDMatrix α shape)
  | [] => inferInstance
  | _ :: shape => letI := instSub (α := α) shape; inferInstance

instance{α : Type u} [Sub α] : Sub (NDMatrix α [0]) := by infer_instance

Aaron Liu (Jan 27 2026 at 02:17):

well that's because of the sub pi instance

Aaron Liu (Jan 27 2026 at 02:18):

I guess that's the only instance you can have if you want to be compatible with mathlib

Frederick Pu (Jan 27 2026 at 02:26):

what's teh sub pi instance?

Aaron Liu (Jan 27 2026 at 02:27):

docs#Pi.instSub

Frederick Pu (Jan 27 2026 at 02:27):

also why does teh second one become a pi?

Aaron Liu (Jan 27 2026 at 02:29):

@[reducible]
def NDMatrix (α : Type u) : List Nat → Type u
| [] => α
| (a::l) => Fin a → NDMatrix α l

variable {α : Type u}

-- `Fin 0 → α`
#reduce (types := true) NDMatrix α [0]

leanprover-community / mathlib