用这个表达式：
putStrLn $ show $ tryMe (Just 2) 25
我们已经掌握了这些起始信息：
putStrLn :: String -> IO ()
show :: Show a => a -> String
tryMe :: Maybe Int -> Int -> Int
Just :: b -> Maybe b
2 :: Num c => c
25 :: Num d => d
（我在各处都使用了不同的类型变量，因此我们可以更轻松地在同一范围内同时考虑它们）
类型检查器的工作基本上是为所有这些变量找到要选择的类型，然后确保参数和结果类型对齐，并且所有必需的类型类实例都存在。
在这里我们可以看到应用于两个参数的tryMe 将是Int，因此a（用作show 的输入）必须是Int。这要求有一个Show Int 实例；确实有，所以我们完成了a。
同样tryMe 想要一个Maybe Int，我们有应用Just 的结果。所以b必须是Int，而我们使用Just是Int -> Maybe Int。
Just 已应用于2 :: Num c => c。我们决定它必须应用于Int，所以c 必须是Int。如果我们有Num Int，我们可以这样做，并且我们这样做了，所以c 被处理了。
剩下25 :: Num d => d。它用作tryMe 的第二个参数，它期望Int，所以d 必须是Int（再次解除Num 约束）。
然后我们只需要确保所有参数和结果类型对齐，这很明显。这主要是对上述内容的重新散列，因为我们通过选择类型变量的唯一可能值使它们排列在一起，所以我不会详细讨论。
现在，这有什么不同？
putStrLn $ show $ doIt (Just 2) 25
好吧，让我们再看一遍：
putStrLn :: String -> IO ()
show :: Show a => a -> String
doIt :: Test t => TT t -> t -> t
Just :: b -> Maybe b
2 :: Num c => c
25 :: Num d => d
show 的输入是将doIt 应用于两个参数的结果，所以它是t。所以我们知道a 和t 是同一类型，这意味着我们需要Show t，但我们还不知道t 是什么，所以我们必须回到那个。
应用Just 的结果在我们想要TT t 的地方使用。所以我们知道Maybe b 必须是TT t，因此Just :: _b -> TT t。我使用 GHC 的 partial type signature syntax 编写了 _b，因为这个 _b 不像我们之前的 b。当我们有Just :: b -> Maybe b 时，我们可以为b 选择我们喜欢的任何类型，而Just 可以具有该类型。但是现在我们需要一些特定但未知的类型_b，这样TT t 就是Maybe _b。我们还没有足够的信息来知道该类型是什么，因为在不知道t 的情况下，我们不知道我们正在使用哪个实例对TT t 的定义。
Just 的参数是2 :: Num c => c。所以我们可以知道c 也必须是_b，这也意味着我们将需要一个Num _b 实例。但由于我们不知道_b 是什么，所以我们无法检查是否存在Num 实例。我们稍后再讨论。
最后25 :: Num d => d 用于doIt 想要t 的地方。好的，所以d 也是t，我们需要一个Num t 实例。同样，我们仍然不知道t 是什么，所以我们无法检查。
总之，我们已经想通了：
putStrLn :: String -> IO ()
show :: t -> String
doIt :: TT t -> t -> t
Just :: _b -> TT t
2 :: _b
25 :: t
还有这些限制有待解决：
Test t, Num t, Num _b, Show t, (Maybe _b) ~ (TT t)
（如果你以前没见过，~ 是我们写的两个类型表达式必须是同一事物的约束）
我们被困住了。我们在这里无法进一步了解，因此 GHC 将报告类型错误。您引用的特定错误消息抱怨我们无法判断TT t 和Maybe _b 是相同的（它调用类型变量a0 和a1），因为我们没有足够的信息来选择它们的具体类型（它们是模棱两可的）。
如果我们为表达式的某些部分添加一些额外的类型签名，我们可以更进一步。添加25 :: Int1 立即让我们读出t 是Int。现在我们可以到达某个地方了！让我们将其修补到我们尚未解决的约束中：
Test Int, Num Int, Num _b, Show Int, (Maybe _b) ~ (TT Int)
Num Int 和Show Int 是显而易见的并且是内置的。我们也有Test Int，这给了我们TT Int = Maybe Int 的定义。所以(Maybe _b) ~ (Maybe Int)，因此_b 也是Int，这也允许我们解除Num _b 约束（又是Num Int）。同样，现在很容易验证所有参数和结果类型是否匹配，因为我们已将所有类型变量填充到具体类型。
但是为什么你的其他尝试没有成功？让我们尽可能回到没有额外类型注释的情况：
putStrLn :: String -> IO ()
show :: t -> String
doIt :: TT t -> t -> t
Just :: _b -> TT t
2 :: _b
25 :: t
还需要解决这些限制：
Test t, Num t, Num _b, Show t, (Maybe _b) ~ (TT t)
然后添加Just 2 :: Maybe Int。因为我们知道这也是Maybe _b 和TT t，这告诉我们_b 是Int。我们现在也知道我们正在寻找一个给我们TT t = Maybe Int 的Test 实例。但这实际上并不能确定t 是什么！也可能有：
instance Test Double where
type TT Double = Maybe Int
doIt (Just a) _ = fromIntegral a
doIt Nothing b = b
现在可以选择t 作为Int 或Double；两者都可以与您的代码一起正常工作（因为25 也可以是Double），但会打印不同的东西！
很容易抱怨因为t 只有一个实例，而TT t = Maybe Int 我们应该选择那个实例。但是实例选择逻辑被定义为不以这种方式猜测。如果您处于可能应该存在另一个匹配实例的情况，但由于代码中的错误而不存在（例如，忘记导入定义它的模块），然后它不会提交它可以看到的唯一匹配实例。只有当它知道没有其他实例可能适用时，它才会选择一个实例。2
所以“只有一个实例TT t = Maybe Int”的论点并没有让 GHC 向后工作以解决 t 可能是 Int。
一般而言，对于类型族，您只能“向前工作”；如果您知道要应用类型族的类型，则可以从中看出结果类型应该是什么，但是如果您知道结果类型，则不能识别输入类型。这常常令人惊讶，因为普通类型构造函数确实让我们以这种方式“逆向工作”；我们使用上面的这个从Maybe _b = Maybe Int 得出_b = Int 的结论。这只适用于新的data 声明，应用类型构造函数总是保留结果类型中的参数类型（例如，当我们将Maybe 应用到Int 时，结果类型是Maybe Int）。相同的逻辑不适用于类型族，因为可能有多个类型族实例映射到同一个类型，即使没有要求存在可识别的模式将结果类型中的某些内容连接到输入类型（我可以有type TT Char = Maybe (Int -> Double, Bool)。
所以你经常会发现，当你需要添加一个类型注解时，你会经常发现在一个类型是一个类型族的结果的地方添加一个是行不通的，你需要而是将输入固定到类型族（或其他需要与其相同的类型）。
1 请注意，您在问题main = putStrLn $ show $ doIt (Just 2) 25::Int 中引用的行实际上不起作用。 :: Int 签名绑定“尽可能远”，因此您实际上声称整个表达式 putStrLn $ show $ doIt (Just 2) 25 是 Int 类型，而它必须是 IO () 类型。我假设当你真正检查它时，你在25 :: Int 周围加上括号，所以putStrLn $ show $ doIt (Just 2) (25 :: Int)。
2 对于 GHC 认为不可能有任何其他匹配实例的“某些知识”有特定的规则。我不会详细讨论它们，但基本上当你有instance Constraints a => SomeClass (T a) 时，它必须能够仅通过考虑SomeClass (T a) 位来明确选择一个实例；它无法查看=> 箭头左侧的约束。