bug ?

Stream: new members

[Nicolas Rolland]

This code works but it crashes the whole Lean Server when typechecking the second function printHKO

x in inferred to be a String so I would expect to be able to replace it with "Hi".

Is it a bug or am I doing something wrong ?

iimport Mathlib.Data.Vector

inductive HVect : (n : Nat) -> (Vector (Type v) n) -> Type (v+1)  where
   | Nil  : HVect 0 ⟨ [], simp ⟩
   | Cons : (t : Type v) -> (x : t) -> HVect n ⟨ts, p⟩ -> HVect (n+1) ⟨t::ts, by simp [p]⟩


def printHOK (v : HVect (n+1) ⟨String::ts, p'⟩) : String :=
   match v with
   | HVect.Cons _ x _ => (x : String)


def printHKO (v : HVect (n+1) ⟨String::ts, p'⟩) : String :=
   match v with
   | HVect.Cons _ x _ => "Hi"

[Mario Carneiro]

no, server crashes are almost always bugs

[Notification Bot]

Nicolas Rolland has marked this topic as resolved.

[Notification Bot]

Nicolas Rolland has marked this topic as unresolved.

[Mario Carneiro]

this seems like a rather severe issue, it is a SIGSEGV which normally shouldn't happen even if there was a bug in the elaborator

[Nicolas Rolland]

I was using 4.3 rc1, testing on other version. I will open a case on github if I can reproduce on head lean+mathlib

[Mario Carneiro]

it reproduces on 4.3.0-rc2 released today

[Mario Carneiro]

it seems that the compiler had difficulty determining the arity of a constant so it threw an error, but it messed up the error payload and it crashes while trying to print the error

[Nicolas Rolland]

opened issue on github