Lean4 interpreter hanging for map to iterated products

Stream: lean4

[Siddhartha Gadgil]

I am trying to use a type TermSeq for terms of various types, with a conversion to iterated products for convenience in some situations. Strangely this is hanging while building (both in VS Code and leanpkg build). Here is the code causing the crash. I am sharing this for any feedback before creating an issue.

inductive TermSeq where
  | empty : TermSeq
  | cons : {α : Type} → (a : α) → (tail: TermSeq) → TermSeq

namespace TermSeq

def prodType : TermSeq → Type
  | empty => Unit
  | @cons α a tail => Prod α (prodType tail)

def asProd : (ts: TermSeq) → prodType ts
  | empty => (() : Unit)
  | @cons α a tail => (a, asProd tail)

end TermSeq

[Mac]

Siddhartha Gadgil said:

I am trying to use a type TermSeq for terms of various types, with a conversion to iterated products for convenience in some situations. Strangely this is hanging while building (both in VS Code and leanpkg build).

Yep, the example hangs for me as well. Surprisingly, this variant (with an extra alternate for the special case of a singleton), on the other hand, does not:

inductive HList.{u} : Type (u + 1)
| unit : HList
| cons : {α : Type u} → (a : α) → (xs : HList) → HList

namespace HList

def tupleType : HList.{u} → Type u
| unit => PUnit
| @cons α a unit => α
| @cons α a (cons b xs) => Prod α (tupleType (cons b xs))

def toTuple : (t : HList) → t.tupleType
| unit => ()
| cons a unit => a
| cons a (cons b xs) => (a, toTuple (cons b xs))

#reduce cons true (cons 0 unit) |>.toTuple -- (true, 0)
#reduce cons true (cons 0 unit) |>.tupleType -- Bool × Nat

[Leonardo de Moura]

@Siddhartha Gadgil I pushed a fix for the TermSeq repro. Thanks for reporting the issue.

[Siddhartha Gadgil]

Thanks a lot