Search code examples
idris

Type constructor with no parameters causing "Can't infer argument" error

I defined a type like this:

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

In Haskell, an empty MyList can be instantiated with Empty, but Idris complains:

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

Why is that?

Solution

  • :set showimplicits in the REPL helps when debugging error messages:

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

    As you can see, the type constructor has an argument and it can't infer it. If you call a function (like Empty is one), Idris tries to infer values for all implicit arguments. If a can be inferred from the context, for example by using the (MyList Nat) Empty, it works.

    If you are explicit about the argument, it works too (and you can see a distinction between Haskell and 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 is explicit, while in Haskell the unbound type parameter is hidden: Empty :: MyList a.