More universe weirdness

Stream: mathlib4

[Patrick Massot]

Compare

import Mathlib.Data.Matrix.Basic

universe u

def test  {R : Type u} (A : Matrix (Fin 2) (Fin 2) R) : ℕ := Id.run do
  let mut B := A
  for _k in [0:3] do
    B := B
  return 1

and

import Mathlib.Data.Matrix.Basic

def test  {R : Type _} (A : Matrix (Fin 2) (Fin 2) R) : ℕ := Id.run do
  let mut B := A
  for _k in [0:3] do
    B := B
  return 1

Can you guess which one will feature an incomprehensible (to me) error message? Do you have an explanation?

[Patrick Massot]

Is it something like "everything monadic will blow up outside of Type 0"?

[Patrick Massot]

Now that I minimized that far and suddenly thought of the Type 0 explanation, I can see that putting everything in Type also fixes my real code.

[Kevin Buzzard]

Are there cases when you would want your real code to apply outside Type (i.e. are you actually using an arbitrary ring)? (I only ask because you spend a lot of teaching time just with reals and naturals)

[Eric Wieser]

Yes, the entire monad framework wants everything to be in the same universe, which means you'd need to ulift [0:3] to the same universe as R (I don't know how to do this)

[Eric Wieser]

@Yaël Dillies and I had some idea on how to change this, but didn't have time to follow through on them

[Patrick Massot]

This is part of an experiment about actually programming something in Lean 4 (see also the discussion about iteration on Fin in the Lean 4 stream), so I definitely intend to use it with actual types such as ℤ of ZMod 5