termination compiler app error

Stream: lean4

[Mario Carneiro]

I think the error here is somewhere in the termination checker, but I haven't minimized it further than this:

def heapifyDown (lt : α → α → Bool) (a : Array α) (i : Fin a.size) : Array α :=
  let left := 2 * i.1 + 1
  let right := left + 1
  have left_le : i ≤ left := sorry
  have right_le : i ≤ right := sorry
  have i_le : i ≤ i := Nat.le_refl _
  have j : {j : Fin a.size // i ≤ j} := if h : left < a.size then
    if lt (a.get i) (a.get ⟨left, h⟩) then ⟨⟨left, h⟩, left_le⟩ else ⟨i, i_le⟩ else ⟨i, i_le⟩
  have j := if h : right < a.size then
    if lt (a.get j) (a.get ⟨right, h⟩) then ⟨⟨right, h⟩, right_le⟩ else j else j
  if h : i ≠ j then
    let a' := a.swap i j
    have : a'.size - j < a.size - i := sorry
    heapifyDown lt a' ⟨j.1.1, a.size_swap i j ▸ j.1.2⟩
  else
    a
termination_by measure fun ⟨_, _, a, i⟩ => a.size - i.1
decreasing_by assumption

gives an error on the def heapifyDown saying:

application type mismatch
  LE.le snd✝
argument has type
  Fin (Array.size fst✝)
but function has type
  Fin x✝ → Fin x✝ → Prop

[Leonardo de Moura]

@Mario Carneiro Thanks for reporting the issue. I will be very grateful if you manage to minimize the example.

[Mario Carneiro]

smaller version

def heapifyDown (a : Array α) (i : Fin a.size) : Array α :=
  have : i < i := sorry
  heapifyDown a ⟨i.1, a.size_swap i i ▸ i.2⟩
termination_by measure fun ⟨_, a, i⟩ => i.1
decreasing_by assumption

[Leonardo de Moura]

Thanks! :)

[Mario Carneiro]

removing the a.size_swap i i ▸ makes the error go away. I think the version of the goal in the assumption context is ill typed

[Mario Carneiro]

Replacing assumption with done and setting pp.all reveals the context:

