how to debug unexpectedly noncomputable definitions?

Stream: lean4

[neil]

Heya,

I'm new to lean4, though I have some experience with Rocq. My focus is more in computer science / type theory at the moment, vs more standard mathematics, but I'm trying out lean for a new project because the programming experience seems much nicer than Rocq's.

However, I've run into an issue where a function I've defined is unexpectedly noncomputable, and the message from the compiler is not useful.

The function is quite small, so I can just share the full definition:

def segment (s : sExpr) (b : bitVec s.bitLength) : s.bitType :=
  match s with
  | .Int => .Int b
  | .Bool => .Bool b
  | .List elem_type length =>
           let length_segmented : (elem_type.List length).bitLength = length * elem_type.bitLength := by
             rw[Nat.mul_comm]
           let b_length_segmented := b.cast length_segmented
           let segmented := b_length_segmented.segment elem_type.bitLength (by rfl)
           let decoded := segmented.map (segment elem_type)
           .List decoded

Of the names used here which I've defined, I think Vector.segment and sExpr.bitLength are computable, in that they can be used with #eval commands. sExpr.bitType does not seem to be computable (e.g. #eval sExpr.Int.bitType yields cannot evaluate, types are not computationally relevant) (though I don't know why...), but it's not used in function body, above, only the type signature.

The message from the compiler, regarding segment is the classic

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

So, is there a good way to debug what's going on here?

[Aaron Liu]

Based on only the error message, that's probably a bug in the compiler. Can you make a #mwe so that we can inspect your code independently?

[neil]

sure. and I should post it here?

[neil]

Should I try to reproduce this without relying on my own Vector.segment definition, or just include that, though it'll add maybe a hundred lines to the MWE?

[Aaron Liu]

Shorter is better, but if you can't reproduce the bug then long code is okay too.

[neil]

inductive TagExpr where | Int | Bool | List (n : Nat)

inductive vExpr (α : Type u) : TagExpr → Type u where
  | Int : α → vExpr α .Int
  | Bool : α → vExpr α .Bool
  | List : Vector α n → vExpr α (.List n)


inductive sExpr where
  | Int
  | Bool
  | List (elem_type : sExpr) (length : Nat)

abbrev sExpr.asType (s : sExpr) (α : Type) :=
  match s with
  | Int => vExpr α .Int
  | Bool => vExpr α .Bool
  | List elem_type length => vExpr (elem_type.asType α) (.List length)

abbrev bitVec : Nat → Type
  | n => Vector Bool n


abbrev sExpr.bitLength : sExpr → Nat
  | .Int => 8
  | .Bool => 1
  | .List elem_type length => elem_type.bitLength * length

abbrev sExpr.bitType (s : sExpr) : Type :=
  match s with
  -- NOTE: for some reason, we have to explicitly unroll .asType, otherwise we
  -- get type errors.
  | .List elem_type length => let α := elem_type.bitType
                              vExpr α (.List length)
  | s => s.asType (bitVec s.bitLength)

-- Split a vector at an exact index, resulting in two vectors of known length.
-- This is accomplished by requiring that the input vector's length is already
-- of the form (k + n) where k is the index of the desired split point.
structure SplitVector (α : Type) (k : Nat) (n : Nat) where
  head : Vector α k
  tail : Vector α n

def Vector.splitExact (v : Vector α (k + n)) (k' : Nat) (_ : k = k')
  : SplitVector α k n :=
  -- Ensure that the 'head' of the split is length exactly k.
  let head := (v.take k).cast (by apply Nat.min_add_right_self)
  -- Ensuring that the 'tail' of the split is length exactly n requires this
  -- intermediate simplification, for legibility.
  let h : min (k + n) (k + n) - k = n := by simp +arith
  let tail := h ▸ v.extract k (k + n)
  SplitVector.mk head tail


-- no idea why simp +arith doesn't just discharge this immediately...
theorem mul_step : (Nat.succ m) * n = n + (m * n) := by
  rw [Nat.mul_comm, Nat.mul_add_one, Nat.add_comm, Nat.mul_comm]


