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)
Quick check for
compatibleTypes. It is not monadic, but it is incomplete
because it does not eta-expand type formers. See comment at
Remark: if the result is
b are indeed compatible.
If it is
false, we must use the full-check.
Complete check for
compatibleTypes. It eta-expands type formers. See comment at
- One or more equations did not get rendered due to their size.
Return true if the LCNF types
b are compatible.
b can be type formers (e.g.,
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
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
Remark: because of "erasure confusion" see note above, we assume
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).