diff options
| author | herbelin | 2013-05-08 17:44:20 +0000 |
|---|---|---|
| committer | herbelin | 2013-05-08 17:44:20 +0000 |
| commit | c9467e5684f9a71cb82ddc72b5b9d501b32b5c5e (patch) | |
| tree | a69b27a71cb8a846e2b0d48f960ed13d603b2446 /pretyping | |
| parent | 8916db4378cf5ceb477a425bdf8f6bdd5fd58716 (diff) | |
Protection against "Bad recursive type" in w_unify0 (bug #3036).
Morally, unification wants to unify "fun x:Meta => Meta"
with "fun x:nat => match x with ... end". Retyping is asked to
type "match x with ... end" in the context "x:Meta" where the
type of x has de facto been lost. Retyping fails.
I don't see an easy remedy since w_unify0 builds the unifier
lazily, and I'm not sure it is worth to propagate the unifier to
retyping so that it knows it. After all, the call to retyping in
w_unify0 is not so critical.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16489 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/unification.ml | 18 |
1 files changed, 12 insertions, 6 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index f3014424c4..219c1ec227 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -382,9 +382,12 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag | Meta k, _ when not (dependent cM cN) (* helps early trying alternatives *) -> if wt && flags.check_applied_meta_types then - (let tyM = Typing.meta_type sigma k in - let tyN = get_type_of curenv sigma cN in - check_compatibility curenv substn tyM tyN); + (try + let tyM = Typing.meta_type sigma k in + let tyN = get_type_of curenv ~lax:true sigma cN in + check_compatibility curenv substn tyM tyN + with RetypeError _ -> + (* Renounce, maybe metas/evars prevents typing *) ()); (* Here we check that [cN] does not contain any local variables *) if Int.equal nb 0 then sigma,(k,cN,snd (extract_instance_status pb))::metasubst,evarsubst @@ -396,9 +399,12 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag | _, Meta k when not (dependent cN cM) (* helps early trying alternatives *) -> if wt && flags.check_applied_meta_types then - (let tyM = get_type_of curenv sigma cM in - let tyN = Typing.meta_type sigma k in - check_compatibility curenv substn tyM tyN); + (try + let tyM = get_type_of curenv sigma cM in + let tyN = Typing.meta_type sigma k in + check_compatibility curenv substn tyM tyN + with RetypeError _ -> + (* Renounce, maybe metas/evars prevents typing *) ()); (* Here we check that [cM] does not contain any local variables *) if Int.equal nb 0 then (sigma,(k,cM,fst (extract_instance_status pb))::metasubst,evarsubst) |