我不明白为什么这段代码应该传递类型检查:
foo :: (Maybe a, Maybe b)
foo = let x = Nothing in (x,x)
由于每个组件都绑定到同一个变量x,我希望这个表达式最通用的类型(Maybe a, Maybe a).如果我使用a where而不是a,我会得到相同的结果let.我错过了什么吗？
我正在从Coq提取到Haskell,需要在Haskell端导入几个模块.是否有任何Coq提取功能允许您自动执行此操作？我知道我可以写一个脚本来做这件事,但我宁愿不必重新发明轮子.