Universe issues with dependent walks

Stream: lean4

[Peter Nelson]

I am trying to tinker with walks in multigraphs and how they relate to simple graphs, and I'm running into a universe issue which is related to the one mentioned in docs#PSigma .

The structure I am trying to define is a walk $x_0, e_1, x_1, \dotsc, e_n, x_n$ in a multigraph, where the $x_i$ are vertices and the $e_i$ are edges. If the $x_i$ and $e_i$ have fixed types, then this is a nice notion of multigraph walk.

However, if we allow $e_{i+1}$ to have a type (sort) that depends on $x_i$ and $x_{i+1}$, then this also generalizes walks in simple graphs, since $e_i$ can be a proof of adjacency. So I really want Sort in the code below.

But the basic definitions give universe problems, like so :

import Mathlib.Data.List.Basic

variable {α β γ : Type*} {ε : α → α → Sort*} {a b c x y z : α}

universe u v

/-- A `DWalk a b` (dependent walk from `a` to `b`) is a list of the form
`a = a₀, e₁, a₁, e₂, ..., eₙ, aₙ = b`, where each `aᵢ` has type `α`,
and each `e_(i+1)` has type `ε a_i a_{i+1}`.

If `ε := fun _ _ ↦ β`, then the `eᵢ` are simply terms (edges) in `β`.
If `G : SimpleGraph α`, then `DWalk G.Adj a b` is equivalent to `SimpleGraph.Walk a b`.

 -/
inductive DWalk {α : Type u} (ε : α → α → Sort v) : α → α → Type (max u v) where
  /-- The `DWalk` with no edges at a vertex `a`. -/
  | nil (x : α) : DWalk ε x x
  /-- Add an edge `(x, e, y)` to the beginning of `w : DWalk y z`. -/
  | cons (x : α) {y z : α} (e : ε x y) (W : DWalk ε y z) : DWalk ε x z

namespace DWalk

/-- a triple `⟨a,b,e⟩` with `e : ε a b` -/
structure Dart {α : Type u} (ε : α → α → Sort v) where
  fst : α
  snd : α
  edge : ε fst snd

/-- The list of darts of a `DWalk`-/
def darts {α : Type u} {ε : α → α → Sort v} {x y : α}  : DWalk ε x y → List (Dart ε)
  | nil x => []
  | cons x (y := y) e W => (Dart.mk x y e) :: W.darts

/-
stuck at solving universe constraint
  ?u.2098+1 =?= max (u+1) v
while trying to unify
  Type ?u.2098 : Type (?u.2098 + 1)
with
  Sort (max (u + 1) v) : Type (max (u + 1) v)

(Same error occurs with `#check List (Dart ε)`)
-/

Is there any way around this?