aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/HoTT_coq_084.v
blob: d007e4e235d8919d9ab464f2b12da6291cded7ba (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
45
46
47
48
49
Set Implicit Arguments.
Set Universe Polymorphism.

Module success.
  Unset Primitive Projections.

  Record group :=
    { carrier : Type;
      id : carrier }.

  Notation "1" := (id _) : g_scope.

  Delimit Scope g_scope with g.
  Bind Scope g_scope with carrier.

  Section foo.
    Variable g : group.
    Variable comp : carrier g -> carrier g -> carrier g.

    Check comp 1 1.
  End foo.
End success.

Module failure.
  Set Primitive Projections.

  Record group :=
    { carrier : Type;
      id : carrier }.

  Notation "1" := (id _) : g_scope.

  Delimit Scope g_scope with g.
  Bind Scope g_scope with carrier.

  Section foo.
    Variable g : group.
    Variable comp : carrier g -> carrier g -> carrier g.

    Check comp 1 1.
    (* Toplevel input, characters 11-12:
Error:
In environment
g : group
comp : carrier g -> carrier g -> carrier g
The term "1" has type "nat" while it is expected to have type "carrier g".
    *)
  End foo.
End failure.