HaskellExtr: Add type annotations to Prelude.==

Also `Export ExtrHaskellBasic` in `ExtrHaskellString`.

Fixes #12257
Fixes #12258

5 files changed, 145 insertions, 6 deletions

diff --git a/doc/changelog/10-standard-library/12263-fix-haskell-extraction.rst b/doc/changelog/10-standard-library/12263-fix-haskell-extraction.rst
new file mode 100644
index 0000000000..c80a070181
--- /dev/null
+++ b/doc/changelog/10-standard-library/12263-fix-haskell-extraction.rst
@@ -0,0 +1,9 @@
+- **Fixed:**
+  In Haskell extraction with ``ExtrHaskellString``, equality comparisons on
+  strings and characters are now guaranteed to be uniquely well-typed, even in
+  very polymorphic contexts under ``unsafeCoerce``; this is achieved by adding
+  type annotations to the extracted code, and by making ``ExtrHaskellString``
+  export ``ExtrHaskellBasic`` (`#12263
+  <https://github.com/coq/coq/pull/12263>`_, fixes `#12257
+  <https://github.com/coq/coq/issues/12257>`_ and `#12258
+  <https://github.com/coq/coq/issues/12258>`_, by Jason Gross).
diff --git a/test-suite/bugs/closed/bug_12257.v b/test-suite/bugs/closed/bug_12257.v
new file mode 100644
index 0000000000..4962048a42
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12257.v
@@ -0,0 +1,3 @@
+(* Test that ExtrHaskellString transitively requires ExtrHaskellBasic *)
+Require Coq.extraction.ExtrHaskellString.
+Import Coq.extraction.ExtrHaskellBasic.
diff --git a/test-suite/output/Extraction_Haskell_String_12258.out b/test-suite/output/Extraction_Haskell_String_12258.out
new file mode 100644
index 0000000000..615abaa3e8
--- /dev/null
+++ b/test-suite/output/Extraction_Haskell_String_12258.out
@@ -0,0 +1,73 @@
+{-# OPTIONS_GHC -cpp -XMagicHash #-}
+{- For Hugs, use the option -F"cpp -P -traditional" -}
+
+{- IMPORTANT: If you change this file, make sure that running [cp
+   Extraction_Haskell_String_12258.out Extraction_Haskell_String_12258.hs &&
+   ghc -o test Extraction_Haskell_String_12258.hs] succeeds -}
+
+module Main where
+
+import qualified Prelude
+
+#ifdef __GLASGOW_HASKELL__
+import qualified GHC.Base
+#else
+-- HUGS
+import qualified IOExts
+#endif
+
+#ifdef __GLASGOW_HASKELL__
+unsafeCoerce :: a -> b
+unsafeCoerce = GHC.Base.unsafeCoerce#
+#else
+-- HUGS
+unsafeCoerce :: a -> b
+unsafeCoerce = IOExts.unsafeCoerce
+#endif
+
+#ifdef __GLASGOW_HASKELL__
+type Any = GHC.Base.Any
+#else
+-- HUGS
+type Any = ()
+#endif
+
+data Output_type_code =
+   Ascii_dec
+ | Ascii_eqb
+ | String_dec
+ | String_eqb
+ | Byte_eqb
+ | Byte_eq_dec
+
+type Output_type = Any
+
+output :: Output_type_code -> Output_type
+output c =
+  case c of {
+   Ascii_dec ->
+    unsafeCoerce
+      ((Prelude.==) :: Prelude.Char -> Prelude.Char -> Prelude.Bool);
+   Ascii_eqb ->
+    unsafeCoerce
+      ((Prelude.==) :: Prelude.Char -> Prelude.Char -> Prelude.Bool);
+   String_dec ->
+    unsafeCoerce
+      ((Prelude.==) :: Prelude.String -> Prelude.String -> Prelude.Bool);
+   String_eqb ->
+    unsafeCoerce
+      ((Prelude.==) :: Prelude.String -> Prelude.String -> Prelude.Bool);
+   Byte_eqb ->
+    unsafeCoerce
+      ((Prelude.==) :: Prelude.Char -> Prelude.Char -> Prelude.Bool);
+   Byte_eq_dec ->
+    unsafeCoerce
+      ((Prelude.==) :: Prelude.Char -> Prelude.Char -> Prelude.Bool)}
+
+type Coq__IO a = GHC.Base.IO a
+
+main :: GHC.Base.IO ()
+main =
+   ((Prelude.>>=) (GHC.Base.return output) (\_ -> GHC.Base.return ()))
+
+
diff --git a/test-suite/output/Extraction_Haskell_String_12258.v b/test-suite/output/Extraction_Haskell_String_12258.v
new file mode 100644
index 0000000000..063ff64337
--- /dev/null
+++ b/test-suite/output/Extraction_Haskell_String_12258.v
@@ -0,0 +1,52 @@
+Require Import Coq.extraction.Extraction.
+Require Import Coq.extraction.ExtrHaskellString.
+Extraction Language Haskell.
+Set Extraction File Comment "IMPORTANT: If you change this file, make sure that running [cp Extraction_Haskell_String_12258.out Extraction_Haskell_String_12258.hs && ghc -o test Extraction_Haskell_String_12258.hs] succeeds".
+Inductive output_type_code :=
+| ascii_dec
+| ascii_eqb
+| string_dec
+| string_eqb
+| byte_eqb
+| byte_eq_dec
+.
+
+Definition output_type_sig (c : output_type_code) : { T : Type & T }
+  := existT (fun T => T)
+            _
+            match c return match c with ascii_dec => _ | _ => _ end with
+            | ascii_dec => Ascii.ascii_dec
+            | ascii_eqb => Ascii.eqb
+            | string_dec => String.string_dec
+            | string_eqb => String.eqb
+            | byte_eqb => Byte.eqb
+            | byte_eq_dec => Byte.byte_eq_dec
+            end.
+
+Definition output_type (c : output_type_code)
+  := Eval cbv [output_type_sig projT1 projT2] in
+      projT1 (output_type_sig c).
+Definition output (c : output_type_code) : output_type c
+  := Eval cbv [output_type_sig projT1 projT2] in
+      match c return output_type c with
+      | ascii_dec as c
+      | _ as c
+        => projT2 (output_type_sig c)
+      end.
+
+Axiom IO_unit : Set.
+Axiom _IO : Set -> Set.
+Axiom _IO_bind : forall {A B}, _IO A -> (A -> _IO B) -> _IO B.
+Axiom _IO_return : forall {A : Set}, A -> _IO A.
+Axiom cast_io : _IO unit -> IO_unit.
+Extract Constant _IO "a" => "GHC.Base.IO a".
+Extract Inlined Constant _IO_bind => "(Prelude.>>=)".
+Extract Inlined Constant _IO_return => "GHC.Base.return".
+Extract Inlined Constant IO_unit => "GHC.Base.IO ()".
+Extract Inlined Constant cast_io => "".
+
+Definition main : IO_unit
+  := cast_io (_IO_bind (_IO_return output)
+                       (fun _ => _IO_return tt)).
+
+Recursive Extraction main.
diff --git a/theories/extraction/ExtrHaskellString.v b/theories/extraction/ExtrHaskellString.v
index 8c61f4e96b..80f527f51b 100644
--- a/theories/extraction/ExtrHaskellString.v
+++ b/theories/extraction/ExtrHaskellString.v
@@ -8,6 +8,8 @@ Require Import Ascii.
 Require Import String.
 Require Import Coq.Strings.Byte.
 
+Require Export ExtrHaskellBasic.
+
 (**
  * At the moment, Coq's extraction has no way to add extra import
  * statements to the extracted Haskell code.  You will have to
@@ -35,19 +37,19 @@ Extract Inductive ascii => "Prelude.Char"
               (Data.Bits.testBit (Data.Char.ord a) 5)
               (Data.Bits.testBit (Data.Char.ord a) 6)
               (Data.Bits.testBit (Data.Char.ord a) 7))".
-Extract Inlined Constant Ascii.ascii_dec => "(Prelude.==)".
-Extract Inlined Constant Ascii.eqb => "(Prelude.==)".
+Extract Inlined Constant Ascii.ascii_dec => "((Prelude.==) :: Prelude.Char -> Prelude.Char -> Prelude.Bool)".
+Extract Inlined Constant Ascii.eqb => "((Prelude.==) :: Prelude.Char -> Prelude.Char -> Prelude.Bool)".
 
 Extract Inductive string => "Prelude.String" [ "([])" "(:)" ].
-Extract Inlined Constant String.string_dec => "(Prelude.==)".
-Extract Inlined Constant String.eqb => "(Prelude.==)".
+Extract Inlined Constant String.string_dec => "((Prelude.==) :: Prelude.String -> Prelude.String -> Prelude.Bool)".
+Extract Inlined Constant String.eqb => "((Prelude.==) :: Prelude.String -> Prelude.String -> Prelude.Bool)".
 
 (* python -c 'print(" ".join(r""" "%s" """.strip() % (r"'"'\''"'" if chr(i) == "'"'"'" else repr(""" "" """.strip()) if chr(i) == """ " """.strip() else repr(chr(i))) for i in range(256)))' # " to satisfy Coq's comment parser *)
 Extract Inductive byte => "Prelude.Char"
 ["'\x00'" "'\x01'" "'\x02'" "'\x03'" "'\x04'" "'\x05'" "'\x06'" "'\x07'" "'\x08'" "'\t'" "'\n'" "'\x0b'" "'\x0c'" "'\r'" "'\x0e'" "'\x0f'" "'\x10'" "'\x11'" "'\x12'" "'\x13'" "'\x14'" "'\x15'" "'\x16'" "'\x17'" "'\x18'" "'\x19'" "'\x1a'" "'\x1b'" "'\x1c'" "'\x1d'" "'\x1e'" "'\x1f'" "' '" "'!'" "'""'" "'#'" "'$'" "'%'" "'&'" "'\''" "'('" "')'" "'*'" "'+'" "','" "'-'" "'.'" "'/'" "'0'" "'1'" "'2'" "'3'" "'4'" "'5'" "'6'" "'7'" "'8'" "'9'" "':'" "';'" "'<'" "'='" "'>'" "'?'" "'@'" "'A'" "'B'" "'C'" "'D'" "'E'" "'F'" "'G'" "'H'" "'I'" "'J'" "'K'" "'L'" "'M'" "'N'" "'O'" "'P'" "'Q'" "'R'" "'S'" "'T'" "'U'" "'V'" "'W'" "'X'" "'Y'" "'Z'" "'['" "'\\'" "']'" "'^'" "'_'" "'`'" "'a'" "'b'" "'c'" "'d'" "'e'" "'f'" "'g'" "'h'" "'i'" "'j'" "'k'" "'l'" "'m'" "'n'" "'o'" "'p'" "'q'" "'r'" "'s'" "'t'" "'u'" "'v'" "'w'" "'x'" "'y'" "'z'" "'{'" "'|'" "'}'" "'~'" "'\x7f'" "'\x80'" "'\x81'" "'\x82'" "'\x83'" "'\x84'" "'\x85'" "'\x86'" "'\x87'" "'\x88'" "'\x89'" "'\x8a'" "'\x8b'" "'\x8c'" "'\x8d'" "'\x8e'" "'\x8f'" "'\x90'" "'\x91'" "'\x92'" "'\x93'" "'\x94'" "'\x95'" "'\x96'" "'\x97'" "'\x98'" "'\x99'" "'\x9a'" "'\x9b'" "'\x9c'" "'\x9d'" "'\x9e'" "'\x9f'" "'\xa0'" "'\xa1'" "'\xa2'" "'\xa3'" "'\xa4'" "'\xa5'" "'\xa6'" "'\xa7'" "'\xa8'" "'\xa9'" "'\xaa'" "'\xab'" "'\xac'" "'\xad'" "'\xae'" "'\xaf'" "'\xb0'" "'\xb1'" "'\xb2'" "'\xb3'" "'\xb4'" "'\xb5'" "'\xb6'" "'\xb7'" "'\xb8'" "'\xb9'" "'\xba'" "'\xbb'" "'\xbc'" "'\xbd'" "'\xbe'" "'\xbf'" "'\xc0'" "'\xc1'" "'\xc2'" "'\xc3'" "'\xc4'" "'\xc5'" "'\xc6'" "'\xc7'" "'\xc8'" "'\xc9'" "'\xca'" "'\xcb'" "'\xcc'" "'\xcd'" "'\xce'" "'\xcf'" "'\xd0'" "'\xd1'" "'\xd2'" "'\xd3'" "'\xd4'" "'\xd5'" "'\xd6'" "'\xd7'" "'\xd8'" "'\xd9'" "'\xda'" "'\xdb'" "'\xdc'" "'\xdd'" "'\xde'" "'\xdf'" "'\xe0'" "'\xe1'" "'\xe2'" "'\xe3'" "'\xe4'" "'\xe5'" "'\xe6'" "'\xe7'" "'\xe8'" "'\xe9'" "'\xea'" "'\xeb'" "'\xec'" "'\xed'" "'\xee'" "'\xef'" "'\xf0'" "'\xf1'" "'\xf2'" "'\xf3'" "'\xf4'" "'\xf5'" "'\xf6'" "'\xf7'" "'\xf8'" "'\xf9'" "'\xfa'" "'\xfb'" "'\xfc'" "'\xfd'" "'\xfe'" "'\xff'"].
 
-Extract Inlined Constant Byte.eqb => "(Prelude.==)".
-Extract Inlined Constant Byte.byte_eq_dec => "(Prelude.==)".
+Extract Inlined Constant Byte.eqb => "((Prelude.==) :: Prelude.Char -> Prelude.Char -> Prelude.Bool)".
+Extract Inlined Constant Byte.byte_eq_dec => "((Prelude.==) :: Prelude.Char -> Prelude.Char -> Prelude.Bool)".
 Extract Inlined Constant Ascii.ascii_of_byte => "(\x -> x)".
 Extract Inlined Constant Ascii.byte_of_ascii => "(\x -> x)".