hoqtop produces ill-typed goal

[ezyang]

The following proof script fails due to Coq having generated an ill-typed term when considering the goal.

Inductive Empty : Type :=.

Inductive paths {A : Type} (a : A) : A -> Type :=
  idpath : paths a a.

Notation "x = y :> A" := (@paths A x y) : type_scope.
Notation "x = y" := (x = y :>_) : type_scope.

Arguments idpath {A a} , [A] a.

Definition idmap {A : Type} : A -> A := fun x => x.

Definition path_sum {A B : Type} (z z' : A + B)
           (pq : match z, z' with
                   | inl z0, inl z'0 => z0 = z'0
                   | inr z0, inr z'0 => z0 = z'0
                   | _, _ => Empty
                 end)
: z = z'.
  destruct z, z', pq; exact idpath.
Defined.

Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
  := match p with idpath => idpath end.

Theorem ex2_8 {A B A' B' : Type} (g : A -> A') (h : B -> B') (x y : A + B)
              (* Fortunately, this unifies properly *)
              (pq : match (x, y) with (inl x', inl y') => x' = y' | (inr x', inr y') => x' = y' | _ => Empty end) :
  let f z := match z with inl z' => inl (g z') | inr z' => inr (h z') end in
  ap f (path_sum x y pq) = path_sum (f x) (f y)
     ((match x as x return match (x, y) with
              (inl x', inl y') => x' = y'
            | (inr x', inr y') => x' = y'
            | _ => Empty
          end -> match (f x, f y) with
               | (inl x', inl y') => x' = y'
               | (inr x', inr y') => x' = y'
               | _ => Empty end with
           | inl x' => match y with
                         | inl y' => ap g
                         | inr y' => idmap
                       end
           | inr x' => match y with
                         | inl y' => idmap
                         | inr y' => ap h
                       end
       end) pq).
Admitted. (* This line fails *)

The error is:

Toplevel input, characters 20-29:
Error: Matching on term "f y" of type "A' + B'" expects 2 branches.

The contents of Show Proof is:

(fun (A B A' B' : Type) (g : A -> A') (h : B -> B') 
   (x y : A + B)
   (pq : let (s, s0) := (x, y) in
         match s with
         | inl x' => match s0 with
                     | inl y' => x' = y'
                     | inr _ => Empty
                     end
         | inr x' => match s0 with
                     | inl _ => Empty
                     | inr y' => x' = y'
                     end
         end) => ?147)

The error can be made to go away by fully annotating the match expressions, as is seen in Issue #54.

The error does not occur if coqtop is invoked directly, even with indices-matter, which suggests the modified coqlib is to fault.

Here is the generated term which typechecks in coqtop but not in hoqtop:

Definition x := forall (A B A' B' : Type) (g : A -> A') (h : B -> B') 
  (x y : A + B)
  (pq : let (s, s0) := (x, y) in
        match s with
        | inl x' => match s0 with
                    | inl y' => x' = y'
                    | inr _ => Empty
                    end
        | inr x' => match s0 with
                    | inl _ => Empty
                    | inr y' => x' = y'
                    end
        end),
let f :=
  fun z : A + B =>
  match z with
  | inl z' => inl (g z')
  | inr z' => inr (h z')
  end in
