ApplicativeDo: document behaviour with strict patterns (#13875)

Test Plan: unit tests, built docs

Reviewers: dfeuer, bgamari, simonpj, austin, erikd

Subscribers: rwbarton, thomie

GHC Trac Issues: #13875, #13242

Differential Revision: https://phabricator.haskell.org/D3691

5 files changed, 107 insertions, 5 deletions

diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst
index d473841dce..c3a2d69a54 100644
--- a/docs/users_guide/glasgow_exts.rst
+++ b/docs/users_guide/glasgow_exts.rst
@@ -928,6 +928,7 @@ is as follows. If the do-expression has the following form: ::
     do p1 <- E1; ...; pn <- En; return E
 
 where none of the variables defined by ``p1...pn`` are mentioned in ``E1...En``,
+and ``p1...pn`` are all variables or lazy patterns,
 then the expression will only require ``Applicative``. Otherwise, the expression
 will require ``Monad``. The block may return a pure expression ``E`` depending
 upon the results ``p1...pn`` with either ``return`` or ``pure``.
@@ -967,12 +968,47 @@ the optimal solution, provided as an option:
     statements).  The default ``ApplicativeDo`` algorithm is ``O(n^2)``.
 
 
+.. _applicative-do-strict:
+
+Strict patterns
+~~~~~~~~~~~~~~~
+
+
+A strict pattern match in a bind statement prevents
+``ApplicativeDo`` from transforming that statement to use
+``Applicative``.  This is because the transformation would change the
+semantics by making the expression lazier.
+
+For example, this code will require a ``Monad`` constraint::
+
+    > :t \m -> do { (x:xs) <- m; return x }
+    \m -> do { (x:xs) <- m; return x } :: Monad m => m [b] -> m b
+
+but making the pattern match lazy allows it to have a ``Functor`` constraint::
+
+    > :t \m -> do { ~(x:xs) <- m; return x }
+    \m -> do { ~(x:xs) <- m; return x } :: Functor f => f [b] -> f b
+
+A "strict pattern match" is any pattern match that can fail.  For
+example, ``()``, ``(x:xs)``, ``!z``, and ``C x`` are strict patterns,
+but ``x`` and ``~(1,2)`` are not.  For the purposes of
+``ApplicativeDo``, a pattern match against a ``newtype`` constructor
+is considered strict.
+
+When there's a strict pattern match in a sequence of statements,
+``ApplicativeDo`` places a ``>>=`` between that statement and the one
+that follows it.  The sequence may be transformed to use ``<*>``
+elsewhere, but the strict pattern match and the following statement
+will always be connected with ``>>=``, to retain the same strictness
+semantics as the standard do-notation.  If you don't want this, simply
+put a ``~`` on the pattern match to make it lazy.
+
 .. _applicative-do-existential:
 
 Existential patterns and GADTs
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-Note that when the pattern in a statement matches a constructor with
+When the pattern in a statement matches a constructor with
 existential type variables and/or constraints, the transformation that
 ``ApplicativeDo`` performs may mean that the pattern does not scope
 over the statements that follow it.  This is because the rearrangement
@@ -985,7 +1021,8 @@ program does not typecheck::
 
     test = do
       A x <- undefined
-      _ <- return True
+      _ <- return 'a'
+      _ <- return 'b'
       return (x == x)
 
 The reason is that the ``Eq`` constraint that would be brought into
@@ -995,8 +1032,12 @@ rearranged the expression to look like this::
 
     test =
       (\x _ -> x == x)
-        <$> do A x <- undefined; return x
-        <*> return True
+        <$> do A x <- undefined; _ <- return 'a'; return x
+        <*> return 'b'
+
+(Note that the ``return 'a'`` and ``return 'b'`` statements are needed
+to make ``ApplicativeDo`` apply despite the restriction noted in
+:ref:`applicative-do-strict`, because ``A x`` is a strict pattern match.)
 
 Turning off ``ApplicativeDo`` lets the program typecheck.  This is
 something to bear in mind when using ``ApplicativeDo`` in combination
