Haskell中使用GADTs返回多态类型的编译问题及解决

Great question—this is a super common gotcha when you're first learning to use GADTs! Let's break down what's going wrong and how to adjust your code to work as expected.

The Core Problem #

First, let's look at the signature of your dataKinds function:

dataKinds :: IO (Kind a)

This tells the compiler that dataKinds returns an IO action producing a Kind a for some fixed type a. But in your case expression, you're returning different variants of Kind that correspond to distinct a types:

• IntK n maps to Kind Int
• StringK (show n) maps to Kind String
• BoolK True/False maps to Kind Bool

The compiler throws an error because it expects all branches to return the same fixed Kind a type, not a mix of incompatible type family members.

Compare this to a regular ADT (without GADTs): if you had written something like:

data Kind = IntK Int | StringK String | BoolK Bool

This works because there's no type parameter a—each constructor belongs to the same unified Kind type. Your GADT, however, defines Kind a as a family of types where each constructor locks in a specific a.

The Fix: Use an Existential Type Wrapper #

To make your code compile, we need to capture the idea that we have a Kind a for some unknown type a, not a fixed one. We can do this with an existential type wrapper:

1. First, define a new type that wraps any Kind a (we add a Show constraint since we want to print the value later):

data SomeKind where
  SomeKind :: Show (Kind a) => Kind a -> SomeKind

This type says: "There exists some type a where we have a Kind a that can be shown."

2. Update dataKinds to return IO SomeKind instead of IO (Kind a), and wrap each branch's result in SomeKind:

dataKinds :: IO SomeKind
dataKinds = Randy.getStdRandom (Randy.randomR (1,6)) >>= \n -> case n of
  1 -> pure $ SomeKind $ IntK n
  2 -> pure $ SomeKind $ IntK n
  3 -> pure $ SomeKind $ StringK (show n)
  4 -> pure $ SomeKind $ StringK (show n)
  5 -> pure $ SomeKind $ BoolK True
  6 -> pure $ SomeKind $ BoolK False

3. Adjust someFunc to unpack the SomeKind wrapper and print the underlying Kind a:

someFunc :: IO ()
someFunc = dataKinds >>= \(SomeKind k) -> putStrLn (show k)

Why This Works #

The SomeKind wrapper hides the specific a type from the compiler when we're dealing with the value generically (like printing it). But when you do need to handle specific Kind variants (e.g., write a function that only works with Kind Int), GADTs still give you precise type safety—you can pattern match on IntK and know you're dealing with an Int without runtime type checks.

GADTs don't weaken type system flexibility—they let you be more precise about types when you need to, while existential wrappers let you handle cases where you don't care about the specific type, just that it meets certain constraints.

内容的提问来源于stack exchange，提问作者James Hamilton