Anomaly: Invalid argument: enforce_eq_instances called with instances of different lengths. (polyproj)

[JasonGross]

I tried to build a module for agda-style reasoning with universes via lift. When I use hoqtop (i.e., when I replace the standard library), I get errors:

Set Implicit Arguments.

Set Printing Universes.

Set Asymmetric Patterns.

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

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

Arguments paths_ind [A] a P f y p.
Arguments paths_rec [A] a P f y p.
Arguments paths_rect [A] a P f y p.

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

Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y :=
  match p with idpath => u end.

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

Definition Sect {A B : Type} (s : A -> B) (r : B -> A) :=
  forall x : A, r (s x) = x.

(** A typeclass that includes the data making [f] into an adjoint equivalence. *)
Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv {
  equiv_inv : B -> A ;
  eisretr : Sect equiv_inv f;
  eissect : Sect f equiv_inv;
  eisadj : forall x : A, eisretr (f x) = ap f (eissect x)
}.

Arguments eisretr {A B} f {_} _.
Arguments eissect {A B} f {_} _.
Arguments eisadj {A B} f {_} _.

Inductive type_eq (A : Type) : Type -> Type :=
| type_eq_refl : type_eq A A
| type_eq_impossible : False -> forall B : Type, type_eq A B.

Definition type_eq_sym {A B} (p : type_eq A B) : type_eq B A
  := match p in (type_eq _ B) return (type_eq B A) with
       | type_eq_refl => type_eq_refl _
       | type_eq_impossible f B => type_eq_impossible _ f A
     end.

Definition type_eq_sym_type_eq_sym {A B} (p : type_eq A B) : type_eq_sym (type_eq_sym p) = p
  := match p as p return type_eq_sym (type_eq_sym p) = p with
       | type_eq_refl => idpath
       | type_eq_impossible f _ => idpath
     end.

