application type mismatch error reports identical types as not matching

[JasonGross]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Sorry, not yet minimized. I'll try to minimize this soon.

section
  variable (G : Type 1) (T : Type 1) (Tm : Type 1)
           (EG : G → G → Type) (ET : T → T → Type) (ETm : Tm → Tm → Type)
           (getCtx : T → G) (getTy : Tm → T)
  inductive CtxSyntaxLayer where
    | emp : CtxSyntaxLayer
    | snoc : (Γ : G) → (t : T) → EG Γ (getCtx t) → CtxSyntaxLayer
end
section
  variable (G : Type 1) (T : Type 1) (Tm : Type 1)
           (EG : G → G → Type) (ET : T → T → Type) (ETm : Tm → Tm → Type)
           (getCtx : T → G) (getTy : Tm → T)
           (GAlgebra : CtxSyntaxLayer G T EG getCtx → G)

  inductive TySyntaxLayer where
  | top : {Γ : G} → TySyntaxLayer
  | bot : {Γ : G} → TySyntaxLayer
  | nat : {Γ : G} → TySyntaxLayer
  | arrow : {Γ : G} → (A B : T) → EG Γ (getCtx A) → EG Γ (getCtx B) → TySyntaxLayer

  def getCtxStep : TySyntaxLayer G T EG getCtx → G
    | TySyntaxLayer.top (Γ := Γ) .. => Γ
    | TySyntaxLayer.bot (Γ := Γ) .. => Γ
    | TySyntaxLayer.nat (Γ := Γ) .. => Γ
    | TySyntaxLayer.arrow (Γ := Γ) .. => Γ
end
section
  variable (G : Type 1) (T : Type 1) (Tm : Type 1)
           (EG : G → G → Type) (ET : T → T → Type) (ETm : Tm → Tm → Type)
           (EGrfl : ∀ {Γ}, EG Γ Γ)
           (getCtx : T → G) (getTy : Tm → T)
           (GAlgebra : CtxSyntaxLayer G T EG getCtx → G) (TAlgebra : TySyntaxLayer G T EG getCtx → T)

  inductive TmSyntaxLayer where
    | tt : {Γ : G} → TmSyntaxLayer
    | zero : {Γ : G} → TmSyntaxLayer
    | succ : {Γ : G} → TmSyntaxLayer
    | app : {Γ : G} → (A B : T) → (Actx : EG Γ (getCtx A)) → (Bctx : EG Γ (getCtx B))
        → (f x : Tm)
        → ET (getTy f) (TAlgebra (TySyntaxLayer.arrow A B Actx Bctx))
        → ET (getTy x) A
        → TmSyntaxLayer
  -- set options for debugging "(kernel) declaration has metavariables" errors
  --set_option trace.Elab.definition true
  --set_option pp.explicit true
  def getTyStep : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra → T
    | TmSyntaxLayer.tt (Γ:=Γ) .. => TAlgebra (TySyntaxLayer.top (Γ:=Γ))
    | TmSyntaxLayer.zero (Γ:=Γ) .. => TAlgebra (TySyntaxLayer.nat (Γ:=Γ))
    | TmSyntaxLayer.succ (Γ:=Γ) .. => TAlgebra (TySyntaxLayer.arrow (TAlgebra (TySyntaxLayer.nat (Γ:=Γ))) (TAlgebra (TySyntaxLayer.nat (Γ:=Γ))) EGrfl EGrfl)
    | TmSyntaxLayer.app (B:=B) .. => B
end