unsolved goals
fst✝¹ : Type u_1
fst✝ : Array.{u_1} fst✝¹
snd✝ : Fin (@Array.size.{u_1} fst✝¹ fst✝)
this : @LT.lt.{0} (Fin (@Array.size.{u_1} fst✝¹ fst✝)) (@instLTFin (@Array.size.{u_1} fst✝¹ fst✝)) snd✝ snd✝
⊢ (@measure.{u_1 + 2}
        (@PSigma.{u_1 + 2, u_1 + 1} (Type u_1)
          fun {α : Type u_1} =>
            @PSigma.{u_1 + 1, 1} (Array.{u_1} α) fun (a : Array.{u_1} α) => Fin (@Array.size.{u_1} α a))
        fun
          (x :
          @PSigma.{u_1 + 2, u_1 + 1} (Type u_1)
            fun {α : Type u_1} =>
              @PSigma.{u_1 + 1, 1} (Array.{u_1} α) fun (a : Array.{u_1} α) => Fin (@Array.size.{u_1} α a)) =>
          heapifyDown._unary.match_1.{u_1, 1}
            (fun
              (x :
              @PSigma.{u_1 + 2, u_1 + 1} (Type u_1)
                fun {α : Type u_1} =>
                  @PSigma.{u_1 + 1, 1} (Array.{u_1} α) fun (a : Array.{u_1} α) => Fin (@Array.size.{u_1} α a)) =>
              Nat)
            x
            fun (x : Type u_1) (a : Array.{u_1} x) (i : Fin (@Array.size.{u_1} x a)) =>
              @Fin.val (@Array.size.{u_1} x a) i).1
    (@PSigma.mk.{u_1 + 2, u_1 + 1} (Type u_1)
      (fun {α : Type u_1} =>
        @PSigma.{u_1 + 1, 1} (Array.{u_1} α) fun (a : Array.{u_1} α) => Fin (@Array.size.{u_1} α a))
      fst✝¹
      (@PSigma.mk.{u_1 + 1, 1} (Array.{u_1} fst✝¹) (fun (a : Array.{u_1} fst✝¹) => Fin (@Array.size.{u_1} fst✝¹ a)) fst✝
        (@Fin.mk (@Array.size.{u_1} fst✝¹ fst✝) (@Fin.val (@Array.size.{u_1} fst✝¹ fst✝) snd✝)
          (@Eq.ndrec.{0, 1} Nat (@Array.size.{u_1} fst✝¹ (@Array.swap.{u_1} fst✝¹ fst✝ snd✝ snd✝))
            (fun (x : Nat) => @LT.lt.{0} Nat instLTNat (@Fin.val x snd✝) x)
            (@Eq.ndrec.{0, 1} Nat (@Array.size.{u_1} fst✝¹ fst✝)
              (fun (x : Nat) => @LT.lt.{0} Nat instLTNat (@Fin.val x snd✝) x)
              (@Fin.isLt (@Array.size.{u_1} fst✝¹ fst✝) snd✝)
              (@Array.size.{u_1} fst✝¹ (@Array.swap.{u_1} fst✝¹ fst✝ snd✝ snd✝))
              (@Eq.symm.{1} Nat (@Array.size.{u_1} fst✝¹ (@Array.swap.{u_1} fst✝¹ fst✝ snd✝ snd✝))
                (@Array.size.{u_1} fst✝¹ fst✝) (@Array.size_swap.{u_1} fst✝¹ fst✝ snd✝ snd✝)))
            (@Array.size.{u_1} fst✝¹ fst✝) (@Array.size_swap.{u_1} fst✝¹ fst✝ snd✝ snd✝)))))
    (@PSigma.mk.{u_1 + 2, u_1 + 1} (Type u_1)
      (fun {α : Type u_1} =>
        @PSigma.{u_1 + 1, 1} (Array.{u_1} α) fun (a : Array.{u_1} α) => Fin (@Array.size.{u_1} α a))
      fst✝¹
      (@PSigma.mk.{u_1 + 1, 1} (Array.{u_1} fst✝¹) (fun (a : Array.{u_1} fst✝¹) => Fin (@Array.size.{u_1} fst✝¹ a)) fst✝
        snd✝))

which contains a subterm fun (x : Nat) => @LT.lt.{0} Nat instLTNat (@Fin.val x snd✝) x which is ill typed because snd✝ : Fin (@Array.size.{u_1} fst✝¹ fst✝) instead of Fin x. This looks like the kind of replacement that rw will sometimes do that yields the motive is not type correct error in lean 3

[Mario Carneiro]

Oh, the termination compiler is a red herring. This has the same error:

def heapifyDown' (a : Array α) (i : Fin a.size) : Array α := sorry
def heapifyDown (a : Array α) (i : Fin a.size) : Array α :=
  heapifyDown' a ⟨i.1, a.size_swap i i ▸ i.2⟩

[Mario Carneiro]

minimized more:

example (a : Array α) (i : Fin a.size) : i.1 < a.size := a.size_swap i i ▸ i.2

[Mario Carneiro]

minimized more:

variable (a : Nat) (i : Fin a) (h : 1 = a)

#check (h ▸ i.2 : i < a) -- h ▸ Eq.symm h ▸ i.isLt : i.val < a

example : i < a := h ▸ i.2
-- application type mismatch
--   i.val
-- argument has type
--   Fin a
-- but function has type
--   Fin x✝ → Nat

The check result is very weird (and there are in fact two Eq.ndrec nodes being generated), but I don't think it is the issue. It seems like this actually is a motive is not type correct error, but it passes elaboration and gets caught late

[Leonardo de Moura]

I pushed a fix for this. The ▸ notation now type checks the generated motives like the rw tactic.