Inconvenient definition for NDBType.asType

[michens]

The following is given in the Typed Queries exercise

Nullable Types
Add support for nullable columns to the query language by representing database types with the following structure:

 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

Use this type in place of DBType in Column and DBExpr, and look up SQL's rules for NULL and comparison operators to determine the types of DBExpr's constructors.

It seems like Lean has issues seeing through this definition of .asType, which led to needing to use convoluted casting and tactics for the rest of the implementation.

For example, you can try to write NDBType.beq as:

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

However, Lean gives the errors:

failed to synthesize instance
  BEq (asType { underlying := underlying✝, nullable := true })

failed to synthesize instance
  BEq (asType { underlying := underlying✝, nullable := false })

Instead, I needed to write it as:

def NDBType.beq (t : NDBType) (x y : t.asType) : Bool :=
  match t with
  | ⟨t', true⟩ =>
    let x' : Option t'.asType := x
    x' == y
  | ⟨t', false⟩ =>
    let x' : t'.asType := x
    x' == y

On the other hand, you can define NDBType.asType with:

abbrev NDBType.asType (t : NDBType) : Type :=
  match t with
  | ⟨t', true⟩ => Option t'.asType
  | ⟨t', false⟩ => t'.asType

At this point, the first declaration of NDBType.beq works, as do the natural modifications needed for the rest of the exercise.