不能从 f x = f₁ y 推导出 f = f₁？答案

【问题标题】：Can't deduce f = f₁ from f x = f₁ y?不能从 f x = f₁ y 推导出 f = f₁？
【发布时间】：2014-04-22 20:09:24
【问题描述】：

{-# LANGUAGE GADTs #-}

data Foo x y where
  Composition :: Foo b c -> Foo a b -> Foo a c
  FMap :: Functor f => (a->b) -> Foo (f a) (f b)

asFunction :: Foo a b -> a->b
asFunction (FMap m) = fmap m
-- asFunction (Composition (FMap m) (FMap n)) = fmap m . fmap n
asFunction (Composition m n) = asFunction m . asFunction n

这按预期工作...直到您取消注释 asFunction 的第二个子句！这实际上只是其他两种模式已经匹配的特殊情况的内联版本，所以我希望它没问题。但是（ghc-7.6.2，或者ghc-7.4.1）

Could not deduce (f ~ f1)
from the context (b1 ~ f a1, b ~ f b2, Functor f)
  bound by a pattern with constructor
             FMap :: forall (f :: * -> *) a b.
                     Functor f =>
                     (a -> b) -> Foo (f a) (f b),
           in an equation for \`asFunction'
  ...

为什么会发生这种情况，为什么在其他子句中不？在更复杂的应用程序中究竟应该做些什么来防止这种麻烦？

【问题讨论】：

它在 7.8.2 中工作......显然在 7.6 和 7.8 之间引入了一些东西来解决这个问题。
@bheklilr 也许是this 功能重新引入？
@Ørjan：好像是这样。做出这样的回答？
好的，我这样做了，详细说明一下。

标签： haskell typechecking gadt unification

【解决方案1】：

这可能与为了支持更灵活（“不饱和”）的类型函数而暂时从 GHC 的类型推断系统中删除的一个特性强制的左/右分解有关，然后是 @987654321 @。

【讨论】：