From 79c8a3879b461a46e5c8bfc42df00b1fcf109514 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 21 Sep 2022 19:14:25 -0700 Subject: [PATCH] fix: LCNF `compatibleTypes` function --- src/Lean/Compiler/LCNF/Types.lean | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) diff --git a/src/Lean/Compiler/LCNF/Types.lean b/src/Lean/Compiler/LCNF/Types.lean index bbffc8db15..11f926d59a 100644 --- a/src/Lean/Compiler/LCNF/Types.lean +++ b/src/Lean/Compiler/LCNF/Types.lean @@ -207,6 +207,22 @@ in fact exhaustive due to LCNF constraints: partial def compatibleTypes (a b : Expr) : Bool := if a.isAnyType || b.isAnyType then true + else if a.isErased || b.isErased then + /- + This is an approximation. This can happen when processing universe polymorphic code. + After instantiating universes, we may have propositions. For example, suppose we have + ``` + def f (α : Sort u) (x : α → α → Sort v) (a b : α) (h : x a b) ... + ``` + The LCNF type for this universe polymorphic declaration is + ``` + def f (α : Sort u) (x : α → α → Sort v) (a b : α) (h : x ◾ ◾) ... + ``` + Now, if we instantiate with `v = 0`, we have that `x ◾ ◾` is also a proposition + and should be equivalent to `◾`. However, to perform this check we need the environment + and local context. We may consider doing at `Check.lean` + -/ + true else let a' := a.headBeta let b' := b.headBeta @@ -236,7 +252,8 @@ partial def joinTypes? (a b : Expr) : Option Expr := do if a.isAnyType then return a else if b.isAnyType then return b else if a == b then return a - else if a.isErased || b.isErased then failure + else if a.isErased || b.isErased then + return erasedExpr -- See comment at `compatibleTypes`. else let a' := a.headBeta let b' := b.headBeta