对普通代数数据类型的模式匹配（不管它是否在GADT语法中定义）只将 * 值信息 * 注入主体。GADT上的模式匹配也可以注入 * 类型信息 *。
比如说，

data NonGADT a where
  Agnostic :: a -> NonGADT a

data GADT a where
  IntSpecific :: Int -> GADT Int
  CharSpecific :: Char -> GADT Char

所有这些构造函数在某种意义上都有相同的签名a -> □ADT a，所以当编译器对涉及模式匹配的函数进行类型检查时，编译器需要先验地使用它。

extractNonGADT :: NonGADT a -> a
extractNonGADT v = case v of
   Agnostic x -> x

extractGADT :: GADT a -> a
extractGADT v = case v of
   IntSpecific x -> x
   CharSpecific x -> x

不同之处在于，extractGADT可以利用内部类型实际上被限制为单个类型的事实，来执行以下操作：

extractGADT' :: GADT a -> a
extractGADT' v = case v of
   IntSpecific x -> x + 5
   CharSpecific x -> toUpper x

一个标准的Hindley-Milner编译器将无法处理这个问题：假设a在整个定义中处处相同。实际上，从技术上讲，它在GHC中也到处都是一样的，只是代码的某些部分在作用域中分别有额外的约束a ~ Int或a ~ Char。但是仅仅添加处理是不够的：必须不允许该附加信息逸出该范围（因为它将不为真），并且这需要额外的检查。

不同之处在于返回类型的多态性。如果它是完全多态的，您可以使用语法，但是任何专门化都需要GADT语法。举例来说：

Foo :: Int -> Bar a b c

因为a、b和c都是不同的类型变量，所以这适合GADTSyntax扩展。但是如果你要写这些代码，你需要GADTs：

Foo :: Int -> Bar Int b c
Foo :: Int -> Bar a b b
Foo :: Eq a => Int -> Bar a b c
-- (actually, ExistentialQuantification is enough for this last one, but GADTs also works)

使用像这样的花哨类型，我们失去了术语具有主类型的属性。您仍然可以使用标准类型推断，但有时它将不得不做出任意选择，这可能导致类型错误，即使一切都是类型安全的;为了避免这种情况，GHC简单地拒绝做出那些任意的选择，并尽可能早地报告错误。