title: Can I check instance presence at runtime?
body: <p>I have a data family of finite vectors:</p>
  
  <pre><code>data family Vec (n :: Nat) e
  data instance Vec 2 Float = Vec2f !Float !Float
  data instance Vec 3 Float = Vec3f !Float !Float !Float
  -- and so on
  </code></pre>
  
  <p>I also have a family of getter functions:</p>
  
  <pre><code>class Get (i :: Nat) (n :: Nat) e where
      get :: Vec n e -&gt; e
  
  instance Get 0 2 Float where
      get (Vec2f x _) = x
  
  instance Get 1 2 Float where
      get (Vec2f _ x) = x
  
  instance Get 0 3 Float where
      get (Vec3f x _ _) = x
  
  instance Get 1 3 Float where
      get (Vec3f _ x _) = x
  
  instance Get 2 3 Float where
      get (Vec3f _ _ x) = x
  -- and so on
  </code></pre>
  
  <p>This way, access to elements of a vector is checked at compile time, so this compiles: </p>
  
  <pre><code>get @0 (Vec2f 0 1)
  </code></pre>
  
  <p>and this doesn't: </p>
  
  <pre><code>get @4 (Vec2f 0 1)
  </code></pre>
  
  <p>Now, I wonder if I can write runtime range check using those functions.
  I tried this:</p>
  
  <pre><code>get' :: forall n e. (KnownNat n) =&gt; Integer -&gt; Vec n e -&gt; Maybe e
  get' i v =
      if i &gt;= 0 &amp;&amp; i &lt; natVal (Proxy :: Proxy n)
          then (flip fmap) (someNatVal i) $ \(SomeNat (Proxy :: Proxy i)) -&gt;
              get @i v -- Could not deduce (Get i n e)
          else Nothing
  </code></pre>
  
  <p>I think I have to check presence of <code>Get i n e</code> instance at runtime, is there a way to do it?</p>