键入构造函数，没有参数导致“无法推断参数”错误

Question

我定义了这样的类型：

data MyList a = Empty | Cons a (MyList a)

在Haskell中，一个空的MyList可以用Empty实例化，但Idris抱怨：

> Empty
(input):Can't infer argument a to Empty

这是为什么？

Answer 1

REPL中的:set showimplicits在调试错误消息时有帮助：

>:set showimplicits
>:t Empty
Main.Empty : {a : Type} -> Main.MyList a

如您所见，类型构造函数有一个参数，它无法推断它。如果你调用一个函数（比如Empty就是一个函数），Idris会尝试推断所有隐式参数的值。如果a可以从上下文中推断出来，例如使用the (MyList Nat) Empty，它就有效。

如果你明确这个论点，它也有效（你可以看到Haskell和Idris之间的区别）：

data MyList : Type -> Type where
  Empty : (a : Type) -> MyList a
  Cons : (a : Type) -> (x : a) -> MyList a -> MyList a

>Empty
Empty : (a : Type) -> MyList a

Idris的a是显式的，而在Haskell中，未绑定的类型参数是隐藏的：Empty :: MyList a。