The Coq mailing list

["Edward Z. Yang" <ezyang AT MIT.EDU>]

I thought it would be fun to port the Chapman-Dagand-McBride-Morris closed
theory of datatypes to Coq. [1]  (I was on a plane and reading their recent
ornaments paper [2], so forgive me for not realizing that the original 
authors had
already done so [3]--however, as you will see, they ran into the same 
difficulty
as me.)  There is a problem:

(**)
    Inductive IDesc {I : Set} : Type :=
      | Var : I -> IDesc
      | One : IDesc
      | Prod : forall S : Set, (S -> @IDesc I) -> IDesc
      | Sum : forall S : Set, (S -> @IDesc I) -> IDesc.

    Fixpoint interp {I : Set} (D : @IDesc I) (X : I -> Set) : Set :=
      match D with
          | Var i => X i
          | One => unit
          | Prod S' T => forall s : S', interp (T s) X
          | Sum S' T => sigT (fun s => interp (T s) X)
      end.

    Inductive Mu {I : Set} (D : I -> @IDesc I) (i : I) : Set :=
      | In : interp (D i) (Mu D) -> Mu D i.
(**)

Coq complains:

(**)
    Error: Non strictly positive occurrence of "Mu" in
     "interp (D i) (Mu I D) -> Mu I D i".
(**)

If we look at interp, it's easy to see: X is never used in a non
strictly positive occurrence. But Coq seems to throw its hands up
in the air and give up, when a Fixpoint is involved!

One can find a suspiciously similar encoding commented out in [2]:

(**)
    (*
    Inductive Mu (D : Desc) : Type :=
        con : descOp D (Mu D) -> Mu D.
    *)

    Inductive MuU (R : Desc)(D : Desc) : Type :=
        id : forall p : Is_true (isId D),
             MuU R R -> MuU R D
      | const : forall p : Is_true (isConst D),
                ConstSet D p -> MuU R D
      | prod : forall p : Is_true (isProd D),
               { x : MuU R (ProdFst D p) & MuU R (ProdSnd D p)} ->
               MuU R D
      | sigma : forall p : Is_true (isSigma D),
                { s : SigmaHd D p & MuU R (SigmaTl D p s)} -> 
                MuU R D
      | pi : forall p : Is_true (isPi D),
             (forall s : PiHd D p, MuU R (PiTl D p s)) ->
             MuU R D
    .
(**)

After which the authors proceed to convert the moral equivalent of interp
into an inductive datatype all by itself, which is very not nice.

So, is there any way to do this properly in Coq?  Teach the positivity
checker to be more clever?  A more clever hack than MuU?  Smells like
something of a puzzle.

Cheers,
Edward

[1] 
https://personal.cis.strath.ac.uk/pierreevariste.dagand/papers/levitation.pdf
[2] http://arxiv.org/abs/1201.4801
[3] 
https://personal.cis.strath.ac.uk/pierreevariste.dagand/stuffs/levitate.tar.gz