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

DefaultSignatures #50

Open lastland opened 6 years ago

lastland commented 6 years ago

Semigroup.hs used the DefaultSignatures extension to define the Semigroup type class:

class Semigroup a where
  (<>) :: a -> a -> a

  default (<>) :: Monoid a => a -> a -> a
  (<>) = mappend

  sconcat :: NonEmpty a -> a
  sconcat = ... 

  stimes :: Integral b => b -> a -> a
  stimes = ...

Notice that the default method has a different type signature.

hs-to-coq will translate the above type class into the following (wrong) Coq code:

Record Semigroup__Dict a := Semigroup__Dict_Build {
  sappend__ : forall `{GHC.Base.Monoid a}, a -> a -> a ;
  sconcat__ : Data.List.NonEmpty.NonEmpty a -> a ;
  stimes__ : forall {b}, forall `{GHC.Real.Integral b}, b -> a -> a }.

The Monoid constraint should not appear in the type signature.

nomeata commented 6 years ago

So it’s just a matter of picking the right signature?

If you fix it manually in the coq file, does the rest go through?

lastland commented 6 years ago

It doesn't. In particular, there is something wrong with the ordering of some instances, but I don't know whether that's caused by this as well or not.

nomeata commented 6 years ago

Oh, ordering of instances often needs manual intervention, using order edits.

lastland commented 6 years ago

I'm aware of that. In fact, I had order edits and yet hs-to-coq generates the instances in the wrong order. Removing the default method from original Haskell file fixes that part of the problem. So somehow the default method influences the ordering (I haven't figured out why).