search

antalsz / hs-to-coq

Convert Haskell source code to Coq source code
https://hs-to-coq.readthedocs.io
MIT License
279 stars 27 forks source link

Translating ADTs with constructors containing type variables #120

Closed lastland closed 5 years ago

lastland commented 5 years ago

hs-to-coq is able to translate ADTs and make certain parameters of the constructors implicit in Coq. For example, consider the following example:

data Foo a b = Bar Int

With proper edits (using data kinds to hint hs-to-coq that a and b have kind Type), this will be translated to Coq in the correct form:

Inductive Foo (a : Type) (b : Type) : Type := Bar : GHC.Num.Int -> Foo a b.

Arguments Bar {_} {_} _.

However, the translation is no longer correct once there are implicit parameters inside the constructors as well. For example:

data Foo a b = Bar Int | forall x. Baz x

This piece of code will be translated to

Inductive Foo (a : Type) (b : Type) : Type
  := Bar : GHC.Num.Int -> Foo a b
  |  Baz {x} : x -> Foo a b.

Arguments Bar {_} {_} _.

Arguments Baz {_} {_} _.

In fact, the correct arguments for Baz should be:

Arguments Baz {_} {_} {_} _.

Notice that the code I provided above requires language extensions such as GADTs and ScopedTypeVariables to be enabled.