newtype deriving for standard classes (Eq, Ord, etc)

[sweirich]

We can't derive instances for newtypes because they use Data.Coerce. Can we pretend that they were written with 'data' instead?

[antalsz]

@nomeata is the one who implemented the deriving code, which currently just leans on GHC's deriving code.

[nomeata]

If we trust GHC, we can just add

Axiom coerce : forall {a} {b}, a -> b.

:-P

Seroiusly: I can have a look. It would likely be easily possible with GHC-8.2, where you can add deriving strategies (https://ghc.haskell.org/trac/ghc/wiki/Commentary/Compiler/DerivingStrategies), but I’ll see if we can trigger that behavior with GHC somehow.

Alternatively, we could pre-process the code before passing it to the type checker and instead of pretending it’s data, change it to be data. (Would only work if the newtype is defined in the current module, though.)

[nomeata]

Stephanie, have you thought about a manual file with a

Class Coercible a b := { coerce : a → b; uncoerce : b → a}

for which we write (or generate) instances for newtypes, and have instances corresponding to GHC’s rules for solving Coercible constraints. It is not a class in GHC, but maybe it can be a class in Coq? (Where, for example, we have backtracking in the type class search, IIRC.)

Even if it does not solve Coercible constraints in all cases where GHC can solve them, it might just work well enough in the relative simple cases posed by GND’ed instances.

[nomeata]

Or, another thought in that direction, if instance resolution is too weak: Have hs-to-coq translate coerce to (ltac:coerce) and implement GHC’s coercible solving strategy using an Ltac coerce :=…. (Just noting ideas here. Maybe I’ll give them a shot when the POPL AEC stuff is done.)

[nomeata]

That seems to work in simple cases, see 3bc06011 for a proof-of-concept.

(I could not do Monad Dual for an independent bug in the deriving integration, but Monad Dual is not even defined using coerce, #34)

In principle, all that is needed is

add Data.Monoid Instance Unpeel_Dual a : Unpeel (Dual a) a := Build_Unpeel _ _ getDual Mk_Dual.

and that should be reasonable to automate.

In practice, a few more order edits are necessary. But then you get Functor Dual and Applicative Dual!

[nomeata]

Hmm, it fails with Last, probably because the derived code uses TypeApplication there, which we do not support yet. Too bad.

But Product and Sum work.

Aha: Looking at the .hs I learn that these uses of coerce are actually manually put in the source, and do not arise due to deriving. Guess I was not addressing the problem of this ticket, but still produced something useful…

[nomeata]

Well, they work almost. We currently generate

Local Definition instance_forall___GHC_Num_Num_a___GHC_Base_Monoid__Product_a__mappend
    {inst_a}
    `{GHC.Num.Num inst_a} : (Product inst_a) -> (Product inst_a) -> (Product inst_a) :=
  GHC.Prim.coerce (GHC.Num.op_zt__ : a -> a -> a).

If we would generate

Local Definition instance_forall___GHC_Num_Num_a___GHC_Base_Monoid__Product_a__mappend
    {a}
    `{GHC.Num.Num inst_a} : (Product a) -> (Product a) -> (Product a) :=
  GHC.Prim.coerce (GHC.Num.op_zt__ : a -> a -> a).

instead (because type variables in instance heads are in scope in the body), then it would work, including resolution of the Coercible type classes.

[antalsz]

Ah, yes, I have an explicit comment about that in the source :-) In the function HsToCoq.ConvertHaskell.Declarations.Instances.topoSortInstance:

-- ASSUMPTION: type variables don't show up in terms.  Broken
-- by ScopedTypeVariables.

[sweirich]

I'm marking this as closed and opened a new ticket about the specific issue with scoped type variables.