namespace SetModel
  def Ctx := Type
  structure Ty where
    ctx : Ctx
    ty : ctx → Type
  structure Tm where
    ty : Ty
    tm : ∀ {Γ}, ty.ty Γ
  def ECtx : Ctx → Ctx → Type := (PLift $ · = ·)
  def ETy  : Ty  → Ty  → Type := (PLift $ · = ·)
  def ETm  : Tm  → Tm  → Type := (PLift $ · = ·)

  def interpCStep : CtxSyntaxLayer Ctx Ty ECtx Ty.ctx → Ctx
    | CtxSyntaxLayer.emp => Unit
    | CtxSyntaxLayer.snoc _ T (PLift.up rfl) => Σ γ : _, T.ty γ

  def Ty.inj Γ T := Ty.mk Γ (λ _ => T)
  def Ty.Unit {Γ} := Ty.inj Γ _root_.Unit
  def Ty.Empty {Γ} := Ty.inj Γ _root_.Empty
  def Ty.Nat {Γ} := Ty.inj Γ _root_.Nat

  def Tm.inj Γ {T} (t : T) := Tm.mk (Ty.inj Γ T) t

  def interpTyStep : TySyntaxLayer Ctx Ty ECtx Ty.ctx → Ty
    | TySyntaxLayer.top (Γ:=Γ) => Ty.Unit (Γ:=Γ)
    | TySyntaxLayer.bot (Γ:=Γ) => Ty.Empty (Γ:=Γ)
    | TySyntaxLayer.nat (Γ:=Γ) => Ty.Nat (Γ:=Γ)
    | TySyntaxLayer.arrow (Γ:=Γ) A B (PLift.up Actx) (PLift.up Bctx) => Ty.mk Γ (λ γ => A.ty (cast Actx γ) → B.ty (cast Bctx γ))

  def interpTmStep : TmSyntaxLayer Ctx Ty Tm ECtx ETy Ty.ctx Tm.ty interpTyStep → Tm
    | TmSyntaxLayer.tt (Γ:=Γ) => Tm.inj Γ Unit.unit
    | TmSyntaxLayer.zero (Γ:=Γ) => Tm.inj Γ (0 : Nat)
    | TmSyntaxLayer.succ (Γ:=Γ) => Tm.inj Γ Nat.succ
    | TmSyntaxLayer.app A B (PLift.up Actx) (PLift.up Bctx) f x (PLift.up fTy) (PLift.up xTy)
        => Tm.inj _ (cast (congrFun fTy _) f.tm)
/-
application type mismatch
  cast (congrFun ?m.6297 (?m.6678 x✝¹ x✝ A B Actx Bctx f x fTy xTy))
argument
  congrFun ?m.6297 (?m.6678 x✝¹ x✝ A B Actx Bctx f x fTy xTy)
has type
  @Eq Type (Ty.ty f.ty (?m.6678 x✝¹ x✝ A B Actx Bctx f x fTy xTy))
    (?m.6803 x✝¹ x✝ A B Actx Bctx f x fTy xTy (?m.6678 x✝¹ x✝ A B Actx Bctx f x fTy xTy))
but is expected to have type
  @Eq Type (Ty.ty f.ty (?m.6678 x✝¹ x✝ A B Actx Bctx f x fTy xTy))
    (?m.6803 x✝¹ x✝ A B Actx Bctx f x fTy xTy (?m.6678 x✝¹ x✝ A B Actx Bctx f x fTy xTy))

-/

Expected behavior: an error message that explains what's wrong

Actual behavior: an error message which claims that identical types aren't the same

Versions

$ lean --version
Lean (version 4.0.0-m2, commit 26dda3f63d88, Release)
$ uname -a
Linux JasonGross-X1 4.19.128-microsoft-standard #1 SMP Tue Jun 23 12:58:10 UTC 2020 x86_64 x86_64 x86_64 GNU/Linux
$ lsb_release -a
No LSB modules are available.
Distributor ID: Ubuntu
Description:    Ubuntu 20.04.1 LTS
Release:        20.04
Codename:       focal

running on WSL2 in Windows 10

[JasonGross]

Even more suspiciously, cast (congrFun fTy f.tm) gives me

application type mismatch
  cast (congrFun ?m.6299 (Tm.tm f))
argument
  congrFun ?m.6299 (Tm.tm f)
has type
  ?m.6265 (Tm.tm f) = ?m.6267 (Tm.tm f)
but is expected to have type
  ?m.6682 x✝¹ x✝ A B Actx Bctx f x fTy xTy = ?m.6683 x✝¹ x✝ A B Actx Bctx f x fTy xTy

so it looks like Lean is somehow forgetting about the first argument to congrFun?

[JasonGross]

Not exactly the same issue, but this seems suspicious too:

#check cast (congrFun _ _)
/-
application type mismatch
  cast (congrFun ?m.13 ?m.14)
argument
  congrFun ?m.13 ?m.14
has type
  ?m.9 ?m.14 = ?m.11 ?m.14
but is expected to have type
  ?m.2 = (?m.9 ?m.14 = ?m.11 ?m.14)

-/

[JasonGross]

Small example:

structure Ty where
  ctx : Type
  ty : ctx → Type
