Coq last occurrence of "typ" must have "A" as 1st argument

Question

Inductive json : Type :=
| Assoc : list (prod string json) -> json
| Bool : bool -> json
| Float : Q -> json
| Int : Z -> json
| List : list json -> json
| Null : unit -> json
| String : string -> json
| Tuple : list json -> json
| Variant : prod string (option json) -> json.

Inductive typ (A:Type) : Type :=
| TAssoc : typ (list (prod string json))
| TBool : typ bool 
| TFloat : typ Q 
| TInt : typ Z 
| TList : typ (list json)
| TNull : typ unit 
| TString : typ string 
| TTuple : typ (list json) 
| TVariant : typ (prod string (option json)).

Definition extract (A:Type) (j:json) (t:typ A) : option A :=
    match j,t with
    | Assoc x, TAssoc => Some x
    | Bool x, TBool => Some x
    | Float x, TFloat => Some x
    | Int x, TInt => Some x
    | List x, TList => Some x
    | String x, TString => Some x
    | Variant x, TVariant => Some x
    | _, _ => None
    end.

I wanted to check the correctness of the extract function, but Coq gave me an error,

Last occurrence of "typ" must have "A" as 1st argument in "typ (list (string * json))".

But in OCaml (or in Haskell), I can make a GADTs like this with almost the same definition,

type 'a foo = Foo : int foo

I don't understand the error actually.What does it mean?

If you could make your code compile up until `extract`, that would help a lot. — Anton Trunov, Jun 23 '18 at 11:22
Oh, so the error message is about `typ`, not `extract`. You probably meant something like `Inductive typ : Type -> Type := ...` — Anton Trunov, Jun 23 '18 at 11:28
I think [this question](https://stackoverflow.com/q/24600256/2747511) should be useful in this case. — Anton Trunov, Jun 23 '18 at 11:31

score 0 · Answer 1 · answered Jun 23 '18 at 13:21

As @AntonTrunov put it, I successfully suppressed the error by changing the type like that

Inductive typ : Type -> Type :=
| TAssoc : typ (list (prod string json))
| TBool : typ bool 
| TFloat : typ Q 
| TInt : typ Z 
| TList : typ (list json)
| TNull : typ unit 
| TString : typ string 
| TTuple : typ (list json) 
| TVariant : typ (prod string (option json)).

It works!

Coq last occurrence of "typ" must have "A" as 1st argument

1 Answers1