diff options
| author | Pierre-Marie Pédrot | 2020-03-31 12:56:34 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-03-31 12:56:34 +0200 |
| commit | d03529ab8fec0cad5705b5f775e43ef26c0dedcb (patch) | |
| tree | 65bd33deead3007350bbd93a662ff88017024a99 | |
| parent | 35b4841eccc645146b62e99edb939fcf4bfcc76d (diff) | |
| parent | 60ec0e0a67e60c52af7e7ef34a2826ef7fb61a26 (diff) | |
Merge PR #11684: Remove spurious anomalies in kernel reduction
Reviewed-by: ppedrot
| -rw-r--r-- | kernel/reduction.ml | 6 | ||||
| -rw-r--r-- | test-suite/success/ConversionOrder.v | 16 |
2 files changed, 20 insertions, 2 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 469d5ccaa2..7574d7b21e 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -354,7 +354,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (match kind a1, kind a2 with | (Sort s1, Sort s2) -> if not (is_empty_stack v1 && is_empty_stack v2) then - anomaly (Pp.str "conversion was given ill-typed terms (Sort)."); + (* May happen because we convert application right to left *) + raise NotConvertible; sort_cmp_universes (info_env infos.cnv_inf) cv_pb s1 s2 cuniv | (Meta n, Meta m) -> if Int.equal n m @@ -471,7 +472,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | (FProd (x1, c1, c2, e), FProd (_, c'1, c'2, e')) -> if not (is_empty_stack v1 && is_empty_stack v2) then - anomaly (Pp.str "conversion was given ill-typed terms (FProd)."); + (* May happen because we convert application right to left *) + raise NotConvertible; (* Luo's system *) let el1 = el_stack lft1 v1 in let el2 = el_stack lft2 v2 in diff --git a/test-suite/success/ConversionOrder.v b/test-suite/success/ConversionOrder.v new file mode 100644 index 0000000000..1e0b4dbf23 --- /dev/null +++ b/test-suite/success/ConversionOrder.v @@ -0,0 +1,16 @@ +(* The kernel may convert application arguments right to left, + resulting in ill-typed terms, but should be robust to them. *) + +Inductive Hide := hide : forall A, A -> Hide. + +Lemma foo : (hide Type Type) = (hide (nat -> Type) (fun x : nat => Type)). +Proof. + Fail reflexivity. + match goal with |- ?l = _ => exact_no_check (eq_refl l) end. + Fail Defined. +Abort. + +Definition HideMore (_:Hide) := 0. + +Definition foo : HideMore (hide Type Type) = HideMore (hide (nat -> Type) (fun x : nat => Type)) + := eq_refl. |