Extraction: do not mix Haskell types Any and () (revert 8e257d4, fix bugs 4844 and 4824)

 The commit 8e257d4 (which consider the dummy type Tdummy to be polymorphic and hence
 immune of the need for unsafeCoerce) is quite wrong, even if in pratice it worked ok
 most of the time. The confusion comes from the fact that the dummy value (__ aka MLdummy
 internally) is implemented in Haskell as Prelude.error, hence it has indeed a polymorphic
 unrestricted type. But the dummy type Tdummy used when extracting types must be monomorphic
 (otherwise type parameters would have to be propagated out of any type definition involving
 Tdummy). We implement Tdummy by Haskell's (), which for instance isn't convertible to Any,
 as shown by the examples in bug reports 4844 and 4824.

 This fix will bring back some more unsafeCoerce in Haskell extraction, including possibly
 a few spurious ones. And these extra unsafeCoerce might also hinder further code optimisations.
 We tried to mitigate that by directly removing [MLmagic] constructors in front of [MLdummy _].

 NB: even if the original bug report mentions universe polymorphism, this issue is
 almost unrelated to it. It just happens that when universe polymorphism is off,
 an inductive instance is fully placed in Prop (cf. template polymorphism) in the example,
 avoiding triggering the issue.

 Warning: the test-suite file is there for archiving the repro case, but currently it doesn't
 test much (we should run ghc on the extracted code).

1 files changed, 47 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/4844.v b/test-suite/bugs/closed/4844.v
new file mode 100644
index 000000000..f140939cc
--- /dev/null
+++ b/test-suite/bugs/closed/4844.v
@@ -0,0 +1,47 @@
+
+(* Bug report 4844 (and 4824):
+   The Haskell extraction was erroneously considering [Any] and
+   [()] as convertible ([Tunknown] an [Tdummy] internally). *)
+
+(* A value with inner logical parts.
+   Its extracted type will be [Sum () ()]. *)
+
+Definition semilogic : True + True := inl I.
+
+(* Higher-order record, whose projection [ST] isn't expressible
+   as an Haskell (or OCaml) type. Hence [ST] is extracted as the
+   unknown type [Any] in Haskell. *)
+
+Record SomeType := { ST : Type }.
+
+Definition SomeTrue := {| ST := True |}.
+
+(* A first version of the issue:
+  [abstrSum] is extracted as [Sum Any Any], so an unsafeCoerce
+  is required to cast [semilogic] into [abstrSum SomeTrue]. *)
+
+Definition abstrSum (t : SomeType) := ((ST t) + (ST t))%type.
+
+Definition semilogic' : abstrSum SomeTrue := semilogic.
+
+(* A deeper version of the issue.
+   In the previous example, the extraction could have reduced
+   [abstrSum SomeTrue] into [True+True], solving the issue.
+   It might do so in future versions. But if we put an inductive
+   in the way, a reduction isn't helpful. *)
+
+Inductive box (t : SomeType) := Box : ST t + ST t -> box t.
+
+Definition boxed_semilogic : box SomeTrue :=
+ Box SomeTrue semilogic.
+
+Require Extraction.
+Extraction Language Haskell.
+Recursive Extraction semilogic' boxed_semilogic.
+(* Warning! To fully check that this bug is still closed,
+   you should run ghc on the extracted code:
+
+Extraction "bug4844.hs" semilogic' boxed_semilogic.
+ghc bug4844.hs
+
+*)