(Bug?) LEAN4 unresolvable termination error

Stream: general

[Aniket Mishra (Sati)]

The error is in the Basic.lean file at https://github.com/satiscugcat/assertion-insecurity-lean/tree/error-showcase (the file currently takes a non insignificant while to typecheck, so it may take some time for the errors to pop up).

The error comes from LEAN trying to prove termination for the "recursor" functions, but apparently in trying to do so it encounters a type application mismatch. I do not understand how. Adding "decreasing_by (all_goals sorry)" results in a weirder kernel error that looks like this. I cannot understand what is going on.
image.png

[Aaron Liu]

that's not good

[Aaron Liu]

you linked to a 3000 line file, so it will be difficult to go through all that

[Aaron Liu]

it'd be a lot easier if you had a #mwe

[Aniket Mishra (Sati)]

Aaron Liu said:

you linked to a 3000 line file, so it will be difficult to go through all that

Right, sorry for that. Branch has been updated to serve as a minimum working example (now about 300 lines)

[Robin Arnez]

Just to clarify; I get the same kind of error for all "recursors". If you're talking about that error, here's a reproducer:

inductive EX {A : Type} (P : A → Type) : Type
  | intro (w : A) (h : P w)

inductive EQ {A : Type} : A → A → Type
  | refl (r : A) : EQ r r

inductive Term : Type
  | pair (t1 t2 : Term)
deriving DecidableEq

def Set (α : Type u) := α → Prop

@[instance]
axiom instSingletonSet : Singleton α (Set α)

@[instance]
axiom instUnionSet : Union (Set α)

@[instance]
axiom instEmptyCollectionSet : EmptyCollection (Set α)

abbrev TermSet := Set Term

inductive dy : TermSet → Term → Type
  | something {x y} : dy x y

inductive Assertion : Type
  | eq (t u : Term)
  | member (t₀ : Term) (tlist : List Term)
deriving DecidableEq

abbrev AssertionSet := Set Assertion

axiom intersection {A : Type} [DecidableEq A] : List A → List A → List A

mutual
inductive eq_ady : TermSet → AssertionSet → Assertion → Type
  | cons_pair {S : TermSet} {A : AssertionSet} {t1 t2 u1 u2 : Term} (p1 : eq_ady S A (Assertion.eq t1 u1)) (p2 : eq_ady S A (Assertion.eq t2 u2)) : eq_ady S A (Assertion.eq (Term.pair t1 t2) (Term.pair u1 u2))
  | irrelevant {S A B} : eq_ady S A B
inductive Eq_Trans : TermSet → AssertionSet → Term → Term → Type
  | two_trans {S : TermSet} {A : AssertionSet} {t1 t2 t3 : Term} (p1 : eq_ady S A (Assertion.eq t1 t2)) (p2 : eq_ady S A (Assertion.eq t2 t3)) : Eq_Trans S A t1 t3
  | trans_trans {S : TermSet} {A : AssertionSet} {t1 tk tk' : Term} (phead : eq_ady S A (Assertion.eq t1 tk)) (plist : Eq_Trans S A tk tk') : Eq_Trans S A t1 tk'
inductive Eq_Int : TermSet → AssertionSet → Term → List Term → Type
  | two_lists {S : TermSet} {A : AssertionSet} {t : Term} {l1 l2 : List Term}  (proof1 : eq_ady S A (Assertion.member t l1)) (proof2 : eq_ady S A (Assertion.member t l2)) : Eq_Int S A t (intersection l1 l2)
  | new_list {S : TermSet} {A : AssertionSet} {t : Term} {l l' : List Term} (proof1 : eq_ady S A (Assertion.member t l)) (proof2 : Eq_Int S A t l') : Eq_Int S A t (intersection l l')
inductive Eq_Wk : TermSet → List Term → Type
  | single {S : TermSet} {t : Term} (proof : dy S t) : Eq_Wk S [t]
  | new {S : TermSet} {t : Term} {tlist : List Term} (proofNew : dy S t) (proofList : Eq_Wk S tlist) : Eq_Wk S (t :: tlist)
end

def pairLeftRecursor {S A t u} : Eq_Trans S A t u →
        Option (
          (EX fun t1  => EX fun x1 => EX fun x2 =>
              eq_ady S A (Assertion.eq t1 x1) × (eq_ady S A (Assertion.eq (x1.pair x2) u)) × (EX fun t2 => EQ t (t1.pair t2)))
        ) := by
  intros p
  cases p with
  | @two_trans _ _ x _ p1 p2 => apply Option.none
  | trans_trans phead plist =>
    match phead with
    | @eq_ady.cons_pair _ _ t1 t2 x1 x2 a b => apply Option.none
    | phead =>
      match (pairLeftRecursor plist) with
      | Option.none => apply Option.none
      | Option.some p => apply Option.none

[Robin Arnez]

The error in question being:

fail to show termination for
  pkRecursor
with errors
failed to infer structural recursion:
Not considering parameter S of pkRecursor:
  it is unchanged in the recursive calls
Not considering parameter A of pkRecursor:
  it is unchanged in the recursive calls
Not considering parameter u of pkRecursor:
  it is unchanged in the recursive calls
Cannot use parameter p:
  failed to eliminate recursive application
    pkRecursor ptail
Cannot use parameter u:
  failed to eliminate recursive application
    pkRecursor ptail


Application type mismatch: The argument
  Eq_Trans.trans_trans phead✝² plist
has type
  Eq_Trans S A t1 tk'
but is expected to have type
  Eq_Trans S A✝ t1 u
in the application
  sizeOf (Eq_Trans.trans_trans phead✝² plist)

[Aniket Mishra (Sati)]

@Robin Arnez thanks for the better minimal example, would you have any idea on why it's happening?