Error: Universe inconsistency (cannot enforce Set <= Prop because Prop < Set). about coq HOT 14 CLOSED

So, here's a shorter example (i.e., no external dependencies) which gives "Error: Universe inconsistency (cannot enforce Set <= Prop)." I'm not sure what happened to the "because Prop < Set" part...

Set Printing Universes.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Universe Polymorphism.

Inductive Unit : Type :=
    tt : Unit.

Inductive Bool : Type :=
  | true : Bool
  | false : Bool.

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

Record PreCategory :=
  {
    Object :> Type;
    Morphism : Object -> Object -> Type
  }.

Definition DiscreteCategory X : PreCategory
  := @Build_PreCategory X
                        (@paths X).

Definition IndiscreteCategory X : PreCategory
  := @Build_PreCategory X
                         (fun _ _ => Unit).

Definition NatCategory (n : nat) :=
  match n with
    | 0 => IndiscreteCategory Unit
    | _ => DiscreteCategory Bool
  end.
(* Error: Universe inconsistency (cannot enforce Set <= Prop).*)

Once again, replacing the Type in Morphism with Set removes the universe inconsistency. The actual file that I'm using is https://github.com/JasonGross/HoTT-categories/blob/master/theories/NatCategory.v.

from coq.

Oops, nevermind, I was running an old version of hoqtop, I think? I'll close or comment again once I figure out what I was doing wrong.

from coq.

This is a problem with hoqc, but not HoTT/coq. I'm rather confused. I'll go report it there, but leave it open here.

from coq.

Ah, the problem is with -indices-matter; the fix for #50 only works without -indices-matter.

from coq.

Ok, without indices-matter, we'd get two PreCategory (* Set Prop ) because both morphisms types lied in Prop. With indices-matter, we get one PreCategory ( Set Set ) for Bool and one PreCategory ( Set Prop *) for Unit (which lives in Prop still). The only way to fix it would be to move [Unit] to Set (where I think it should be) as there is no notion of implicit coercion from one polymorphic inductive instance to another.

from coq.

It seems like having a notion of implicit coercion between polymorphic inductive instances would be a nice, if seldom-used, feature to have (though I imagine that you'd have to take variance into account to get the universe subtyping to work out, and this might make it annoyingly complicated).

If I don't want to move Unit to Set (which I actually already have), I could do

Definition NatCategory (n : nat) :=                                                                                                         
  match n as n return match n with 0 => _ | _ => _ end with                                                                                 
    | 0 => IndiscreteCategory Unit                                                                                                          
    | _ => DiscreteCategory Bool                                                                                                            
  end.

But then I can't do fun n : nat => Object (NatCategory n), and have to first destruct n. But this is not very important. Perhaps if there is no easy way to do this, mark down somewhere that this is on a wish list?

from coq.

Indeed, it looks very complicated, and even if we had a good variance analysis, coercion could be dangerous as it might make a term typecheck when you'd rather have an inconsistency...

from coq.

Is variance a solved problem for W-types? I think I understand variance for Pi types, and I feel like you should be able to do some sort of structural induction over W-types to figure out variance.

My understanding of universe inconsistencies is that their primary purpose is to have a systematic way of preventing the type-checking of terms that exploit size paradoxes to prove False. So I feel like universe inconsistencies, ideally, should only come up when you're trying to prove False by exploiting a size issue. Are there other times that you'd prefer an inconsistency?

from coq.

Actually, it seems that Coq already knows about variance, to some degree. If I manually unfold IndiscreteCategory in the example above, then the definition goes through, because Unit is re-typechecked as a Set. But normalizing everything to determine whether or not there's a universe inconsistency seems prohibitively expensive. Perhaps one way to do it would be to equip each universe variable with a variance which it gets at type-checking/initialization time, and which should be able to be determined by some simple rules (if you unify two universes of different known variances, both become non-variant, and in all cases their variances must be the same; and the rule for Pi/arrow types might be sufficient?)? (But, again, this seems like a large project for not very much gain, and I don't expect to see it anytime soon, if ever.)

from coq.

Indeed, it should be possible in principle, to make the Pi/arrow variance go through inductives. One can easily check variance by building an identity function on each inductive type I us -> I vs which will infer the necessary universe constraints on us and vs, at least in simple cases. However I'm not sure how to apply it to general terms without doing normalization. One could indeed have a variance inference during typechecking, but I'm a bit worried you'd also have to look at the constraints to decide it. Anyway, I'm thinking about it.

from coq.

Would it be possible to first try to do universe checking without any coercions, and then, instead of raising a universe inconsistency if it come to that, unfold the heads of the things which you failed to unify, and try again? (That is, is it possible to be able to do normalization, but not feel the cost of this unless you'd get a universe inconsistency without normalization? And, further, to partially normalize, so that only as much is unfolded as I'd need to manually unfold to make it go through?)

from coq.

That is already what happens in my branch. If you unify two transparent constants and unifying their universe instances raises a universe inconsistency then it backtracks to unfolding. Note that it would not change anything here as IndiscreteCategory and DiscreteCategory already have fixed universes that are incompatible (Set and Prop).

from coq.

I'm confused, then, why

Definition NatCategory (n : nat) :=                                                                                                         
  match n with                                                                                                                              
    | 0 => (fun X => @Build_PreCategory X                                                                                                   
                         (fun _ _ => Unit : Prop)) Unit                                                                                     
    | _ => DiscreteCategory Bool                                                                                                            
  end.

typechecks when

Definition NatCategory (n : nat) :=
  match n with
    | 0 => IndiscreteCategory Unit
    | _ => DiscreteCategory Bool
  end.

does not?

Is it because the universes for X and/or Prop are refreshed in the first case but not in the second? If so, is there a reason that the relevant universes can't be refreshed after unfolding in the second case?

from coq.

Fixed in trunk-polyproj (but not in HoTT/coq trunk), so closing here.

from coq.