Module Type LiftT.
  Section local.
    Let type_cast_up_type : Type.
    Proof.
      let U0 := constr:(Type) in
      let U1 := constr:(Type) in
      let unif := constr:(U0 : U1) in
      exact (forall T : U0, { T' : U1 & type_eq T' T }).
    Defined.

    Axiom type_cast_up : type_cast_up_type.
  End local.

  Definition Lift (T : Type) := projT1 (type_cast_up T).
  Definition lift {T} : T -> Lift T
    := match projT2 (type_cast_up T) in (type_eq _ T') return T' -> Lift T with
         | type_eq_refl => fun x => x
         | type_eq_impossible bad _ => match bad with end
       end.
  Section equiv.
    Definition lower' {T} : Lift T -> T
      := match projT2 (type_cast_up T) in (type_eq _ T') return Lift T -> T' with
           | type_eq_refl => fun x => x
           | type_eq_impossible bad _ => match bad with end
         end.
    Definition lift_lower {T} (x : Lift T) : lift (lower' x) = x.
    Proof.
      unfold lower', lift.
      destruct (projT2 (type_cast_up T)) as [|[]].
      reflexivity.
    Defined.
    Definition lower_lift {T} (x : T) : lower' (lift x) = x.
    Proof.
      unfold lower', lift, Lift in *.
      destruct (type_cast_up T) as [T' p]; simpl.
      let y := match goal with |- ?y => constr:(y) end in
      let P := match (eval pattern p in y) with ?f p => constr:(f) end in
      apply (@transport _ P _ _ (type_eq_sym_type_eq_sym p)); simpl in *.
      generalize (type_eq_sym p); intro p'; clear p.
      destruct p' as [|[]]; simpl.
      reflexivity.
    Defined.

    Global Instance isequiv_lift A : IsEquiv (@lift A).
    Proof.
      refine (@BuildIsEquiv
                _ _
                lift lower'
                lift_lower
                lower_lift
                _).
      compute.
      intro x.
      destruct (type_cast_up A) as [T' p].
      let y := match goal with |- ?y => constr:(y) end in
      let P := match (eval pattern p in y) with ?f p => constr:(f) end in
      apply (@transport _ P _ _ (type_eq_sym_type_eq_sym p)); simpl in *.
      generalize (type_eq_sym p); intro p'; clear p.
      destruct p' as [|[]]; simpl.
      reflexivity.
    Defined.
  End equiv.
  Definition lower {A} := (@equiv_inv _ _ (@lift A) _).
End LiftT.

Module Lift : LiftT.
  Section local.
    Let type_cast_up_type : Type.
    Proof.
      let U0 := constr:(Type) in
      let U1 := constr:(Type) in
      let unif := constr:(U0 : U1) in
      exact (forall T : U0, { T' : U1 & type_eq T' T }).
    Defined.

    Definition type_cast_up : type_cast_up_type
      := fun T => existT (fun T' => type_eq T' T) T (type_eq_refl _).
  End local.

  Definition Lift (T : Type) := projT1 (type_cast_up T).
  Definition lift {T} : T -> Lift T
    := match projT2 (type_cast_up T) in (type_eq _ T') return T' -> Lift T with
         | type_eq_refl => fun x => x
         | type_eq_impossible bad _ => match bad with end
       end.
  Section equiv.
    Definition lower' {T} : Lift T -> T
      := match projT2 (type_cast_up T) in (type_eq _ T') return Lift T -> T' with
           | type_eq_refl => fun x => x
           | type_eq_impossible bad _ => match bad with end
         end.
    Definition lift_lower {T} (x : Lift T) : lift (lower' x) = x.
    Proof.
      unfold lower', lift.
      destruct (projT2 (type_cast_up T)) as [|[]].
      reflexivity.
    Defined.
    Definition lower_lift {T} (x : T) : lower' (lift x) = x.
    Proof.
      unfold lower', lift, Lift in *.
      destruct (type_cast_up T) as [T' p]; simpl.
      let y := match goal with |- ?y => constr:(y) end in
      let P := match (eval pattern p in y) with ?f p => constr:(f) end in
      apply (@transport _ P _ _ (type_eq_sym_type_eq_sym p)); simpl in *.
      generalize (type_eq_sym p); intro p'; clear p.
      destruct p' as [|[]]; simpl.
      reflexivity.
    Defined.

    Global Instance isequiv_lift A : IsEquiv (@lift A).
    Proof.
      refine (@BuildIsEquiv
                _ _
                lift lower'
                lift_lower
                lower_lift
                _).
      compute.
      intro x.
      destruct (type_cast_up A) as [T' p].
      let y := match goal with |- ?y => constr:(y) end in
      let P := match (eval pattern p in y) with ?f p => constr:(f) end in
      apply (@transport _ P _ _ (type_eq_sym_type_eq_sym p)); simpl in *.
      generalize (type_eq_sym p); intro p'; clear p.
      destruct p' as [|[]]; simpl.
      reflexivity.
    Defined.
  End equiv.
  Definition lower {A} := (@equiv_inv _ _ (@lift A) _).
End Lift.
(* Toplevel input, characters 15-24:
Anomaly: Invalid argument: enforce_eq_instances called with instances of different lengths.
Please report. *)

[mattam82]

Hmm, that's a hard one. It's a module design issue. When importing HoTT or running hoqtop you set universe polymorphism on, so everything is polymorphic here. When checking lower's body in Lift we try a conversion with LiftT's lower body, however the isequiv_lift there is depending on less universes than the one in Lift. So when checking isequiv_lift, module subtyping should do something about universes. But it's unclear to me what to do and will actually requires a change in the structure that is kept for module types, only a constr is there for Definitions or with constraints...

The question is then. If in the module type we have foo : ∀ ψ, τ := b. and in the module we get foo : ∀ ψ', τ' := b'. What should we do? I guess we should check that ψ' |= ψ and ψ' |- b' = b but really there is no link between ψ and ψ's variables in general (in the monomorphic case, I think it's alright, it's just the constraints and they talk about the same variables). In a way that requires solving a unification problem up to quantifications... Ok sorry to think out loud. Instead we should check Ψ /\ Ψ' |- b = b' -> ψ''. ψ'' will unify what's required to be unified between ψ and ψ'. Then we'll have to refine b' according to Ψ'' seen as a substitution: it might make the implementation less general, but will give back a term convertible with the ascribed body b. How does that sound?

[mattam82]

Hmm, It's not gonna be monotonic. A latter definition in the module might fail due to this restriction...

[mattam82]

This would mean that module signature ascriptions have to be checked incrementally... and then all that module subtyping should be done properly outside the kernel...

[andrejbauer]

Just give us those explicit universes and say it was our fault when asked about them.

[JasonGross]

@andrejbauer, what do you mean? I like having typical ambiguity most of the time, and don't want to give it up in most places. It would be nice to also be able to explicitly reason about universes, but I get the impression that this is hard. That was my goal in making this module, that you could use lift and lower to reason about universes a la Agda, on top of this system without explicit universes.

@mattam82, I am not sure what I expect the behavior to be, because I do not see the use of Definitions in Module Types. My intuition is that it should check that the body in the implementation is no more restrictive than the body in the type (but it can be less restrictive).

Here is a version with modules that type-checks:

Set Implicit Arguments.

Set Printing Universes.

Set Asymmetric Patterns.

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

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

Arguments paths_ind [A] a P f y p.
Arguments paths_rec [A] a P f y p.
Arguments paths_rect [A] a P f y p.

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

Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y :=
  match p with idpath => u end.

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

Definition Sect {A B : Type} (s : A -> B) (r : B -> A) :=
  forall x : A, r (s x) = x.

(** A typeclass that includes the data making [f] into an adjoint equivalence. *)
Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv {
  equiv_inv : B -> A ;
  eisretr : Sect equiv_inv f;
  eissect : Sect f equiv_inv;
  eisadj : forall x : A, eisretr (f x) = ap f (eissect x)
}.

Arguments eisretr {A B} f {_} _.
Arguments eissect {A B} f {_} _.
Arguments eisadj {A B} f {_} _.

Inductive type_eq (A : Type) : Type -> Type :=
| type_eq_refl : type_eq A A
| type_eq_impossible : False -> forall B : Type, type_eq A B.

Definition type_eq_sym {A B} (p : type_eq A B) : type_eq B A
  := match p in (type_eq _ B) return (type_eq B A) with
       | type_eq_refl => type_eq_refl _
       | type_eq_impossible f B => type_eq_impossible _ f A
     end.

Definition type_eq_sym_type_eq_sym {A B} (p : type_eq A B) : type_eq_sym (type_eq_sym p) = p
  := match p as p return type_eq_sym (type_eq_sym p) = p with
       | type_eq_refl => idpath
       | type_eq_impossible f _ => idpath
     end.

Module Type LiftT_Base.
  Section local.
    Let type_cast_up_type : Type.
    Proof.
      let U0 := constr:(Type) in
      let U1 := constr:(Type) in
      let unif := constr:(U0 : U1) in
      exact (forall T : U0, { T' : U1 & type_eq T T' }).
    Defined.

    Axiom type_cast_up : type_cast_up_type.
  End local.
End LiftT_Base.

Module MakeLift (Cast : LiftT_Base).
  Definition Lift (T : Type) := projT1 (Cast.type_cast_up T).
  Definition paths_Lift (T : Type) : (T : Type) = Lift T
    := match projT2 (Cast.type_cast_up T) in (type_eq _ T') return (T : Type) = T' with
         | type_eq_refl => idpath
         | type_eq_impossible bad _ => match bad with end
       end.
  Definition lift {T} : T -> Lift T
    := match paths_Lift T in (_ = T') return T -> T' with
         | idpath => fun x => x
       end.
  Global Instance isequiv_lift T : IsEquiv (@lift T)
    := match paths_Lift T as p in (_ = T') return
             @IsEquiv (T : Type) (T' : Type)
                      (match p in (paths _ T') return (T : Type) -> (T' : Type) with
                         | idpath => fun x => x
                       end)
       with
         | idpath => @BuildIsEquiv
                       _ _
                       (fun x => x)
                       (fun x => x)
                       (fun _ => idpath)
                       (fun _ => idpath)
                       (fun _ => idpath)
       end.
  Definition lower {A} := (@equiv_inv _ _ (@lift A) _).
End MakeLift.

Module CastBase : LiftT_Base.
  Section local.
    Let type_cast_up_type : Type.
    Proof.
      let U0 := constr:(Type) in
      let U1 := constr:(Type) in
      let unif := constr:(U0 : U1) in
      exact (forall T : U0, { T' : U1 & type_eq T T' }).
    Defined.

    Definition type_cast_up : type_cast_up_type
      := fun T => existT (fun T' => type_eq T T') T (type_eq_refl _).
  End local.
End CastBase.

Module Lift := MakeLift CastBase.

Set Printing Universes.

Check @Lift.Lift.
Check @Lift.lift.
Check @Lift.paths_Lift.
Check @Lift.isequiv_lift.

Fail Check Lift.Lift nat : Set.

[JasonGross]

And here is a smaller version that doesn't use Modules and seems to work more nicely. I might go integrate this into HoTT:

Set Implicit Arguments.
Set Printing Universes.
Set Asymmetric Patterns.

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

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

Arguments paths_ind [A] a P f y p.
Arguments paths_rec [A] a P f y p.
Arguments paths_rect [A] a P f y p.

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

Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y :=
  match p with idpath => u end.

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

Definition Sect {A B : Type} (s : A -> B) (r : B -> A) :=
  forall x : A, r (s x) = x.

(** A typeclass that includes the data making [f] into an adjoint equivalence. *)
Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv {
  equiv_inv : B -> A ;
  eisretr : Sect equiv_inv f;
  eissect : Sect f equiv_inv;
  eisadj : forall x : A, eisretr (f x) = ap f (eissect x)
}.

Arguments eisretr {A B} f {_} _.
Arguments eissect {A B} f {_} _.
Arguments eisadj {A B} f {_} _.

Inductive type_eq (A : Type) : Type -> Type :=
| type_eq_refl : type_eq A A
| type_eq_impossible : False -> forall B : Type, type_eq A B.

Section local.
  Let type_cast_up_type : Type.
  Proof.
    let U0 := constr:(Type) in
    let U1 := constr:(Type) in
    let unif := constr:(U0 : U1) in
    exact (forall T : U0, { T' : U1 & type_eq T T' }).
  Defined.

  Definition type_cast_up : type_cast_up_type
    := fun T => existT (fun T' => type_eq T T') T (type_eq_refl _).
End local.

Definition Lift (T : Type) := projT1 (type_cast_up T).
Definition paths_Lift (T : Type) : (T : Type) = Lift T
  := match projT2 (type_cast_up T) in (type_eq _ T') return (T : Type) = T' with
       | type_eq_refl => idpath
       | type_eq_impossible bad _ => match bad with end
     end.
Definition lift {T} : T -> Lift T
  := match paths_Lift T in (_ = T') return T -> T' with
       | idpath => fun x => x
     end.
Global Instance isequiv_lift T : IsEquiv (@lift T)
  := match paths_Lift T as p in (_ = T') return
           @IsEquiv (T : Type) (T' : Type)
                    (match p in (paths _ T') return (T : Type) -> (T' : Type) with
                       | idpath => fun x => x
                     end)
     with
       | idpath => @BuildIsEquiv
                     _ _
                     (fun x => x)
                     (fun x => x)
                     (fun _ => idpath)
                     (fun _ => idpath)
                     (fun _ => idpath)
     end.
Definition lower {A} := (@equiv_inv _ _ (@lift A) _).

Fail Check Lift nat : Set.
Check 1 : Lift nat.

[JasonGross]

And this also seems to work (building on the above):

Definition lift {T} : T -> Lift T := fun x => x.
Global Instance isequiv_lift T : IsEquiv (@lift T)
  := @BuildIsEquiv
       _ _
       (fun x => x)
       (fun x => x)
       (fun _ => idpath)
       (fun _ => idpath)
       (fun _ => idpath).
Definition lower {A} := (@equiv_inv _ _ (@lift A) _).

[JasonGross]

This seems fixed in trunk-polyproj.