title: Polymorphic constant in a dependent type signature?
body: <p>Say I'd like to define a type of a proof that some vector has a certain sum. I'd also like that proof to work for any <code>Monoid</code> type <code>t</code>. My first attempt was this:</p>
  
  <pre><code>data HasSum : Monoid t =&gt; t -&gt; Vect n t -&gt; Type where
      EndNeutral : Monoid t =&gt; HasSum Prelude.Algebra.neutral []
      Component : Monoid t =&gt; (x : t) -&gt; HasSum sum xs -&gt; HasSum (x &lt;+&gt; sum) (x :: xs)
  </code></pre>
  
  <p>Unfortunately, the compiler argues it <code>Can't find implementation for Monoid t</code>. So I tried with an implicit argument so that I can specify its type:</p>
  
  <pre><code>    EndNeutral : Monoid t =&gt; {Prelude.Algebra.neutral : t} -&gt; HasSum Prelude.Algebra.neutral []
  </code></pre>
  
  <p>This compiles, but this does not:</p>
  
  <pre><code>x : HasSum 0 []
  x = EndNeutral
  </code></pre>
  
  <p>strangely claiming that it <code>Can't find implementation for Monoid Integer</code>.</p>
  
  <p>My final attempt was to define a helper constant with capital letter name so that Idris doesn't confuse it for a bound variable:</p>
  
  <pre><code>ZERO : Monoid t =&gt; t
  ZERO = neutral
  
  data HasSum : Monoid t =&gt; t -&gt; Vect n t -&gt; Type where
      EndNeutral : Monoid t =&gt; HasSum ZERO []
      Component : Monoid t =&gt; {rem : t} -&gt; (x : t) -&gt; HasSum rem xs -&gt; HasSum (x &lt;+&gt; rem) (x :: xs)
  </code></pre>
  
  <p>but now it can't guess the type of <code>ZERO</code> in the definition of <code>EndNeutral</code> (<code>Can't find implementation for Monoid t</code>). So I tried again with an implicit binding:</p>
  
  <pre><code>    EndNeutral : Monoid t =&gt; {ZERO : t} -&gt; HasSum ZERO []
  </code></pre>
  
  <p>but now <code>ZERO</code> becomes a bound variable and although it compiles, it does not work as expected, because it allows to construct a proof of empty vectory having an arbitrary sum.</p>
  
  <p>At this point I ran out of ideas. Does anyone know how to express a polymorphic constant in an Idris type?</p>