ap f (path_sum x y pq) =
path_sum (f x) (f y)
  (match
     x as x0
     return
       (match x0 with
        | inl x' => match y with
                    | inl y' => x' = y'
                    | inr _ => Empty
                    end
        | inr x' => match y with
                    | inl _ => Empty
                    | inr y' => x' = y'
                    end
        end ->
        match f x0 with
        | inl x' => match f y with
                    | inl y' => x' = y'
                    | inr _ => Empty
                    end
        | inr x' => match f y with
                    | inl _ => Empty
                    | inr y' => x' = y'
                    end
        end)
   with
   | inl x' =>
       match
         y as y0
         return
           (match y0 with
            | inl y' => x' = y'
            | inr _ => Empty
            end ->
            match f (inl x') with
            | inl x'0 =>
                match f y0 with
                | inl y' => x'0 = y'
                | inr _ => Empty
                end
            | inr x'0 =>
                match f y0 with
                | inl _ => Empty
                | inr y' => x'0 = y'
                end
            end)
       with
       | inl y' => ap g
       | inr _ => idmap
       end
   | inr x' =>
       match
         y as y0
         return
           (match y0 with
            | inl _ => Empty
            | inr y' => x' = y'
            end ->
            match f (inr x') with
            | inl x'0 =>
                match f y0 with
                | inl y' => x'0 = y'
                | inr _ => Empty
                end
            | inr x'0 =>
                match f y0 with
                | inl _ => Empty
                | inr y' => x'0 = y'
                end
            end)
       with
       | inl _ => idmap
       | inr y' => ap h
       end
   end pq).

[JasonGross]

Here is some code that reproduces the error in HoTT/coq, with coqc -indices-matter -nois:

(* File reduced by coq-bug-finder from 526 lines to 84 lines. *)
Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
Reserved Notation "x = y  :>  T"
         (at level 70, y at next level, no associativity).
Reserved Notation "x = y" (at level 70, no associativity).
Reserved Notation "x + y" (at level 50, left associativity).

Delimit Scope core_scope with core.
Open Scope core_scope.
Open Scope type_scope.
Global Set Universe Polymorphism.

Notation "A -> B" := (forall (_ : A), B) : type_scope.

Set Implicit Arguments.

Inductive sum (A B : Type) : Type :=
| inl : A -> sum A B
| inr : B -> sum A B.

Notation "x + y" := (sum x y) : type_scope.

Arguments inl {A B} _ , [A] B _.
Arguments inr {A B} _ , A [B] _.

Inductive prod (A B : Type) : Type :=
  pair : A -> B -> prod A B.

Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
Inductive Empty : Prop := .

Inductive paths {A : Type} (a : A) : A -> Type :=
  idpath : paths a a.

Notation "x = y :> A" := (@paths A x y) : type_scope.

Notation "x = y" := (x = y :>_) : type_scope.
Arguments idpath {A a} , [A] a.

Definition idmap {A : Type} : A -> A := fun x => x.

Definition path_sum {A B : Type} (z z' : A + B)
           (pq : match z, z' with
                   | inl z0, inl z'0 => z0 = z'0
                   | inr z0, inr z'0 => z0 = z'0
                   | _, _ => Empty
                 end)
: z = z'.

  admit.
Defined.
Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
  := match p with idpath => idpath end.

Theorem ex2_8 {A B A' B' : Type} (g : A -> A') (h : B -> B') (x y : A + B)

        (pq : match (x, y) with (inl x', inl y') => x' = y' | (inr x', inr y') => x' = y' | _ => Empty end) :
  let f z := match z with inl z' => inl (g z') | inr z' => inr (h z') end in
  ap f (path_sum x y pq) = path_sum (f x) (f y)
                                    ((match x as x return match (x, y) with
                                                              (inl x', inl y') => x' = y'
                                                            | (inr x', inr y') => x' = y'
                                                            | _ => Empty
                                                          end -> match (f x, f y) with
                                                                   | (inl x', inl y') => x' = y'
                                                                   | (inr x', inr y') => x' = y'
                                                                   | _ => Empty end with
                                        | inl x' => match y with
                                                      | inl y' => ap g
                                                      | inr y' => idmap
                                                    end
                                        | inr x' => match y with
                                                      | inl y' => idmap
                                                      | inr y' => ap h
                                                    end
                                      end) pq).

Admitted.

[JasonGross]

However, it is fixed in trunk-polyproj (but not in HoTT/coq trunk), so I think we (@ezyang or @mattam82) should close this issue.

[JasonGross]

Actually, getting it is easier than that; @ezyang, if you add Set Universe Polymorphism to the top of your example, it produces the error under HoTT/coq (the relevant difference between HoTT's stdlib and Coq's is that HoTT's runs a Global Set Universe Polymorphism.).