Definition of `NDBType.asType` in exercise 7.3.6.2. Nullable Types

Thanks a lot for the great book. It was a great pleasure to work through it.

In exercise 7.3.6.2., NDBType.asType is defined as follows:

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

An alternative definition is:

abbrev NDBType.asType : NDBType → Type
| ⟨t, false⟩ => t.asType
| ⟨t, true⟩  => Option t.asType

With the alternative definition, match expressions are able to infer more than with the original definition. I'm using the current most recent stable Lean (4.25.2). Three examples that work with the alternative definition, but not with the original one:

#check (42 : (NDBType.mk .int false).asType)

def NDBType.beq : (t : NDBType) → t.asType → t.asType → Bool
| ⟨.int, false⟩
| ⟨.int, true⟩
| ⟨.bool, false⟩
| ⟨.bool, true⟩
| ⟨.string, false⟩
| ⟨.string, true⟩  => BEq.beq

instance (t : NDBType) : BEq t.asType :=
  match t with | ⟨_, false⟩ | ⟨_, true⟩ => inferInstance

It is possible to define NDBType.beq in ways that do work with the original definition. For example:

def NDBType.beq (t : NDBType) : t.asType → t.asType → Bool :=
  match t with
  | ⟨_, true⟩ => fun
    | some x, some y  => x == y
    | _, _ => false
  | ⟨t, false⟩ => t.beq

But there are considerably less such ways.

I found the exercise more demanding than most of the exercises in the book. Unless the additional difficulty introduced by the way NDBType.asType is defined is intended, I suggest to change the definition.

Start by locating the source for exercise 7.3.6.2, Nullable Types, and read the definition of NDBType.asType in that exercise. Check the reported examples with Lean 4.25.2, then update the exercise if appropriate so the definition supports the intended pattern inference and the examples work as described.