When will you support Coq 8.7.1?

[jimyu94]

I tried to compile with Coq 8.7.1 and coq-mathcomp-ssreflect 1.6.4, but got the following error:

COQC Data/Foldable.v
File "./Data/Foldable.v", line 152, characters 4-9:
Error:
In environment
f : Type -> Type
foldMap : forall m a : Type, Base.Monoid m -> (a -> m) -> f a -> m
foldr : forall a b : Type, (a -> b -> b) -> b -> f a -> b
foldl :=
fun (b a : Type) (f0 : b -> a -> b) (z : b) (t : f a) =>
appEndo
  (getDual
     (foldMap (Dual (Endo b)) a ?H@{f0:=f; f:=f0}
        (Basics.compose Mk_Dual (Basics.compose Mk_Endo (Base.flip f0))) t))
  z : forall b a : Type, (b -> a -> b) -> b -> f a -> b
foldl' :=
fun (b a : Type) (f0 : b -> a -> b) (z0 : b) (xs : f a) =>
let f' := fun (x : a) (k : b -> b) (z : b) => k GHC.Base.$! f0 z x in
foldr a (b -> b) f' Base.id xs z0 :
forall b a : Type, (b -> a -> b) -> b -> f a -> b
The term "foldl ?b ?a" has type "(?b -> ?a -> ?b) -> ?b -> f ?a -> ?b"
while it is expected to have type
 "forall b a : Type, (b -> a -> b) -> b -> f a -> b".

make: *** [Data/Foldable.vo] Error 1

I didn't try it with Coq 8.6, but I suppose this error occurs since I am using 8.7.1. Considering Coq 8.7 is a compatibility-focused release, I guess your code could be easily converted to this version. Would you please commit a change? Thank you so much!

[nomeata]

Thanks for trying hs-to-coq. At the moment, supporting multiple versions of Coq is not a priority, so I recommend that you try 8.6 for now (opam can help with managing multiple versions of Coq).

If you find that this problem is easily fixable in a way that works with both 8.6 and 8.7, please submit a patch!

[nomeata]

Ok, Coq 8.7 is supported now. @jimyu94, if that prevented you from trying hs-to-coq, try again :-)