在Haskell中使用GADTs返回多态类型

采用以下代码:

{-# LANGUAGE DataKinds, GADTs #-}


module Lib where

import System.Random as Randy

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

data Kind a where
  IntK :: Int -> Kind Int
  StringK :: String -> Kind String
  BoolK :: Bool -> Kind Bool
  OtherK :: a -> Kind a


instance Show (Kind a) where
  show (IntK n)    = "KindInt " ++ show n
  show (StringK s) = "KindString " ++ s
  show (BoolK b)   = "KindBool " ++ show b


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

这段代码不会编译,基本上是因为编译器不喜欢 pure $ IntK n 指定 Kind Int 由第一行返回,但 StringK 和 BoolK 由最后四行返回:

• Couldn't match type ‘[Char]’ with ‘Int’
  Expected type: IO (Kind Int)    
    Actual type: IO (Kind String)                               
• In the expression: pure $ StringK (show n)

我觉得这很奇怪。我可以不用GADTs轻松做到这一点,只需使用普通 data 公告但我认为像GADTs这样的增强不会降低类型系统的灵活性,而是会增加它的灵活性。我做错什么了吗?我只是遇到了这个扩展,所以我可能误解了什么。如何使用GADTs编译程序?