controlling elaboration order of tactics in terms

Stream: lean4

[Rob Lewis]

A student of mine has run into the following problem: using tactics to construct data, the order of elaboration can cause type checking to fail prematurely. His MWE is below. If you'll accept for the moment that using tactics to construct data is actually a reasonable thing to do in our application, is there anything we can do to tweak the elaboration order that might make this work?

inductive Dict : List (String × Type) → Type 1
  | nil : Dict []
  | cons {α hs nm} : α → Dict hs → Dict ((nm, α) :: hs)

-- This is Type-valued predicate
inductive List.MemT {α : Type _} : α → List α → Type _
  | hd {x xs} : List.MemT x (x :: xs)
  | tl {x xs y} : List.MemT x xs → List.MemT x (y :: xs)

def List.removeMem {α : Type _} {x} : (xs : List α) → List.MemT x xs → List α
  | _ :: xs, .hd => xs
  | x :: xs, .tl h => x :: removeMem xs h

def Dict.dropEntry {τ : Type} {hs : List (String × Type)} (nm : String) :
  Dict hs → (h : List.MemT (nm, τ) hs) → Dict (hs.removeMem h)
  | .cons x xs, .hd => xs
  | .cons x xs, .tl h' => .cons x (dropEntry nm xs h')

macro "mem" : tactic =>
  `(tactic| repeat (first | apply List.MemT.hd | apply List.MemT.tl))

def d1 : Dict [("a", Nat), ("b", Bool)] := .cons 4 (.cons true .nil)
def d2 : Dict [("a", Nat), ("b", Nat)] := .cons 3 (.cons 1 .nil)

-- These terms elaborate correctly...
#check d1.dropEntry "b" (by mem) -- Dict (List.removeMem [("a", Nat), ("b", Bool)] (List.MemT.tl List.MemT.hd))
#check d2.dropEntry "b" (by mem) -- Dict (List.removeMem [("a", Nat), ("b", Nat)] (List.MemT.tl List.MemT.hd))

-- And their types are definitionally equal
example : Dict (List.removeMem [("a", Nat), ("b", Bool)] (List.MemT.tl List.MemT.hd)) =
  Dict (List.removeMem [("a", Nat), ("b", Nat)] (List.MemT.tl List.MemT.hd)) :=
rfl

-- Type-correctness of this equality depends on the proof produced by `mem`
def p : Prop := d1.dropEntry "b" (by mem) = d2.dropEntry "b" (by mem) -- fails
def p' : Prop := d1.dropEntry "b" (.tl .hd) = d2.dropEntry "b" (.tl .hd) -- succeeds

[Mario Carneiro]

(d1.dropEntry "b" (by mem) :) = (d2.dropEntry "b" (by mem) :) works

[Rob Lewis]

My eye can only see a :smile: and mismatched parens -- I guess this is a type annotation without providing the type, that's different from : _ somehow?

[Mario Carneiro]

it's like : _ from lean 3

[Mario Carneiro]

in lean 4 : _ does nothing

[Mario Carneiro]

(e :) is basically the same as have := e; this where the have := is a separate tactic block

[Mario Carneiro]

that is, it elaborates e as much as possible, then asserts that the resulting type is equal to the expected type

[Mario Carneiro]

rather than using the expected type to influence elaboration

[Rob Lewis]

So, exactly what we want here. That's perfect, and I only thought to try : _. Thanks!