coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Coq 8.5 extractor bug

From: Kazuhiko Sakaguchi <pi8027 AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Coq 8.5 extractor bug
Date: Tue, 9 Feb 2016 20:11:34 +0900
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=pi8027 AT gmail.com; spf=Pass smtp.mailfrom=pi8027 AT gmail.com; spf=None smtp.helo=postmaster AT mail-yk0-f178.google.com
Ironport-phdr: 9a23:DRhiWx8uaoBVFv9uRHKM819IXTAuvvDOBiVQ1KB90OIcTK2v8tzYMVDF4r011RmSDdqdsKoP0bCempujcFJDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXsq3G/pQQfBg/4fVIsYL+lRciJ14/tjaibwN76XUZhvHKFe7R8LRG7/036l/I9ps9cEJs30QbDuXBSeu5blitCLFOXmAvgtI/rpMYwu3cYh/V0/MlZFK7+Yq4QTLpCDT1gPXpmytfssEzgRBmS5nofVS0tmxlBDBXO7BCyCo/w4nOg6cJy3SCbOYv9SrViCmfq1LtiVBK90HRPDDU+6myC0sE=

Hello,

I found an extracted code that can't be typed in OCaml and Haskell.
This issue happens on Coq 8.5, however, it can't be reproduced in Coq
8.5 beta 3.

For more details, please see attached file.

Thanks,

Kazuhiko

Record rec := {
  T :> Type;
  _ : T;
  _ : (T -> T) * T;
}.

Definition Rec := Build_rec.

Module Type Sig.
Parameter tt' : Rec unit tt ((fun x => x), tt).
End Sig.

Module Mod : Sig.
Definition tt' := tt.
End Mod.

Definition x :=
  match Rec unit tt ((fun x => x), tt) as T return T -> T with
    Build_rec _ _ (f, _) => f
  end
  Mod.tt'.

Extraction Language Ocaml.
Extraction "x.ml" x.
Extraction Language Haskell.
Extraction "x.hs" x.

[Coq-Club] Coq 8.5 extractor bug, Kazuhiko Sakaguchi, 02/09/2016
- Re: [Coq-Club] Coq 8.5 extractor bug, Jacques-Henri Jourdan, 02/09/2016