GADT pattern match must have a known result type [GHC-25897]

A pattern match on a GADT cannot succeed unless GHC knows the result type of the pattern match. This information might, for example, be derived from a type 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.

A related situation where this error can arise is when binding a GADT constructor with a let binding; see the second example.

Examples

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
   |

Example1.hs

Before

{-# 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
foo = \case
  FA -> True
  FB -> False

After

{-# 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'.
foo :: F x -> Bool
foo = \case
  FA -> True
  FB -> False

Example2.hs

Before

{-# 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

After

{-# 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'
foo :: F x -> G x
foo = \case
  FA -> True
  FB -> False

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.

Note: if the TypeFamilies extension is active, 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
  |                  ^

Let.hs

Before

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)

After

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)