title: Problems in defining an applicative instance
body: <p>Suppose that I'm wanting to define a data-type indexed by two type level environments. Something like:</p>
  
  <pre><code>data Woo s a = Woo a | Waa s a
  
  data Foo (s :: *) (env :: [(Symbol,*)]) (env' :: [(Symbol,*)]) (a :: *) =
       Foo { runFoo :: s -&gt; Sing env -&gt; (Woo s a, Sing env') }
  </code></pre>
  
  <p>The idea is that <code>env</code> is the input environment and <code>env'</code> is the output one. So, type <code>Foo</code> acts like an <a href="https://gist.github.com/pthariensflame/5054294" rel="noreferrer">indexed state monad</a>. So far, so good. My problem is how could I show that <code>Foo</code> is an applicative functor. The obvious try is</p>
  
  <pre><code>instance Applicative (Foo s env env') where
      pure x = Foo (\s env -&gt; (Woo x, env))
      -- definition of (&lt;*&gt;) omitted.
  </code></pre>
  
  <p>but GHC complains that <code>pure</code> is ill-typed since it infers the type </p>
  
  <pre><code>    pure :: a -&gt; Foo s env env a
  </code></pre>
  
  <p>instead of the expected type</p>
  
  <pre><code>    pure :: a -&gt; Foo s env env' a
  </code></pre>
  
  <p>what is completely reasonable. My point is, it is possible to define an <code>Applicative</code> instance for <code>Foo</code> allowing to change the environment type? I googled for <a href="https://www.google.com.br/webhp?hl=pt-BR&amp;sa=X&amp;ved=0ahUKEwjowLqr1KzNAhUGkJAKHZ8aDc0QPAgD#hl=pt-BR&amp;q=indexed%20applicative%20functor" rel="noreferrer">indexed functors</a>, but at first sight, they don't appear to solve my problem. Can someone suggest something to achieve this?</p>