Merge branch 'experimental/upstream' into upstream

1 files changed, 22 insertions, 0 deletions

diff --git a/test-suite/success/universes-coercion.v b/test-suite/success/universes-coercion.v
new file mode 100644
index 00000000..d7504340
--- /dev/null
+++ b/test-suite/success/universes-coercion.v
@@ -0,0 +1,22 @@
+(* This example used to emphasize the absence of LEGO-style universe
+   polymorphism; Matthieu's improvements of typing on 2011/3/11 now
+   makes (apparently) that Amokrane's automatic eta-expansion in the
+   coercion mechanism works; this makes its illustration as a "weakness"
+   of universe polymorphism obsolete (example submitted by Randy Pollack).
+
+   Note that this example is not an evidence that the current
+   non-kernel eta-expansion behavior is the most expected one.  
+*)
+
+Parameter K : forall T : Type, T -> T.
+Check (K (forall T : Type, T -> T) K).
+
+(*
+   note that the inferred term is
+     "(K (forall T (* u1 *) : Type, T -> T) (fun T:Type (* u1 *) => K T))"
+   which is not eta-equivalent to 
+     "(K (forall T : Type, T -> T) K"
+   because the eta-expansion of the latter
+     "(K (forall T : Type, T -> T) (fun T:Type (* u2 *) => K T)"
+  assuming K of type "forall T (* u2 *) : Type, T -> T"
+*)