title: In Idris, can I prove free theorems, e.g. the only (total) function of type `forall t. t -> t` is `id`?
body: <p>For sufficiently polymorphic types, parametricity can uniquely determine the function itself (see <a href="http://www.cs.sfu.ca/CourseCentral/831/burton/Notes/July14/free.pdf" rel="nofollow noreferrer">Wadler's <em>Theorems for free!</em></a> for details). For example, the only total function with type <code>forall t. t -&gt; t</code> is the identity function <code>id</code>.</p>
  
  <p>Is it possible to state and prove this in Idris? (And if it can't be proven inside Idris, is it true anyway?)</p>
  
  <p>The following is my attempt (I know that function equality is not a primitive concept in Idris, so I assert that any function of generic type <code>t -&gt; t</code> always returns the same result as the identity function would return):</p>
  
  <pre><code>%default total
  
  GenericEndomorphism: Type
  GenericEndomorphism = (t: Type) -&gt; (t -&gt; t)
  
  id_is_an_example : GenericEndomorphism
  id_is_an_example t = id
  
  id_is_the_only_example : (f : GenericEndomorphism) -&gt; (t : Type) -&gt; (x : t) -&gt; f t x = x
  id_is_the_only_example f t x = ?id_is_the_only_example_rhs
  </code></pre>
  
  <p>The resulting hole is:</p>
  
  <pre><code>- + Main.id_is_the_only_example_rhs [P]
   `--                                f : GenericEndomorphism
                                      t : Type
                                      x : t
       -------------------------------------------------------
        Main.id_is_the_only_example_rhs : f t x = x
  </code></pre>