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

[whxvd]

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.