CODEWITHSUNDEEP
equalitydependent-typeidris
Karl
Karl

Reputation: 1153

Proving function evaluates to True in Idris

Edit: I have discovered that if I inline the definition of t1 directly, then this type checks just fine. So it seems that the definition is treating t1 as just an unknown variable and not as my actual earlier definition. Is there some way to force this?

Preface: I fully realize this isn't the idiomatic way to write this. I just want to understand what's happening here specifically.

I have written a trivial implementation of a binary tree and a function elemBT which checks whether a tree contains a particular element and evaluates to a Boolean (think of Haskell's elem function, except for binary trees).

t1 : BT Nat
t1 = Node 5 Nil Nil

elemBT : Eq a => a -> BT a -> Bool

> elemBT 5 t1
True : Bool

Now that I know elemBT evaluates to True, I expect to be able to write a very simple statement which proves that by doing the following.

t1contains5 : elemBT 5 t1 = True
t1contains5 = Refl

Somewhat unexpectedly this results in a unification failure. However, I am able to do nearly the exact same thing using built in lists just fine.

junk : elem 5 [1,5] = True
junk = Refl

And this type checks as expected. Why doesn't my example with binary trees work the same way?

Thanks.

Upvotes: 2

Views: 98

Answers (1)

Karl
Karl

Reputation: 1153

I have resolved this myself. It turns out that sometime relatively recently (perhaps late 2015) a change was made to Idris which treats any lowercase, potentially implicit variable as implicit. If I capitalize T1, then this problem goes away completely.

There is some further discussion in the Github repository here

Upvotes: 4

Related Questions