CODEWITHSUNDEEP
idris
Real John Connor
Real John Connor

Reputation: 445

Why can't dependent types in Idris handle this situation?

I want to do the following:

data Foo : (a : Type) -> (b : Type) -> (c : a -> b -> Type) -> Type where
  Bar : a -> (c a) -> Foo a b c

but I get the following error: 

When checking type of test.Bar:
When checking argument c to test.Foo:
    Type mismatch between
            Type -> Type (Type of c)
    and
            a -> b -> Type (Expected type)

    Specifically:
            Type mismatch between
                    Type
            and
                    b -> Type

This seems like it should be valid to me. That is c has the correct type in the expression Foo a b c, but Idris thinks it has the type b -> Type, or what I think of as (c a).

Am I missing something, or is this a limitation of Idris?

Upvotes: 1

Views: 200

Answers (1)

András Kovács
András Kovács

Reputation: 30103

(c a) has type b -> Type, while all fields of a data constructor must have type Type. It's an error, exactly as Idris says. Your c type constructor takes two arguments but you only applied it to a single a.

Upvotes: 3

Related Questions