comparison src/Universes.v @ 388:057a29f9c773

Baffling unification messages explained
author Adam Chlipala <adam@chlipala.net>
date Thu, 12 Apr 2012 16:27:28 -0400
parents 6413675f8e04
children 4b1242b277b2
comparison
equal deleted inserted replaced
387:7ece04e15446 388:057a29f9c773
347 bar 347 bar
348 : Prop 348 : Prop
349 ]] 349 ]]
350 350
351 The type that Coq comes up with may be used in strictly more contexts than the type one might have expected. *) 351 The type that Coq comes up with may be used in strictly more contexts than the type one might have expected. *)
352
353
354 (** ** Deciphering Baffling Messages About Inability to Unify *)
355
356 (** One of the most confusing sorts of Coq error messages arises from an interplay between universes, syntax notations, and %\index{implicit arguments}%implicit arguments. Consider the following innocuous lemma, which is symmetry of equality for the special case of types. *)
357
358 Theorem symmetry : forall A B : Type,
359 A = B
360 -> B = A.
361 intros ? ? H; rewrite H; reflexivity.
362 Qed.
363
364 (** Let us attempt an admittedly silly proof of the following theorem. *)
365
366 Theorem illustrative_but_silly_detour : unit = unit.
367 (** [[
368 apply symmetry.
369 ]]
370 <<
371 Error: Impossible to unify "?35 = ?34" with "unit = unit".
372 >>
373
374 Coq tells us that we cannot, in fact, apply our lemma [symmetry] here, but the error message seems defective. In particular, one might think that [apply] should unify [?35] and [?34] with [unit] to ensure that the unification goes through. In fact, the problem is in a part of the unification problem that is %\emph{%#<i>#not#</i>#%}% shown to us in this error message!
375
376 The following command is the secret to getting better error messages in such cases: *)
377
378 Set Printing All.
379 (** [[
380 apply symmetry.
381 ]]
382 <<
383 Error: Impossible to unify "@eq Type ?46 ?45" with "@eq Set unit unit".
384 >>
385
386 Now we can see the problem: it is the first, %\emph{%#<i>#implicit#</i>#%}% argument to the underlying equality function [eq] that disagrees across the two terms. The universe [Set] may be both an element and a subtype of [Type], but the two are not definitionally equal. *)
387
388 Abort.
389
390 (** A variety of changes to the theorem statement would lead to use of [Type] as the implicit argument of [eq]. Here is one such change. *)
391
392 Theorem illustrative_but_silly_detour : (unit : Type) = unit.
393 apply symmetry; reflexivity.
394 Qed.
395
396 (** There are many related issues that can come up with error messages, where one or both of notations and implicit arguments hide important details. The [Set Printing All] command turns off all such features and exposes underlying CIC terms.
397
398 For completeness, we mention one other class of confusing error message about inability to unify two terms that look obviously unifiable. Each unification variable has a scope; a unification variable instantiation may not mention variables that were not already defined within that scope, at the point in proof search where the unification variable was introduced. Consider this illustrative example: *)
399
400 Unset Printing All.
401
402 Theorem ex_symmetry : (exists x, x = 0) -> (exists x, 0 = x).
403 econstructor.
404 (** %\vspace{-.15in}%[[
405 H : exists x : nat, x = 0
406 ============================
407 0 = ?98
408 ]]
409 *)
410
411 destruct H.
412 (** %\vspace{-.15in}%[[
413 x : nat
414 H : x = 0
415 ============================
416 0 = ?99
417 ]]
418 *)
419
420 (** [[
421 symmetry; exact H.
422 ]]
423
424 <<
425 Error: In environment
426 x : nat
427 H : x = 0
428 The term "H" has type "x = 0" while it is expected to have type
429 "?99 = 0".
430 >>
431
432 The problem here is that variable [x] was introduced by [destruct] %\emph{%#<i>#after#</i>#%}% we introduced [?99] with [eexists], so the instantiation of [?99] may not mention [x]. A simple reordering of the proof solves the problem. *)
433
434 Restart.
435 destruct 1 as [x]; apply ex_intro with x; symmetry; assumption.
436 Qed.
437
438 (** This restriction for unification variables may seem counterintuitive, but it follows from the fact that CIC contains no concept of unification variable. Rather, to construct the final proof term, at the point in a proof where the unification variable is introduced, we replace it with the instantiation we eventually find for it. It is simply syntactically illegal to refer there to variables that are not in scope. *)
352 439
353 440
354 (** * The [Prop] Universe *) 441 (** * The [Prop] Universe *)
355 442
356 (** In Chapter 4, we saw parallel versions of useful datatypes for %``%#"#programs#"#%''% and %``%#"#proofs.#"#%''% The convention was that programs live in [Set], and proofs live in [Prop]. We gave little explanation for why it is useful to maintain this distinction. There is certainly documentation value from separating programs from proofs; in practice, different concerns apply to building the two types of objects. It turns out, however, that these concerns motivate formal differences between the two universes in Coq. 443 (** In Chapter 4, we saw parallel versions of useful datatypes for %``%#"#programs#"#%''% and %``%#"#proofs.#"#%''% The convention was that programs live in [Set], and proofs live in [Prop]. We gave little explanation for why it is useful to maintain this distinction. There is certainly documentation value from separating programs from proofs; in practice, different concerns apply to building the two types of objects. It turns out, however, that these concerns motivate formal differences between the two universes in Coq.