GADT compilation failure with Hoopl example

[bollu]

Experiment

Consider the piece of haskell code (which is extracted from Hoopl):

{-# LANGUAGE GADTs #-}
data O
data C
data MaybeO ex t where
  JustO    :: t -> MaybeO O t
  NothingO ::      MaybeO C t

main :: IO ()
main = undefined

This generates the coq code from hs-to-coq:

(* Main *)

(* Default settings (from HsToCoq.Coq.Preamble) *)

Generalizable All Variables.

Unset Implicit Arguments.
Set Maximal Implicit Insertion.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Require Coq.Program.Tactics.
Require Coq.Program.Wf.

(* Converted imports: *)

Require GHC.Err.
Require GHC.Types.

(* Converted type declarations: *)

Inductive O : Type :=.

Inductive C : Type :=.

Inductive MaybeO ex t : Type
  := JustO : forall {t}, t -> MaybeO O t
  |  NothingO : forall {t}, MaybeO C t.
(* Converted value declarations: *)

Definition main : GHC.Types.IO unit :=
  GHC.Err.undefined.

(* External variables:
     unit GHC.Err.undefined GHC.Types.IO
*)

Error

╰─$ coqc fail.v
File "./fail.v", line 27, characters 21-22:
Error:
t is already used as name of a parameter of the inductive type; bound
variables in the type of a constructor shall use a different name.

On changing the declaration of MaybeO to:

(* === edited declaration to fix t=== *)
Inductive MaybeO ex t : Type
  := JustO :  t -> MaybeO O t
  |  NothingO :  MaybeO C t.

It fails with the error:

Press ENTER or type command to continue%                                                                                                                               ╰─$ coqc fail.v
File "./fail.v", line 26, characters 0-87:
Error: Last occurrence of "MaybeO" must have "ex" as 1st argument in
 "t -> MaybeO O t".

Expected

The version of MaybeO produced is weird. In particular, I would have expected something like this to be generated:

(* ===Expected code=== *)
Inductive MaybeO: Type -> Type -> Type
  := JustO : forall {t}, t -> MaybeO O t
  |  NothingO : forall {t}, MaybeO C t.

In the version that is compiled by hs-to-coq, there are two problems:

1. The t variable is already bound by the Inductive MaybeO ex t, thus it should not be reused at the forall {t}.

2. the hs-to-coq declaration does not capture what the haskell code is trying to say? (Note: I do not understand Coq very well, so I could be wrong here)

The hs-to-coq version is creating a type Maybe :: (ex: *) -> (o : *) -> *, whose inhabitants have types Maybe ex o for all ex, o :: *.

The version I wrote creates a type MaybeO :: * -> * -> *, whose inhabitants are MaybeO O t and MaybeO C t.

Is there something I am missing (am I compiling my code wrong?) Or does hs-to-coq not support this as of now?

Thanks!

[sweirich]

Hi Siddarth,

Thanks for your report. We haven't tried hs-to-coq on many GADTs yet and don't consider them a supported feature. However, I found that adding the edits

data type arguments GADT.MaybeO  (indices: ex t)
data kinds GADT.MaybeO Type, Type

with your original file (after adding module GADT where at the beginning)

produces the following Coq output (after the usual preamble).

 Inductive O : Type :=.

Inductive C : Type :=.

Inductive MaybeO : forall (ex t : Type), Type
  := JustO : forall {ex t : Type}, forall {t}, t -> MaybeO O t
  |  NothingO : forall {ex t : Type}, forall {t}, MaybeO C t.

The reason that the edits are necessary is that Coq makes a distinction between datatype parameters and indices but Haskell does not. By default, hs-to-coq outputs definitions only using parameters, because they are more commonly used. However, GADTs require the use of indices instead. Perhaps we could make hs-to-coq smarter in this respect, but for now the user must specify. The second edit provides kind information for the type variables: Coq cannot infer them in this situation.

[bollu]

Thank you! Much appreciated :) I did not know the terminology regarding "indeces" and "datatype parameter", but now I do.

If GADTs are not considered supported, is it still okay to send issues regarding GADTs?

[bollu]

I am unable to get the example working. You mentioned "... adding the edits" - Adding the edits where? To an edits file? (This does not seem to be the case, since the syntax does not seem like that of an edits file). I am not sure which file I must edit.

[sweirich]

Sorry for being unclear --- yes, to an edits file.

We don't mind issues about GADTs (they help us understand what the tool does and does not currently support.) However, GADTs are not our current priority so we may not fix them.

[bollu]

Ah, thanks! I now understood what you meant :)

You meant:

1. edit the .hs file to add a module GADT where ... <haskell definitions>.

2. add the definitions

data type arguments GADT.MaybeO  (indices: ex t)
data kinds GADT.MaybeO Type, Type

to the edits file, and the invoke hs-to-coq --edits <edits-file> <haskell-file.hs> Much appreciated.