def Vector.segment (v : Vector α (k * s)) (s' : Nat) (_ : s = s'):
  Vector (Vector α s) k :=
  match k with
  | .zero => #v[]
  | .succ k' =>
        -- The idea here is that a vector of length (k'.succ * s) can be
        -- rearranged into (abusing notation) #v[s] + #v[k' * s]; the former is
        -- one of our segments, while the latter is easily itself segmented.
        --
        -- First, we rearrange the length index in order to apply splitExact.
        let hk : (.succ k') * s = s + (k' * s) := by apply mul_step
        let split := ((v.cast hk).splitExact s (by rfl): SplitVector α s (k' * s))
        let this_segment := Vector.singleton split.head
        -- Now, the 'tail' index is conveniently expressed for immediate
        -- recursion of segment.
        let rest_segments := split.tail.segment s (by rfl)
        -- Finally, we need to flip the length around in the index, since
        -- `this.append rest` will have length 1 + k, but we need it to have
        -- length k.succ, or k + 1.
        let h : (1 + k') = (k'.succ) := by rw[Nat.add_comm, Nat.add_one]
        h ▸ (this_segment.append rest_segments)


def segment (s : sExpr) (b : bitVec s.bitLength) : s.bitType :=
  match s with
  | .Int => .Int b
  | .Bool => .Bool b
  | .List elem_type length =>
           let length_segmented : (elem_type.List length).bitLength = length * elem_type.bitLength := by
             rw[Nat.mul_comm]
           let b_length_segmented := b.cast length_segmented
           let segmented := b_length_segmented.segment elem_type.bitLength (by rfl)
           let decoded := segmented.map (segment elem_type)
           .List decoded

[neil]

here's basically everything involved for now, I'm going to see if I can define a separate, similar function on sExprs which still results in this error

[neil]

the "problem" is that I'm using indexed families sort of heavily, so it's difficult to just pull out a small piece

[neil]

ok actually I'm not going to try to define something smaller, because producing a valid s.bitType basically requires this much code, since you have to satisfy all the length requirements for the various Vectors

[neil]

(for context, I'm writing a type-directed de-/serialization framework, where users provide "signatures" [here the minimal type sExpr] which direct parsing bytestrings into host-language values [here the type vExpr, which is generic to support partial-parsing and other sorts of operations, and which is indexed because I want to experiment with relying on dependent types to make this as correct-by-construction as possible].

I'm using dependent typing to ensure that bytestrings conform to the given signature, and to couple the resulting value expressions to that signature as well. Hence sExpr.bitLength, for the former, and sExpr.bitType / sExpr.asType \a, for the latter.)
)

[Aaron Liu]

something is wrong if a working function starts printing errors after turning on compiler tracing

[neil]

wait, sorry, I don't think that's what's happening in my case--the interactive lean output just puts a red quiggly on my definition of segment with the error message I posted.

I haven't tried to "use" segment, so it's not that it "was working" but isn't when the compiler is given different commands

[neil]

what I meant by the topic title was that, based on its definition but independently of any actual feedback from lean, I would have expected segment to be computable as defined

[neil]

if you do try to do something like #eval (segment .Bool #v[true]), which should just be vExpr.Bool #v[true], you instead get (interpreter) unknown declaration '_eval', but maybe that's expected given that segment has failed to compile.

Also, neither segment nor Vector.segment can be marked partial

[Aaron Liu]

I have no idea what's going on, but this is what I have so far

import Lean.Meta.Basic
import Mathlib.Util.WhatsNew
inductive TagExpr where | Int | Bool | List (n : Nat)

inductive vExpr (α : Type u) : TagExpr → Type u where
  | Int : α → vExpr α .Int
  | Bool : α → vExpr α .Bool
  | List : Vector α n → vExpr α (.List n)


inductive sExpr where
  | Int
  | Bool
  | List (elem_type : sExpr) (length : Nat)

abbrev sExpr.asType (s : sExpr) (α : Type) :=
  match s with
  | Int => vExpr α .Int
  | Bool => vExpr α .Bool
  | List elem_type length => vExpr (elem_type.asType α) (.List length)

abbrev bitVec : Nat → Type
  | n => Vector Bool n

-- `sorry`ing this one fixes it so maybe something with `abbrev` being `@[reducible, inline]`?
abbrev sExpr.bitLength : sExpr → Nat
  | .Int => 8
  | .Bool => 1
  | .List elem_type length => elem_type.bitLength * length

abbrev sExpr.bitType (s : sExpr) : Type :=
  match s with
  -- NOTE: for some reason, we have to explicitly unroll .asType, otherwise we
  -- get type errors.
  | .List elem_type length => let α := elem_type.bitType
                              vExpr α (.List length)
  | s => s.asType (bitVec s.bitLength)

def Vector.segment (v : Vector α (k * s)) (s' : Nat) (_ : s = s'):
  Vector (Vector α s) k :=
  sorry

-- whatsnew in
-- set_option trace.compiler true in
def segment (s : sExpr) (b : bitVec s.bitLength) : s.bitType :=
  match s with
  | .Int => .Int b
  | .Bool => .Bool b
  | .List elem_type length =>
           let length_segmented : (elem_type.List length).bitLength = length * elem_type.bitLength := by
             rw[Nat.mul_comm]
           let b_length_segmented := b.cast length_segmented
           let segmented := b_length_segmented.segment elem_type.bitLength (by rfl)
           let decoded := segmented.map (segment elem_type)
           .List decoded
run_meta do
  let env ← Lean.getEnv
  let n := `segment._cstage2
  let u? ← (do
    for k in env.constants do
      if k.fst = n then return some k.snd
    return none)
  let some u := u? | failure
  Lean.logInfo <| repr <| u.value!

[neil]

do you have no idea what's going on in a way that I can help by commenting on the mwe, or do you mean that you have no idea what's going on in a way that requires understanding the compiler

[Aaron Liu]

I have no idea what's wrong with the compiler but look I got some cool trace messages

[neil]

lmao

[Aaron Liu]

Maybe I'll study the compiler this week

[Aaron Liu]

Actually since they're replacing it soon maybe not

[neil]

can you post the traces?

[neil]

maybe I should just actually install mathlib and generate them myself

[Aaron Liu]

You can look at them on the web server

[Aaron Liu]

hover over the code block and click the pop-out on the top right

[neil]

i love Infrastructure

[neil]

wow ok you got it

[Aaron Liu]

It seems to work fine on the new compiler so just update Lean maybe?

[neil]

change the abbrev sExpr.bitLength to @[reducible] def ... and it works

[neil]

yeah, I'll just update Lean.

fwiw when I was looking this up it looked like there were some issues with inlining and this same trace

[neil]

these docs implicitly suggest using the reducible-def : https://docs.lean-lang.org/lean4/doc/examples/interp.lean.html

but the dependently typed programming section of "functional programming in Lean" suggests using abbrev, sooo

[neil]

how did you figure to start mucking with the abbrevs? was it just a case of trying to change anything that looked suspicious / bisecting, or was there some trace output that suggested making that particular change?

[Aaron Liu]

The new compiler is enabled by default as of 3 days ago, so I don't think it's in any versions yet

[Aaron Liu]

neil said:

how did you figure to start mucking with the abbrevs? was it just a case of trying to change anything that looked suspicious / bisecting, or was there some trace output that suggested making that particular change?

I was replacing definitions by sorry in an attempt to make the example more minimal, and then it suddenly started working

[neil]

I don't understand how that works, in that wouldn't replacing definitions by sorry make it /less/ computable, not /more/?

[neil]

oh wow, I just replaced the definition of Vector.segment with sorry and there's nothing at all reported from the definition of segment. So I suppose, if you use sorry in a definition, lean is giving you the benefit of the doubt and marking it computable? I suppose that makes sorry much more useful for prototyping.

[Tomas Skrivan]

I have encountered similar problem https://github.com/leanprover/lean4/issues/7874 it might be worth posting your example there too

[Henrik Böving]

Both the bug described here as well as in the issue seems to be handled by the new compiler, coming soon to a Lean release near you.