Make suggested example changes

Author: david-christiansen

message-index/messages/GHC-25897/example1/after/Example1.hs

@@ -15,20 +15,7 @@ data F x where
 -- result type of the pattern match
 -- is known, from the type signature,
 -- to be 'Bool'.
-foo2 :: F x -> Bool
-foo2 = \case
-  FA -> True
-  FB -> False
-
-type family G a where
-  G A = Bool
-  G B = Bool
-
--- Compiles successfully, because the
--- result type of the pattern match
--- is known, from the type signature,
--- to be 'G x'
-foo3 :: F x -> G x
-foo3 = \case
+foo :: F x -> Bool
+foo = \case
   FA -> True
   FB -> False

message-index/messages/GHC-25897/example1/after/Example2.hs

@@ -0,0 +1,25 @@
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module Example2 where
+
+data X = A | B
+
+data F x where
+  FA :: F A
+  FB :: F B
+
+type family G a where
+  G A = Bool
+  G B = Bool
+
+-- Compiles successfully, because the
+-- result type of the pattern match
+-- is known, from the type signature,
+-- to be 'G x'
+foo3 :: F x -> G x
+foo3 = \case
+  FA -> True
+  FB -> False

message-index/messages/GHC-25897/example1/before/Example1.hs

@@ -12,6 +12,6 @@ data F x where
   FB :: F B
 
 -- Results in error GHC-25897
-foo1 = \case
+foo = \case
   FA -> True
   FB -> False

message-index/messages/GHC-25897/example1/before/Example2.hs

@@ -0,0 +1,17 @@
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module Example2 where
+
+data X = A | B
+
+data F x where
+  FA :: F A
+  FB :: F B
+
+-- Results in error GHC-25897
+foo = \case
+  FA -> True
+  FB -> False

message-index/messages/GHC-25897/example1/index.md

@@ -1,3 +1,35 @@
 ---
 title: A pattern match, without known return type, on a GADT
 ---
+
+In this example, the definition `foo` uses pattern matching on a GADT. GHC is not able to infer types for GADT pattern matches, but no type signature is provided. Following the suggestion in the error message and adding a type signature solves the problem.
+
+Both starting files in this example are identical, but they are matched with different solutions. `Example2.hs` demonstrates that GHC's expected type need not be a concrete base type - even a type family satisfies this check.
+
+## Message
+
+The following message is provided for both lines 16 and 17, because GHC type checks each branch of a pattern match separately:
+
+```
+Example1.hs:16:9: error:
+    • Could not deduce (p ~ Bool)
+      from the context: x ~ 'A
+        bound by a pattern with constructor: FA :: F 'A,
+                 in a \case alternative
+        at Example1.hs:16:3-4
+      ‘p’ is a rigid type variable bound by
+        the inferred type of foo :: F x -> p
+        at Example1.hs:(15,1)-(17,13)
+    • In the expression: True
+      In a \case alternative: FA -> True
+      In the expression:
+        \case
+          FA -> True
+          FB -> False
+    • Relevant bindings include
+        foo :: F x -> p (bound at Example1.hs:15:1)
+    Suggested fix: Consider giving ‘foo’ a type signature
+   |
+16 |   FA -> True
+   |   
+```

message-index/messages/GHC-25897/index.md

@@ -10,29 +10,4 @@ type of the pattern match. This information might, for example, be derived from
 signature, or by type inference due to the context in which the pattern match occurs.
 
 To solve the problem you must somehow tell GHC the type of the pattern
-match.  For example, in the below error message GHC suggests giving
-the pattern match a type signature.
-
-```
-example1.hs:14:9: error: [GHC-25897]
-    • Could not deduce ‘p ~ Bool’
-      from the context: x ~ A
-        bound by a pattern with constructor: FA :: F A,
-                 in a \case alternative
-        at test17.hs:14:3-4
-      ‘p’ is a rigid type variable bound by
-        the inferred type of foo1 :: F x -> p
-        at test17.hs:(13,1)-(15,13)
-    • In the expression: True
-      In a \case alternative: FA -> True
-      In the expression:
-        \case
-          FA -> True
-          FB -> False
-    • Relevant bindings include
-        foo1 :: F x -> p (bound at test17.hs:13:1)
-    Suggested fix: Consider giving ‘foo1’ a type signature
-   |
-14 |   FA -> True
-   |         ^^^^
-```
+match.