Documentation

Lean.Compiler.LCNF.Check

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:

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:

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 .

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 NatList 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.

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

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

        Equations
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[inline]
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[inline]
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        @[inline]
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For

                            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