Zulip Chat Archive

Stream: lean4

Topic: Bug in sizeOf generation


Parth Shastri (Dec 02 2022 at 05:56):

The following inductive type yields a strange error.

inductive Bug
  | mk : (Unit  Nat  Bug)  Bug
error: application type mismatch
  a_ih () ()
argument has type
  Unit
but function has type
  Nat  Nat

Using set_option genSizeOf false suppresses the error, suggesting it occurs in the code that generates the sizeOf definition.
I believe the bug lies in this function which determines if the field is to be skipped:

private partial def ignoreField (x : Expr) : MetaM Bool := do
  let type  whnf ( inferType x)
  if type.isForall then
    -- TODO: add support for finite domains
    if type.isArrow && type.bindingDomain!.isConstOf ``Unit then
      ignoreField type.bindingBody!
    else
      return true
  else
    return false

Notice that the recursive call is made directly on the body of the forall type, rather than an expression of that type. Then, the inferType will yield an incorrect result.
A possible fix is to replace the function with the following

private partial def ignoreField (x : Expr) : MetaM Bool := do
  helper ( inferType x)
where
  helper type := do
    let type  whnf type
    if type.isForall then
      -- TODO: add support for finite domains
      if type.isArrow && type.bindingDomain!.isConstOf ``Unit then
        helper type.bindingBody!
      else
        return true
    else
      return false

Last updated: Dec 20 2023 at 11:08 UTC