fix: use a def-eq aware mapping at toLinearExpr

The new test exposes the problem fixed by this commit.
In the termination proof we have two `sizeOf xs` terms that are not
syntactically identical (only definitional equal) because the
instances are different.

src/Lean/Meta/KExprMap.lean

@@ -0,0 +1,45 @@
+/-
+Copyright (c) 2022 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Leonardo de Moura
+-/
+import Lean.HeadIndex
+import Lean.Meta.Basic
+
+namespace Lean.Meta
+
+/--
+  A mapping that indentifies definitionally equal expressions.
+  We implement it as a mapping from `HeadIndex` to `Std.AssocList Expr α`.
+
+  Remark: this map may be quite inefficient if there are many `HeadIndex` collisions.
+-/
+structure KExprMap (α : Type) where
+  map : Std.PHashMap HeadIndex (Std.AssocList Expr α) := {}
+  deriving Inhabited
+
+def KExprMap.find? (m : KExprMap α) (e : Expr) : MetaM (Option α) := do
+  match m.map.find? e.toHeadIndex with
+  | none => return none
+  | some ps =>
+    for ⟨e', a⟩ in ps do
+      if (← isDefEq e e') then
+        return some a
+    return none
+
+private def updateList (ps : Std.AssocList Expr α) (e : Expr) (v : α) : MetaM (Std.AssocList Expr α) := do
+  match ps with
+  | Std.AssocList.nil => return Std.AssocList.nil
+  | Std.AssocList.cons e' v' ps =>
+    if (← isDefEq e e') then
+      return Std.AssocList.cons e v ps
+    else
+      return Std.AssocList.cons e' v' (← updateList ps e v)
+
+def KExprMap.insert (m : KExprMap α) (e : Expr) (v : α) : MetaM (KExprMap α) :=
+  let k := e.toHeadIndex
+  match m.map.find? k with
+  | none    => return { map := m.map.insert k (Std.AssocList.cons e v Std.AssocList.nil) }
+  | some ps => return { map := m.map.insert k (← updateList ps e v) }
+
+end Lean.Meta

src/Lean/Meta/Tactic/LinearArith/Nat.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 import Lean.Meta.Check
 import Lean.Meta.Offset
+import Lean.Meta.KExprMap
 
 namespace Lean.Meta.Linear.Nat
 
@@ -52,7 +53,7 @@ def LinearCnstr.toArith (ctx : Array Expr) (c : LinearCnstr) : MetaM Expr := do
 namespace ToLinear
 
 structure State where
-  varMap : ExprMap Nat := {}
+  varMap : KExprMap Nat := {} -- It should be fine to use `KExprMap` here because the mapping should be small and few HeadIndex collisions.
   vars   : Array Expr := #[]
 
 abbrev M := StateRefT State MetaM
@@ -60,11 +61,12 @@ abbrev M := StateRefT State MetaM
 open Nat.Linear.Expr
 
 def addAsVar (e : Expr) : M LinearExpr := do
-  if let some x := (← get).varMap.find? e then
+  if let some x ← (← get).varMap.find? e then
     return var x
   else
     let x := (← get).vars.size
-    modify fun s => { varMap := s.varMap.insert e x, vars := s.vars.push e }
+    let s ← get
+    set { varMap := (← s.varMap.insert e x), vars := s.vars.push e : State }
     return var x
 
 partial def toLinearExpr (e : Expr) : M LinearExpr := do

tests/lean/run/instanceIssues.lean

@@ -0,0 +1,9 @@
+inductive Vector (α : Type u) : Nat → Type u
+  | nil  : Vector α 0
+  | cons : α → Vector α n → Vector α (n + 1)
+
+def test [Monad m] (xs : Vector α a) : m Unit :=
+  match xs with
+  | Vector.nil => return ()
+  | Vector.cons x xs => test xs
+termination_by test xs => sizeOf xs