Abbrev does not reduce?

Stream: lean4

[Pim Otte]

I ran into the above while working throug FPIL4

inductive DBType where
 | bool

abbrev DBType.asType : DBType → Type
  | .bool => Bool

structure NDBType where
  underlying : DBType
  nullable : Bool

abbrev NDBType.asType (t : NDBType) : Type :=
  if t.nullable then
    Option t.underlying.asType
  else
    t.underlying.asType

def test1 : ({underlying := .bool, nullable := false} : NDBType).asType := false

def test2 (a : Bool) (b : Bool) : Prop := (a : Bool) ∧ ¬ b

def test3 (a : ({underlying := .bool, nullable := false} : NDBType).asType) (b : Bool) : Prop := (a : Bool) ∧ ¬ b

The above code works until test3, where it yields:

application type mismatch
  And a
argument
  a
has type
  NDBType.asType { underlying := DBType.bool, nullable := false } : Type
but is expected to have type
  Prop : Type

Because the type definitions use abbrev I thought I understood the above type should just reduce to Bool, but I'm probably overlooking something. This only occurs with the double "asType" constructions, just the one layer doesn't cause this problem. Any pointers?

[Arthur Adjedj]

Even though NBDType.asType does reduce here, it reduces to its definition, which makes use of if ... then ... else, which itself is syntactic sugar for the ite function. Since ite is not reducible, the whole thing doesn't reduce to Bool here. Changing your definition to use a match instead of ite fixes the problem here:

inductive DBType where
 | bool

abbrev DBType.asType : DBType → Type
  | .bool => Bool

structure NDBType where
  underlying : DBType
  nullable : Bool

abbrev NDBType.asType (t : NDBType) : Type := match t.nullable with
  | .true =>
    Option t.underlying.asType
  | .false =>
    t.underlying.asType

def test3 (a : ({underlying := .bool, nullable := false} : NDBType).asType) (b : Bool) : Prop := (a : Bool) ∧ ¬ b --works

Maybe it would make sense to mark ite as reducible ? it would make its behaviour more in line with matches.