diff --git a/testsuite/tests/ado/T13242.hs b/testsuite/tests/ado/T13242.hs
index ccaa93c087..2111b85baf 100644
--- a/testsuite/tests/ado/T13242.hs
+++ b/testsuite/tests/ado/T13242.hs
@@ -1,6 +1,6 @@
--- Panic.hs
 {-# LANGUAGE ApplicativeDo #-}
 {-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE GADTs #-}
 module T13242 where
 
 import Data.STRef
diff --git a/testsuite/tests/ado/T13242a.hs b/testsuite/tests/ado/T13242a.hs
new file mode 100644
index 0000000000..540b041fed
--- /dev/null
+++ b/testsuite/tests/ado/T13242a.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE ApplicativeDo #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE GADTs #-}
+module T13242a where
+
+data T where A :: forall a . Eq a => a -> T
+
+test :: IO Bool
+test = do
+  A x <- undefined
+  _ <- return 'a'
+  _ <- return 'b'
+  return (x == x)
diff --git a/testsuite/tests/ado/T13242a.stderr b/testsuite/tests/ado/T13242a.stderr
new file mode 100644
index 0000000000..dc4564f168
--- /dev/null
+++ b/testsuite/tests/ado/T13242a.stderr
@@ -0,0 +1,47 @@
+
+T13242a.hs:10:5: error:
+    • Couldn't match expected type ‘a0’ with actual type ‘a’
+        because type variable ‘a’ would escape its scope
+      This (rigid, skolem) type variable is bound by
+        a pattern with constructor: A :: forall a. Eq a => a -> T,
+        in a pattern binding in
+             'do' block
+        at T13242a.hs:10:3-5
+    • In the expression:
+        do A x <- undefined
+           _ <- return 'a'
+           _ <- return 'b'
+           return (x == x)
+      In an equation for ‘test’:
+          test
+            = do A x <- undefined
+                 _ <- return 'a'
+                 _ <- return 'b'
+                 return (x == x)
+    • Relevant bindings include x :: a (bound at T13242a.hs:10:5)
+
+T13242a.hs:13:11: error:
+    • Ambiguous type variable ‘a0’ arising from a use of ‘==’
+      prevents the constraint ‘(Eq a0)’ from being solved.
+      Relevant bindings include x :: a0 (bound at T13242a.hs:10:5)
+      Probable fix: use a type annotation to specify what ‘a0’ should be.
+      These potential instances exist:
+        instance Eq Ordering -- Defined in ‘GHC.Classes’
+        instance Eq Integer
+          -- Defined in ‘integer-gmp-1.0.0.1:GHC.Integer.Type’
+        instance Eq a => Eq (Maybe a) -- Defined in ‘GHC.Base’
+        ...plus 22 others
+        ...plus five instances involving out-of-scope types
+        (use -fprint-potential-instances to see them all)
+    • In a stmt of a 'do' block: return (x == x)
+      In the expression:
+        do A x <- undefined
+           _ <- return 'a'
+           _ <- return 'b'
+           return (x == x)
+      In an equation for ‘test’:
+          test
+            = do A x <- undefined
+                 _ <- return 'a'
+                 _ <- return 'b'
+                 return (x == x)
diff --git a/testsuite/tests/ado/all.T b/testsuite/tests/ado/all.T
index a738c7a6df..bb1cc163d1 100644
--- a/testsuite/tests/ado/all.T
+++ b/testsuite/tests/ado/all.T
@@ -9,4 +9,5 @@ test('T11607', normal, compile_and_run, [''])
 test('ado-optimal', normal, compile_and_run, [''])
 test('T12490', normal, compile, [''])
 test('T13242', normal, compile, [''])
+test('T13242a', normal, compile_fail, [''])
 test('T13875', normal, compile_and_run, [''])