DefaultSignatures

[lastland]

Issue by lastland Wednesday Nov 29, 2017 at 21:10 GMT Originally opened as https://github.com/antalsz/hs-to-coq/issues/50

---

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.

[lastland]

Comment by nomeata Wednesday Nov 29, 2017 at 22:01 GMT

---

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]

Comment by lastland Wednesday Nov 29, 2017 at 22:04 GMT

---

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.

[lastland]

Comment by nomeata Thursday Nov 30, 2017 at 14:20 GMT

---

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

[lastland]

Comment by lastland Thursday Nov 30, 2017 at 16:08 GMT

---

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).