Add GHC-25897

Author: tomjaguarpaw

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

@@ -0,0 +1,34 @@
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module Example1 where
+
+data X = A | B
+
+data F x where
+  FA :: F A
+  FB :: F B
+
+-- Compiles successfully, because the
+-- 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
+  FA -> True
+  FB -> False

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

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

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

@@ -0,0 +1,3 @@
+---
+title: A pattern match, without known return type, on a GADT
+---

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

@@ -0,0 +1,39 @@
+---
+title: GADT pattern match must have a known result type
+summary: A pattern match on a GADT cannot succeed unless GHC knows the result type of the pattern match.
+severity: error
+introduced: 9.6.1
+---
+
+A pattern match on a GADT cannot succeed unless GHC knows the result
+type of the pattern match, for example because the pattern match has a
+type signature, or because the type of the pattern match can be
+inferred from its context.
+
+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
+   |         ^^^^
+```