# 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 `a`s 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.

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

- jps : FVarIdSet

  Join points that are in scope.

- vars : FVarIdSet

  Variables and local functions in scope

Instances For

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

- all : FVarIdHashSet

  All free variables found

Instances For

source
@[reducible, inline]
abbrev Lean.Compiler.LCNF.Check.CheckM (α : Type) :
Type
Equations

- Lean.Compiler.LCNF.Check.CheckM = ReaderT Lean.Compiler.LCNF.Check.Context (StateRefT' IO.RealWorld Lean.Compiler.LCNF.Check.State Lean.Compiler.LCNF.InferType.InferTypeM)

Instances For

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

- Lean.Compiler.LCNF.Check.checkTypes = do let __do_lift ← liftM Lean.Compiler.LCNF.getConfig pure __do_lift.checkTypes

Instances For

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

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

Instances For

source
def Lean.Compiler.LCNF.Check.isCtorParam (f : Expr) (i : Nat) :
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

Instances For

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

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

Instances For

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

- One or more equations did not get rendered due to their size.
- Lean.Compiler.LCNF.Check.checkLetValue (Lean.Compiler.LCNF.LetValue.lit 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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

source
@[inline]
def Lean.Compiler.LCNF.Check.withFVarId {α : Type} (fvarId : FVarId) (x : CheckM α) :
CheckM α
Equations

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

Instances For

source
@[inline]
def Lean.Compiler.LCNF.Check.withJp {α : Type} (fvarId : FVarId) (x : CheckM α) :
CheckM α
Equations

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

Instances For

source
@[inline]
def Lean.Compiler.LCNF.Check.withParams {α : Type} (params : Array Param) (x : CheckM α) :
CheckM α
Equations

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

Instances For

source
partial def Lean.Compiler.LCNF.Check.checkFunDeclCore (declName : Name) (params : Array Param) (type : Expr) (value : Code) :
CheckM Unit
source
partial def Lean.Compiler.LCNF.Check.checkFunDecl (funDecl : FunDecl) :
CheckM Unit
source
partial def Lean.Compiler.LCNF.Check.checkCases (c : Cases) :
CheckM Unit
source
partial def Lean.Compiler.LCNF.Check.check (code : Code) :
CheckM Unit
source
def Lean.Compiler.LCNF.Check.run {α : Type} (x : CheckM α) :
CompilerM α
Equations

- Lean.Compiler.LCNF.Check.run x = ReaderT.run ((ReaderT.run x { }).run' { }) { }

Instances For

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

- decl.check = Lean.Compiler.LCNF.Check.run (Lean.Compiler.LCNF.DeclValue.forCodeM (Lean.Compiler.LCNF.Check.checkFunDeclCore decl.name decl.params decl.type) decl.value)

Instances For

source
def Lean.Compiler.LCNF.checkDeadLocalDecls (decls : Array Decl) :
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.

Instances For