title: Type Juggling with Existentials at Runtime
body: <p>I'm playing around with existentials and GADTs in Haskell, and I'm trying to define a DSL for combinators (such as SKI). I have the GADT working, as well as a reduction function which works fine (and isn't really relevant to the question)</p>
  
  <pre><code>{-# LANGUAGE GADTs, ExistentialQuantification #-}
  
  import Control.Applicative
  import Data.Monoid
  import Control.Monad
  
  data Comb t where
      S :: Comb ((a -&gt; b -&gt; c) -&gt; (a -&gt; b) -&gt; a -&gt; c)
      K :: Comb (a -&gt; b -&gt; a)
      I :: Comb (a -&gt; a)
      B :: Comb ((b -&gt; c) -&gt; (a -&gt; b) -&gt; a -&gt; c)
      C :: Comb ((b -&gt; a -&gt; c) -&gt; a -&gt; b -&gt; c)
      W :: Comb ((a -&gt; a -&gt; b) -&gt; a -&gt; b)
      (:$) :: Comb (a -&gt; b) -&gt; Comb a -&gt; Comb b
  </code></pre>
  
  <p>What I'm trying to do now is define a way to read combinator strings in from the user at runtime. Obviously, I need an existential type to do this, since the GADT's type information needs to be hidden.</p>
  
  <pre><code>data CombBox = forall a. CombBox { unCombBox :: Comb a }
  
  ($$) :: CombBox -&gt; CombBox -&gt; Maybe CombBox
  x $$ y = undefined -- ???
  </code></pre>
  
  <p>I would like the <code>($$)</code> function to somehow "look inside" the <code>CombBox</code> existentials at runtime and, if it is possible to combine the two combinators using <code>:$</code> and get a well-typed result, I would like the result to be that. Otherwise, I want <code>Nothing</code>. So, for example,</p>
  
  <pre><code>CombBox S $$ CombBox K ==&gt; Just (CombBox (S :$ K))
  CombBox W $$ CombBox I ==&gt; Nothing
  </code></pre>
  
  <p>The latter should fail because <code>W</code> expects a 2-ary function where <code>I</code> takes one argument. But I would like to relegate this check to the runtime, and I'm not sure if such a thing is possible in the Haskell (+ GHC extensions) type system.</p>