blob: d750434027e405d78e12b7d37b5f2d14fca9fb2b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
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"
*)
|
