The Coq mailing list

[Roger Witte <rogerwite AT yahoo.co.uk>]

The error message is indicating s universe inconsistency.  i have encountered this error when a declaration that should be monographic is declared polymorphic.  Unfortunately the declaration concerned is not the one in which the error occurs.

If possible, just make your project Universe Monographic.  If you still get universe inconsistency, you may need to check that you really haven't hit a paradox.

If you are sure that you are not trying to put a proper class inside a set, then you need to ensure that you fon't do so accidently.

There ate two approaches:

Explicit declaration and specification of universes or explicit declaration of monomorphic and polymorphic.  These are not mutually exclusive.

Personally I find this difficult and end up doing s fair amount of trial and error.  I find that polymorphic things often default to being in too large a universe but that monomorphic things or things with explicitly declared universes end up in too small a universe.

i know Regis list contains experts who will offer you more precise and helpful advice, but I am hoping that by highlighting precisely what I have and have not been able to learn from the reference manual, I can help them to improve the documentation.

Sent from Yahoo Mail on Android

On Sun, 13 Mar, 2016 at 18:56, Lars Rasmusson

<Lars.Rasmusson AT sics.se> wrote:

Hi,

I'm trying to implement the postfix parser in sec. 3.1 of Ralf Hinze's Functional Pearl Compile Time Parsing [1] (for Haskell) with the definitions of Monad and the Continuation Passing Style Monad given below.

To do that I need to be able to type  for instance this term. 

   (return_ tt _ leaf)

but Coq gives the error below.  Is there some way to type this program in Coq?  

(Probably I have made an error somewhere, but I'm not able to spot it.)

Thankful for any help!

/Lars

[1] http://www.cs.ox.ac.uk/people/ralf.hinze/publications/Quote.pdf

(**********************************************************************)

Class Monad (m: Type -> Type): Type :=

  {

    return_ {A}:     A -> m A;

    bind    {A B}:   m A -> (A -> m B) -> m B;

    right_unit {A}:  forall (a: m A), bind a return_ = a;

    left_unit  {A}:  forall (a: A) B (f: A -> m B),

                       bind (return_ a) f = f a;

    associativity {A B C}:

                     forall a (f: A -> m B) (g: B -> m C),

                       bind a (fun x => bind (f x) g) = bind (bind a f) g

}.

Notation "a >>= f" := (bind a f) (at level 50, left associativity).

Definition lift {m} {M:Monad m} {A B: Type} (f: A->B) (a: A): m B :=

  return_ (f a).

Definition CPS (S:Type) := forall A, (S->A) -> A.

Instance CPSMonad : Monad CPS  :=

  {|

    return_ S s A f := f s ;

    bind    A B m k C c := m _ (fun a => k a _ c)

  |}.

auto. auto. auto. Defined.

(**********************************************************************)

Inductive Tree := Leaf | Fork (_ _:Tree).

Definition leaf_ ST (st:ST) := (st, Leaf).

Definition leaf {ST:Type}   := lift (leaf_ ST).

Definition

(* this works *)

Check (return_ tt) >>= leaf.

(* this doesn't work *)

Check return_ tt _ leaf.

(*

Toplevel input, characters 19-23:

Error:

The term "leaf" has type "unit -> CPS (unit * Tree)"

while it is expected to have type "unit -> ?T"

(unable to find a well-typed instantiation for "?T": cannot ensure that

"Type@{max(Top.27, Top.29+1)}" is a subtype of "Type@{Top.29}").

 *)

(* More like in the paper, just for fun 

Module example.

  Definition quote := return_ tt.

  Definition leaf_ ST (st:ST) := (st, Leaf).

  Definition leaf {ST:Type}   := lift (leaf_ ST).

  Definition fork_ ST (st:(ST * Tree) * Tree) :=

    match st with ((st',l),r) => (st', Fork l r) end.

  Definition fork {ST}               := lift (fork_ ST).

  Definition endquote (st:unit*Tree) := match st with (_,t) => t end.

  (* this constructs the Tree (Fork Leaf Leaf) *)

  Compute (quote >>= leaf >>= leaf >>= fork >>= (lift endquote)) _ (fun x=>x).

  Arguments quote {_} _.

  (* this should do the same but fails with the same error as above*)

  Check quote leaf leaf fork endquote.

End example.

*)