DefaultSignatures

[lastland]

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]

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]

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]

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

[lastland]

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