Why is this mutually recursive data definition not total and how can I fix it?

Question

I am experimenting with Idris a lot lately and came up with the following "type level definition of a set":

mutual
  data Set : Type -> Type where
    Empty : Set a
    Insert : (x : a) -> (xs : Set a) -> Not (Elem x xs) -> Set a

  data Elem : (x : a) -> Set a -> Type where
    Here : Elem x (Insert x xs p)
    There : Elem x xs -> Elem x (Insert y xs p)

So a set is either empty or it consists of a set and an additional element that is proven not to be in that set already.

When I totality check this, I get the error

[...] is not strictly positive

for Insert, Here and There. I have been searching the documentation for terms like "strictly positive" and the totality checker in general, but I cannot figure out why this case in particular is not total (or strictly positive). Can somebody explain this?

The natural next question then is of course how to "fix" it. Can I somehow change the definition, keeping its semantics, so that it totality checks?

Since I don't really need the definition to look like this (it is only an experiment after all) it would also be interesting to know whether there is another, somehow more idiomatic way to represent Sets at the type level that is total.

Cactus Cactus · Accepted Answer · 2016-07-21T19:58:07

This SO post explains what strictly positive types are and why they matter. In your case, since Not (Elem x xs) simply means a function Elem x xs -> Void, this is where the "type being defined occurring on the left-hand side of an arrow" comes from.

Can you make do with something like this?

mutual
  data Set : Type -> Type where
    Empty : Set a
    Insert : (x : a) -> (xs : Set a) -> NotElem x xs -> Set a

  data NotElem : (x : a) -> Set a -> Type where
    NotInEmpty : NotElem x Empty
    NotInInsert : Not (x = y) -> NotElem x ys -> NotElem x (Insert y ys p)

Why is this mutually recursive data definition not total and how can I fix it?

1 Answers