Note: Type compatibility checking for LCNF

We used to have a type compatibility relation ≃ for LCNF types. It treated erased types/values as wildcards. Examples:

• List Nat ≃ List ◾
• (List ◾ → List ◾) ≃ (List Nat → List Bool)

We used this relation to sanity check compiler passes, and detect buggy transformations that broke type compatibility. For example, given an application f a, we would check whether as type as compatible with the type expected by f.

However, the type compatibility relation is not transitive. Example:

• List Nat ≃ List ◾, List ◾ ≃ List String, but List Nat and List String are not compatible.

We tried address the issue above by adding casts, which required us to then add cast elimination simplifications, and generated a significant overhead in the code generator.

Here is an example of transformation that would require the insertion of a cast operation.

def foo (g : List A → List A) (a : List B) :=
  fun f (x : List ◾) :=
    let _x.1 := g x
    ...
  let _x.2 := f a
  ...

The code above would not trigger any type compatibility issue, but by inlining f without adding cast operations, we would get the following type incorrect code.

def foo (g : List A → List A) (a : List B) :=
let _x.2 := g a -- Type error
...

We have considered using a reflexive and transitive subtype relation ≺.

• A ≺ A
• (Nat × Nat) ≺ (Nat × ◾) ≺ (◾ × ◾) ≺ ◾
• List Nat ≺ List ◾ ⊀ List String
• (List ◾ → List Nat) ≺ (List Bool → List ◾) Note that A ≺ B implies A ≃ B

The subtype relation has better properties, but also has problems. First, when converting to LCNF we would have to add more casts. Example: the function takes a List ◾, but the value has type ◾. Moreover, recall that (List Nat → List Nat) ⊀ (◾ → ◾) forcing us to add many casts operations when moving to the mono phase where we erase type parameters.

Recall that type compatibility and subtype relationships do not help with memory layout. We have that (UInt32 × UInt32) ≺ (◾ × ◾) ≺ ◾ but elements of these types have different runtime representation.

Thus, we have decided to abandon the type compatibility checks and cast operations in LCNF. The only drawback is that we lose the capability of catching simple bugs at compiler passes.

In the future, we can try to add a sanity check flag that instructs the compiler to use the subtype relation in sanity checks and add the necessary casts.

structure Lean.Compiler.LCNF.Check.Context : Type

• jps : Lean.FVarIdSet

  Join points that are in scope.

• vars : Lean.FVarIdSet

  Variables and local functions in scope

structure Lean.Compiler.LCNF.Check.State : Type

• all : Lean.FVarIdHashSet

  All free variables found

@[reducible, inline]

abbrev Lean.Compiler.LCNF.Check.CheckM (α : Type) : Type

def Lean.Compiler.LCNF.Check.checkTypes : Lean.Compiler.LCNF.Check.CheckM Bool

def Lean.Compiler.LCNF.Check.checkFVar (fvarId : Lean.FVarId) : Lean.Compiler.LCNF.Check.CheckM Unit

def Lean.Compiler.LCNF.Check.isCtorParam (f : Lean.Expr) (i : Nat) : Lean.CoreM Bool

Return true f is a constructor and i is less than its number of parameters.

Equations

• One or more equations did not get rendered due to their size.
• Lean.Compiler.LCNF.Check.isCtorParam f i = pure false

def Lean.Compiler.LCNF.Check.checkAppArgs (f : Lean.Expr) (args : Array Lean.Compiler.LCNF.Arg) : Lean.Compiler.LCNF.Check.CheckM Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Compiler.LCNF.Check.checkLetValue (e : Lean.Compiler.LCNF.LetValue) : Lean.Compiler.LCNF.Check.CheckM Unit

Equations

• One or more equations did not get rendered due to their size.
• Lean.Compiler.LCNF.Check.checkLetValue (Lean.Compiler.LCNF.LetValue.value value) = pure ()
• Lean.Compiler.LCNF.Check.checkLetValue Lean.Compiler.LCNF.LetValue.erased = pure ()
• Lean.Compiler.LCNF.Check.checkLetValue (Lean.Compiler.LCNF.LetValue.const declName us args) = Lean.Compiler.LCNF.Check.checkAppArgs (Lean.mkConst declName us) args
• Lean.Compiler.LCNF.Check.checkLetValue (Lean.Compiler.LCNF.LetValue.proj typeName idx fvarId) = Lean.Compiler.LCNF.Check.checkFVar fvarId

def Lean.Compiler.LCNF.Check.checkJpInScope (jp : Lean.FVarId) : Lean.Compiler.LCNF.Check.CheckM Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Compiler.LCNF.Check.checkParam (param : Lean.Compiler.LCNF.Param) : Lean.Compiler.LCNF.Check.CheckM Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Compiler.LCNF.Check.checkParams (params : Array Lean.Compiler.LCNF.Param) : Lean.Compiler.LCNF.Check.CheckM Unit

