diff --git a/message-index/messages/GHC-25897/example2/after/Let.hs b/message-index/messages/GHC-25897/example2/after/Let.hs
new file mode 100644
index 00000000..d7cb5397
--- /dev/null
+++ b/message-index/messages/GHC-25897/example2/after/Let.hs
@@ -0,0 +1,12 @@
+module Main where
+
+data Showable where
+  MkShowable :: Show a => a -> Showable
+
+showShowable :: Showable -> String
+showShowable showable =
+  case showable of
+    MkShowable x -> show x
+
+main :: IO ()
+main = putStrLn $ showShowable (MkShowable 42)
diff --git a/message-index/messages/GHC-25897/example2/before/Let.hs b/message-index/messages/GHC-25897/example2/before/Let.hs
new file mode 100644
index 00000000..d977d31a
--- /dev/null
+++ b/message-index/messages/GHC-25897/example2/before/Let.hs
@@ -0,0 +1,12 @@
+module Main where
+
+data Showable where
+  MkShowable :: Show a => a -> Showable
+
+showShowable :: Showable -> String
+showShowable showable =
+  let MkShowable x = showable
+  in show x
+
+main :: IO ()
+main = putStrLn $ showShowable (MkShowable 42)
diff --git a/message-index/messages/GHC-25897/example2/index.md b/message-index/messages/GHC-25897/example2/index.md
new file mode 100644
index 00000000..da9297b1
--- /dev/null
+++ b/message-index/messages/GHC-25897/example2/index.md
@@ -0,0 +1,32 @@
+---
+title: Binding a `GADT` constructor in `let`
+---
+
+In this example, we use a `let` binding to unpack the constructor of a GADT. Naively, this should work fine, because there is only one constructor. Yet GHC does not accept this code!
+
+The fix is to use pattern-matching, either with a `case` or by pattern-matching in a function argument.
+
+For more details about why this is necessary, see the [GHC user guide on ExistentialQuantification](https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/existential_quantification.html#restrictions).
+
+Note: if the `TypeFamilies` extension is active, [GHC-46956](/messages/GHC-46956) is generated instead.
+
+## Message
+
+```
+Let.hs:8:18: error: [GHC-25897]
+    • Couldn't match expected type ‘p’ with actual type ‘a’
+      ‘a’ is a rigid type variable bound by
+        a pattern with constructor:
+          MkShowable :: forall a. Show a => a -> Showable,
+        in a pattern binding
+        at Let.hs:8:7-18
+      ‘p’ is a rigid type variable bound by
+        the inferred type of x :: p
+        at Let.hs:8:7-29
+    • In the pattern: MkShowable x
+      In a pattern binding: MkShowable x = showable
+      In the expression: let MkShowable x = showable in show x
+  |
+8 |   let MkShowable x = showable
+  |                  ^
+```
diff --git a/message-index/messages/GHC-25897/index.md b/message-index/messages/GHC-25897/index.md
index ed787744..6bfedab3 100644
--- a/message-index/messages/GHC-25897/index.md
+++ b/message-index/messages/GHC-25897/index.md
@@ -11,3 +11,6 @@ signature, or by type inference due to the context in which the pattern match oc
 
 To solve the problem you must somehow tell GHC the type of the pattern
 match.
+
+A related situation where this error can arise is when binding a GADT constructor with
+a `let` binding; see the second example.
diff --git a/message-index/messages/GHC-46956/example2/after/Let.hs b/message-index/messages/GHC-46956/example2/after/Let.hs
new file mode 100644
index 00000000..e09af76d
--- /dev/null
+++ b/message-index/messages/GHC-46956/example2/after/Let.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE TypeFamilies #-}
+module Main where
+
+data Showable where
+  MkShowable :: Show a => a -> Showable
+
+showShowable :: Showable -> String
+showShowable showable =
+  case showable of
+    MkShowable x -> show x
+
+main :: IO ()
+main = putStrLn $ showShowable (MkShowable 42)
diff --git a/message-index/messages/GHC-46956/example2/before/Let.hs b/message-index/messages/GHC-46956/example2/before/Let.hs
new file mode 100644
index 00000000..f5963d08
--- /dev/null
+++ b/message-index/messages/GHC-46956/example2/before/Let.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE TypeFamilies #-}
+module Main where
+
+data Showable where
+  MkShowable :: Show a => a -> Showable
+
+showShowable :: Showable -> String
+showShowable showable =
+  let MkShowable x = showable
+  in show x
+
+main :: IO ()
+main = putStrLn $ showShowable (MkShowable 42)
diff --git a/message-index/messages/GHC-46956/example2/index.md b/message-index/messages/GHC-46956/example2/index.md
new file mode 100644
index 00000000..3d89e2d2
--- /dev/null
+++ b/message-index/messages/GHC-46956/example2/index.md
@@ -0,0 +1,30 @@
+---
+title: Binding a `GADT` constructor in `let`
+---
+
+In this example, we use a `let` binding to unpack the constructor of a GADT. Naively, this should work fine, because there is only one constructor. Yet GHC does not accept this code!
+
+The fix is to use pattern-matching, either with a `case` or by pattern-matching in a function argument.
+
+For more details about why this is necessary, see the [GHC user guide on ExistentialQuantification](https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/existential_quantification.html#restrictions).
+
+Note: this example generates GHC-46956 because the `TypeFamilies` extension is active. If it isn't, [GHC-25897](/messages/GHC-25897) is generated instead.
+
+## Message
+
+```
+Let.hs:9:18: error: [GHC-46956]
+    • 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:
+          MkShowable :: forall a. Show a => a -> Showable,
+        in a pattern binding
+        at Let.hs:9:7-18
+    • In the pattern: MkShowable x
+      In a pattern binding: MkShowable x = showable
+      In the expression: let MkShowable x = showable in show x
+  |
+9 |   let MkShowable x = showable
+  |                  ^
+```
diff --git a/message-index/messages/GHC-46956/index.md b/message-index/messages/GHC-46956/index.md
index 19da4856..9611d281 100644
--- a/message-index/messages/GHC-46956/index.md
+++ b/message-index/messages/GHC-46956/index.md
@@ -6,3 +6,7 @@ severity: error
 ---
 
 This error occurs during kind inference. When inferring a kind for a type variable, GHC creates a fresh metavariable to stand for the kind. Later, if something forces this kind metavariable to be equal to some other kind, unification equates them. However, local kind quantification can lead to the existence of kinds that are only valid in the scope of the quantifier. If a kind metavariable that originated outside this scope were unified with the locally-bound kind, then the resulting program would contain an ill-scoped kind signature.
+
+This situation can arise for multiple reasons.
+- In the first example, the cause is a manually-specified type signature with the kind variable in the wrong position.
+- In the second example, the cause is a pattern match on a GADT constructor in a `let` binding (use `case` instead).