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

Deal with `Default` instance generation #102

Open antalsz opened 6 years ago

antalsz commented 6 years ago

As we saw in #100 (preserving record names), our story for tracking Default instances isn't great and needs some manual skipping.

As I understand it, #100 introduces too many Default instances, and so we need to start keeping better track of which types have such instances. That way, we can check that some constructor can be fully applied to default arguments.

I haven't looked at the Default code, but we'll need to be careful to differentiate between three cases:

  1. Default Int – type of kind Type which may or may not have Default instances.
  2. Default (Maybe a) – type constructors which always have a Default instance.
  3. Default a => Default (Pair a) – type constructors which have a Default instance when their arguments do.

This also doesn't address higher-order type constructors…

sweirich commented 6 years ago

Can you make this ticket more concrete?

antalsz commented 6 years ago

@sweirich done, although I haven't looked into the details closely