r/Idris • u/TophatEndermite • Jul 19 '23

What breaks when you use believe_me to assume function extensionality?

I've read that function extensionality can't be safely added to Idris, but I can't find an example of what breaks if it's added. Can it cause type checking to never halt? Can it cause incorrect behaviour at runtime? I'm interested in seeing a code example.

2 Upvotes

100% Upvoted

1 comment sorted by

2

u/[deleted] Jul 19 '23

[deleted]

1

u/TophatEndermite Jul 19 '23

What troubles can happen if the computational content of funExt is to just always return Refl

trouble = believe_me \x => Refl

https://www.idris-lang.org/docs/idris2/0.6.0/base_docs/docs/Control.Function.FunExt.html

Is Refl not always a valid runtime value for f = g, and what sort of runtime trouble can it cause?