Zulip Chat Archive

Stream: lean4

Topic: significance of (kernel) in error messages?


view this post on Zulip Jason Gross (Mar 10 2021 at 15:06):

I'm getting

96:7: (kernel) function expected
  tm✝¹ _x_13

and

110:7: (kernel) compiler failed to infer low level type, unknown declaration 'SetModel.interpTmStep'

Does getting a message from the kernel roughly analogous to getting an anomaly from Coq or an internal error from gcc?

view this post on Zulip Jason Gross (Mar 10 2021 at 15:08):

Here's an unminimized example:

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

structure SyntaxModel where
  Ctx : Type 1
  Ty : Type 1
  Tm : Type 1
  EC : Ctx  Ctx  Type
  ETy : Ty  Ty  Type
  ETm : Tm  Tm  Type
  getCtx : Ty  Ctx
  getTy : Tm  Ty
  interpCStep : CtxSyntaxLayer Ctx Ty EC getCtx  Ctx
  interpTyStep : TySyntaxLayer Ctx Ty EC getCtx  Ty
  interpTmStep : TmSyntaxLayer Ctx Ty Tm EC ETy getCtx getTy interpTyStep  Tm

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) (Tm.mk fty ftm) (Tm.mk (Ty.mk xctx xty) xtm) (PLift.up fTy) (PLift.up xTy)
        => { ty := B
           , tm := fun {γ} =>
                     (by
                       simp at fTy xTy; subst fTy xTy; simp at Actx Bctx; subst Actx Bctx
                       simp [interpTyStep, cast] at *
                       exact (ftm xtm)
                     )
               }

  def Model : SyntaxModel :=
    {
      Ctx := Ctx
    , Ty := Ty
    , Tm := Tm
    , EC := ECtx
    , ETy := ETy
    , ETm := ETm
    , getCtx := Ty.ctx
    , getTy := Tm.ty
    , interpCStep := interpCStep
    , interpTyStep := interpTyStep
    , interpTmStep := interpTmStep
    }
end SetModel

using the latest Lean nightly

view this post on Zulip Jason Gross (Mar 10 2021 at 15:18):

Reported as https://github.com/leanprover/lean4/issues/341

view this post on Zulip Leonardo de Moura (Mar 10 2021 at 15:25):

This is a known bug in the code generator. It is in an old part that is still written in C/C++. We need to infer types in the compiler, and we reused the kernel type checker for this. However, the compiler performs transformations that may produce type incorrect terms. This happens in code that makes heavy use of dependent types (like yours). I will check if there is some "band-aid" to workaround this particular instance of the problem.
The definitive solution will only happen when we replace this part of the compiler with Lean code, and implement a custom inferType method for the compiler.

Does getting a message from the kernel roughly analogous to getting an anomaly from Coq or an internal error from gcc?

Yes, a message with the (kernel) prefix usually indicates there is a bug in the frontend or code generator.


Last updated: May 07 2021 at 12:15 UTC