HepLean Documentation

Lean.Compiler.LCNF.CompatibleTypes

Compatible Types #

We used to type check LCNF after each compiler pass. However, we disable this capability because cast management was too costly. The casts may be needed to ensure the result of each pass is still typeable. However, these sanity checks are useful for catching silly mistakes. Thus, we have added an "LCNF type linter". When turned on, this "linter" option instructs the compiler to perform compatibility type checking in the LCNF code after some compiler passes. Recall most casts are only needed in functions that make heavy use of dependent types. We claim it is "defensible" to say this sanity checker is a linter. If the sanity checker fails, it means the user is "abusing" dependent types and performance may suffer at runtime. Here is an example of code that "abuses" dependent types:

def Tuple (α : Type u) : Nat → Type u
  | 0   => PUnit
  | 1   => α
  | n+2 => α × Tuple α (n+1)

def mkConstTuple (a : α) : (n : Nat) → Tuple α n
  | 0 => ⟨⟩
  | 1 => a
  | n+2 => (a, mkConstTuple a (n+1))

def Tuple.map (f : α → β) (xs : Tuple α n) : Tuple β n :=
  match n with
  | 0 => ⟨⟩
  | 1 => f xs
  | _+2 => match xs with
    | (a, xs) => (f a, Tuple.map f xs)
source
partial def Lean.Compiler.LCNF.compatibleTypesQuick (a b : Lean.Expr) :
Bool

Quick check for compatibleTypes. It is not monadic, but it is incomplete because it does not eta-expand type formers. See comment at compatibleTypes. Remark: if the result is true, then a and b are indeed compatible. If it is false, we must use the full-check.

source
partial def Lean.Compiler.LCNF.InferType.compatibleTypesFull (a b : Lean.Expr) :
Lean.Compiler.LCNF.InferType.InferTypeM Bool

Complete check for compatibleTypes. It eta-expands type formers. See comment at compatibleTypes.

source
def Lean.Compiler.LCNF.InferType.compatibleTypesFull.etaExpand? (e : Lean.Expr) :
Lean.Compiler.LCNF.InferType.InferTypeM (Option Lean.Expr)
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Lean.Compiler.LCNF.InferType.compatibleTypes (a b : Lean.Expr) :
    Lean.Compiler.LCNF.InferType.InferTypeM Bool

    Return true if the LCNF types a and b are compatible. Remark: a and b can be type formers (e.g., List, or fun (α : Type) => Nat → Nat × α) Remark: We may need to eta-expand type formers to establish whether they are compatible or not. For example, suppose we have

    fun (x : B) => Id B ◾ ◾
Id B ◾

    We must eta-expand Id B ◾ to fun (x : B) => Id B ◾ x. Note that, we use x instead of ◾ to make the implementation simpler and skip the check whether B is a type former type. However, this simplification should not affect correctness since ◾ is compatible with everything. Remark: see comment at isErasedCompatible. Remark: because of "erasure confusion" see note above, we assume ◾ (aka lcErasure) is compatible with everything. This is a simplification. We used to use isErasedCompatible, but this only address item 1. For item 2, we would have to modify the toLCNFType function and make sure a type former is erased if the expected type is not always a type former (see S.mk type and example in the note above).

    Equations
    Instances For