Equations

• Lean.Compiler.LCNF.Check.checkParams params = Array.forM Lean.Compiler.LCNF.Check.checkParam params

def Lean.Compiler.LCNF.Check.checkLetDecl (letDecl : Lean.Compiler.LCNF.LetDecl) : Lean.Compiler.LCNF.Check.CheckM Unit

def Lean.Compiler.LCNF.Check.addFVarId (fvarId : Lean.FVarId) : Lean.Compiler.LCNF.Check.CheckM Unit

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Lean.Compiler.LCNF.Check.withFVarId {α : Type} (fvarId : Lean.FVarId) (x : Lean.Compiler.LCNF.Check.CheckM α) : Lean.Compiler.LCNF.Check.CheckM α

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Lean.Compiler.LCNF.Check.withJp {α : Type} (fvarId : Lean.FVarId) (x : Lean.Compiler.LCNF.Check.CheckM α) : Lean.Compiler.LCNF.Check.CheckM α

@[inline]

def Lean.Compiler.LCNF.Check.withParams {α : Type} (params : Array Lean.Compiler.LCNF.Param) (x : Lean.Compiler.LCNF.Check.CheckM α) : Lean.Compiler.LCNF.Check.CheckM α

Equations

• One or more equations did not get rendered due to their size.

partial def Lean.Compiler.LCNF.Check.checkFunDeclCore (declName : Lean.Name) (params : Array Lean.Compiler.LCNF.Param) (type : Lean.Expr) (value : Lean.Compiler.LCNF.Code) : Lean.Compiler.LCNF.Check.CheckM Unit

partial def Lean.Compiler.LCNF.Check.checkFunDecl (funDecl : Lean.Compiler.LCNF.FunDecl) : Lean.Compiler.LCNF.Check.CheckM Unit

partial def Lean.Compiler.LCNF.Check.checkCases (c : Lean.Compiler.LCNF.Cases) : Lean.Compiler.LCNF.Check.CheckM Unit

partial def Lean.Compiler.LCNF.Check.check (code : Lean.Compiler.LCNF.Code) : Lean.Compiler.LCNF.Check.CheckM Unit

def Lean.Compiler.LCNF.Check.run {α : Type} (x : Lean.Compiler.LCNF.Check.CheckM α) : Lean.Compiler.LCNF.CompilerM α

Equations

• One or more equations did not get rendered due to their size.

def Lean.Compiler.LCNF.Decl.check (decl : Lean.Compiler.LCNF.Decl) : Lean.Compiler.LCNF.CompilerM Unit

def Lean.Compiler.LCNF.checkDeadLocalDecls (decls : Array Lean.Compiler.LCNF.Decl) : Lean.Compiler.LCNF.CompilerM Unit

Check whether every local declaration in the local context is used in one of given decls.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Compiler.LCNF.checkDeadLocalDecls.visitFVar (fvarId : Lean.FVarId) : StateM Lean.FVarIdHashSet Unit

def Lean.Compiler.LCNF.checkDeadLocalDecls.visitParam (param : Lean.Compiler.LCNF.Param) : StateM Lean.FVarIdHashSet Unit

Equations

• Lean.Compiler.LCNF.checkDeadLocalDecls.visitParam param = Lean.Compiler.LCNF.checkDeadLocalDecls.visitFVar param.fvarId

def Lean.Compiler.LCNF.checkDeadLocalDecls.visitParams (params : Array Lean.Compiler.LCNF.Param) : StateM Lean.FVarIdHashSet Unit

Equations

• Lean.Compiler.LCNF.checkDeadLocalDecls.visitParams params = Array.forM Lean.Compiler.LCNF.checkDeadLocalDecls.visitParam params

partial def Lean.Compiler.LCNF.checkDeadLocalDecls.visitCode (code : Lean.Compiler.LCNF.Code) : StateM Lean.FVarIdHashSet Unit

def Lean.Compiler.LCNF.checkDeadLocalDecls.visitDecl (decl : Lean.Compiler.LCNF.Decl) : StateM Lean.FVarIdHashSet Unit

Equations

• Lean.Compiler.LCNF.checkDeadLocalDecls.visitDecl decl = do Lean.Compiler.LCNF.checkDeadLocalDecls.visitParams decl.params Lean.Compiler.LCNF.checkDeadLocalDecls.visitCode decl.value

def Lean.Compiler.LCNF.checkDeadLocalDecls.visitDecls (decls : Array Lean.Compiler.LCNF.Decl) : StateM Lean.FVarIdHashSet Unit