[WIP] migrating to GHC 8.10 and Coq 8.18. #205
Draft
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
Hi there, This new translation newtype Down a = Down
{ getDown :: a -- ^ @since 4.14.0.0
}looked to my like the Class Setoid :=
{
carr : Type;
...
}
Class Group :=
{
base_Setoid :: Setoid
neutr : carr
...
}.I noticed in my project, that problems occured, if I would have declared explicit Instances (for Example As I said, just wanted to share this as a thought, I do not have a detailed overview for this project. But I hope, that you can manage to migrate this project to a higher version. |
Unclear why this is necessary. Further investigation needed.
GHC changed the way that derived instances are processed. The new code closely follows code from newer GHC versions, namely in the function `tcTyClsInstDecls`.
This averts a problem caused by `GHC/Base.hs` importing `GHC/Maybe.hs`.
Add `/dev/null` to the list of files to `cat` so that `cat` doesn't try to read from stdin, and also to ensure that the target files always get created.
As of GHC 8.10.7, the base library has typeclass instances generated by
`GeneralizedNewtypeDeriving`. The following definition
```haskell
class C x where
g :: t
newtype N a = N a
deriving (C)
```
is translated into the following instance:
```haskell
instance C a => C (N a) where
g = GHC.Prim.coerce (g) :: t'
```
where `t'` is obtained by substituting `C a` for `x` in `t`.
This causes problems when `f` is a polymorphic function. For example,
if `g` is `fmap`, then `t` is `forall a b. (a -> b) -> f a -> f b`. The
resulting Gallina looks roughly like
```coq
Definition Functor__N_fmap {inst_a : Type} `{GHC.Base.Functor inst_a}
: forall {a b, Type}, (a -> b) -> N a -> N b :=
fun {a b : Type} => GHC.Prim.coerce (GHC.Base.fmap) : (a -> b) -> N a -> N b.
```
The problem is that `GHC.Base.fmap` has a fully-polymorphic type, but
our generated
`Functor__N_fmap` has already "eaten" the type arguments that it is
expecting. Coq will therefore fail to find an appropriate `Coercible` instance.
The underlying problem problem is that `GeneralizedNewtypeDeriving` is
breaking our assumption that the body of a Haskell definition never
takes any additional type arguments; i.e., all type arguments should
be (implicitly) already taken before the `=`. (Comment to that effect:
"ASSUMPTION: type variables don't show up in terms. Broken by
ScopedTypeVariables.")
The "correct" solution probably entails
inferring the type of the method body and unifying it against the expected
method type. But it would also require rather fishy-looking `Unpeel`
instance; something like
```coq
Instance Unpeel_forall (a : Type) (p q : a -> Type)
(u : forall x, HsToCoq.Unpeel.Unpeel (p x) (q x)) : HsToCoq.Unpeel.Unpeel (forall x, p x) (forall x, q x).
```
which would probably have to be given explicitly. This commit instead
takes the quick-and-dirty approach of simply detecting method bodies
that "look like" they were generated by `GeneralizedNewtypeDeriving` and
dropping their annotations. The above Gallina code becomes instead
```coq
Definition Functor__N_fmap {inst_a : Type} `{GHC.Base.Functor inst_a}
: forall {a b, Type}, (a -> b) -> N a -> N b :=
fun {a b : Type} => GHC.Prim.coerce (GHC.Base.fmap).
```
This does result in local type changes relative to the original Haskell
code (e.g., the argument to `coerce` is no longer fully-quantified), but
that is probably okay. Also, it could theoretically result in false
positives, but that is also probably okay.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR is a WIP that tries to migrate hs-to-coq to GHC 8.10 and Coq 8.18.
(I have also been trying to migrate it to GHC 9, but that requires more time than I currently have, so I'm instead trying GHC 8.10 for now.)
Changes:
Since Coq 8.18, the default locality of typeclass instances has been changed to
#[export], which requires a file toRequire ImportorRequire Exporta module to make these instances in scope. Unfortunately, this does not work well with our current method, as we usually onlyRequirea module. I have changed hs-to-coq to mark all instances with an explicit#[global]locality---this might not be the best way moving forward, but it should resolve many issues for now.Issues:
Our translation no longer produces derived instances for certain
newtypes, for example:DownfromData.Ord. I suspect the reason is that the definition of thesenewtypes has changed from:to
I don't know why such a change would result in hs-to-coq not producing the derived instance.
I need more time to dig into the issue. I am currently recording all these in this PR so I can remember what's going on in the future. If anyone is interested in helping us with this, please feel free to explore based on this branch---I am also happy to chat!