aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/HoTT_coq_089.v
blob: 2da4aff6a11185ada79cc3cbb08112981e3baff9 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
Set Implicit Arguments. 
Set Universe Polymorphism.
Set Printing Universes.

Inductive type_paths (A : Type) : Type -> Prop
  := idtypepath : type_paths A A.
Monomorphic Definition comp_type_paths := Eval compute in type_paths@{Type Type}.
Check comp_type_paths.
(* comp_type_paths
     : Type (* Top.12 *) -> Type (* Top.12 *) -> Prop *)
(* This is terrible. *)

Inductive type_paths' (A : Type) : Type -> Prop
  := idtypepath' : type_paths' A A
   | other_type_path : False -> forall B : Type, type_paths' A B.
Monomorphic Definition comp_type_paths' := Eval compute in type_paths'.
Check comp_type_paths'.
(* comp_type_paths'
     : Type (* Top.24 *) -> Type (* Top.23 *) -> Prop *)
(* Ok, then ... *)

(** Fail if it's [U0 -> U0 -> _], but not on [U0 -> U1 -> _]. *)
Goal Type.
Proof.
  match type of comp_type_paths' with
    | ?U0 -> ?U1 -> ?R
      => exact (@comp_type_paths' nat U0)
  end.
Defined.

Goal Type.
Proof.
   match type of comp_type_paths with
    | ?U0 -> ?U1 -> ?R
      => exact (@comp_type_paths nat U0)
  end.
  (* Toplevel input, characters 110-112:
Error:
The term "Type (* Top.51 *)" has type "Type (* Top.51+1 *)"
while it is expected to have type "Type (* Top.51 *)"
(Universe inconsistency: Cannot enforce Top.51 < Top.51 because Top.51
= Top.51)). *)
  
Defined.