structure Tm where
  ty : Ty
  tm : ∀ {Γ}, ty.ty Γ

#check fun (x' : Type)
  (f : Tm)
  (fTy : f.ty = Ty.mk x' (fun _ => Unit))
  (xTy : Unit)
  => Tm.mk _ (cast (congrFun fTy _) _)
/-
12:15: application type mismatch
  cast (congrFun ?m.457 Γ✝)
argument
  congrFun ?m.457 Γ✝
has type
  @Eq Type (?m.618 x' f fTy xTy) (Ty.ty (?m.617 x' f fTy xTy) Γ✝)
but is expected to have type
  @Eq Type (?m.618 x' f fTy xTy) (Ty.ty (?m.617 x' f fTy xTy) Γ✝)

-/

[JasonGross]

This looks like a de Bruijn indexing bug or something?

structure Ty where
  ctx : Type
  ty : ctx → Type
structure Tm where
  ty : Ty
  tm : ∀ {Γ}, ty.ty Γ

def Ty.inj Γ T := Ty.mk Γ (λ _ => T)
def Tm.inj Γ {T} (t : T) := Tm.mk (Ty.inj Γ T) t

#check fun (x' : Type)
  (f : Tm)
  (fTy : f.ty = Ty.mk x' (fun _ => Unit))
  (xTy : Unit)
  => Tm.inj _ (cast (congrFun fTy _) _)
/-
15:16: application type mismatch
  cast (congrFun ?m.513 xTy)
argument
  congrFun ?m.513 xTy
has type
  @Eq Type (?m.565 x' f fTy xTy) (?m.564 x' f fTy xTy)
but is expected to have type
  @Eq Type (?m.565 x' f fTy xTy) (?m.564 x' f fTy xTy)


-/

Why is it picking up xTy when I haven't used that argument anywhere?

[leodemoura]

After the other fixes I pushed today, the types are not identical anymore. For example, for the last example, we now get

error: application type mismatch
  congrFun fTy
argument
  fTy
has type
  f.ty = { ctx := x', ty := fun (x : x') => Unit }
but is expected to have type
  ?m.615 x' f fTy xTy = (?m.614 x' f fTy xTy).ty

It is still a bit cryptic, but at least it suggests the problem is due to higher-order unification.

[JasonGross]

Indeed, this error message is much better. Even better would be to add details about how ?m.614 can't be inferred from just its .ty projection. (Though, if you have judgmental eta for structures, then this unification problem should be uniquely solvable by instantiating ?m.615 with f.ty and instantiating ?m.614 with its constructor applied to new evars, one of which can then be unified. This may leave over a "cannot infer hole" at the end, but this is different from a unification error.)

However, assuming you don't want to enhance unification in this way (or if you want to make a fresh issue for that), and assuming that Lean previously turning congrFun fTy _ into congrFun ?m.513 xTy (which is by far the most worrisome part of this bug, IMO) is expected to be fixed by the recent commits, and isn't indicative of some deeper bug that the commits are now hiding, I'm happy to consider this bug resolved.

[leodemoura]

assuming that Lean previously turning congrFun fTy _ into congrFun ?m.513 xTy (which is by far the most worrisome part of this bug, IMO) is expected to be fixed by the recent commits, and isn't indicative of some deeper bug that the commits are now hiding

I investigated why congrFun fTy _ was previously being displayed as congrFun ?m xTy.
I agree it is weird, but it is not due to another bug.
When Lean 4 is elaborating a term e with expected type T, it tries unify the typeOf(e) with T. If this test fails, it creates a new hole (metavariable) to be filled with a coercion from typeOf(e) to T. This coercion is synthesized later because the types may contain metavariables that are blocking coercion resolution. However, there was a missing case. Before trying to synthesize the coercion, Lean should try to unify typeOf(e) with T again because it may succeed after metavariables in these type have been instantiated. This was the bug fix. Without the bug fix, the hole corresponding to fTy was never being resolved. This is why we have a ?m.513 in the error message. The xTy appears by accident when Lean tries to compute the expected type for the error message, and in the process has to resolve the following higher-order unification problem

?m.472 ?m.513 =?= ?m.562 x' f fTy xTy

and uses the (first-order) approximated solution

?m.472 := ?m.562 x' f fTy
?m.513 := xTy

[leodemoura]

I'm happy to consider this bug resolved.

Me too.