title: How to reference type class-polymorphic variables in a theorem type?
body: <p>I have written a Haskell-style <code>Functor</code> type class:</p>
  
  <pre class="lang-coq prettyprint-override"><code>Class Functor (f: Type -&gt; Type) := {
    map {a b: Type}: (a -&gt; b) -&gt; (f a -&gt; f b);
    map_id: forall (a: Type) (x: f a), map id x = x
  }
  </code></pre>
  
  <p>Where <code>id</code> has the obvious definition.</p>
  
  <p>Now, I've proven instances of <code>Functor</code> for <code>list</code> and the function type. But I want to prove statements about <em>any</em> functor. To start with, I want to prove what's essentially a tautology: a restatement of the <code>map_id</code> for any functor.</p>
  
  <pre class="lang-coq prettyprint-override"><code>Theorem map_id_restatement: forall (F: Type -&gt; Type), 
    Functor F -&gt; forall T (x: F T), map id x = x.
  </code></pre>
  
  <p>The idea being to prove this theorem I would simply <code>apply map_id</code>. But I get an error when I try to start proving this:</p>
  
  <pre class="lang-coq prettyprint-override"><code>Toplevel input, characters 88-91:
  Error:
  
  Could not find an instance for "Functor F" in environment:
  
  F : Type -&gt; Type
  T : Type
  x : F T
  </code></pre>
  
  <p>But the <code>Functor F</code> instance should be already in scope due to the assumption in the type. Why is it not recognized?</p>
  
  <p>Edit:</p>
  
  <p>OK, I figured out I could make it work by quantifying the <code>Functor F</code>:</p>
  
  <pre class="lang-coq prettyprint-override"><code>Theorem map_id_restatement: forall (F: Type -&gt; Type) (finst: Functor F),
    forall T (x: F T), map id x = x.
  Proof. apply @map_id. Qed.
  </code></pre>
  
  <p>Why is this necessary? Interestingly, it <em>doesn't</em> work if I don't explicitly give a name to the functor instance (i.e. if I just write <code>(_: Functor F)</code>).</p>