<html>
  <head>

    <meta http-equiv="content-type" content="text/html; charset=utf-8">
  </head>
  <body bgcolor="#FFFFFF" text="#000000">
    <div class="comment-body markdown-body markdown-format
      js-comment-body"><code>`inferFunRange` is failing in the code
        below, where I expected Agda to report "inferFunRange succeeded
        (x : A) → F x → Set". I traced the cause back to the call to
        `blockOnMeta! x`, which runs `commitTC &gt;&gt; blockOnMeta x`.
        This looks like a bug to me but I don't know enough about Agda
        to say for sure. Would someone please explain why this is
        happening?<br>
        <br>
        ```<br>
        open import Prelude<br>
        open import Tactic.Reflection<br>
        <br>
        macro<br>
          test-inferFunRange : Tactic<br>
          test-inferFunRange hole = do<br>
            goal ← inferFunRange hole -|<br>
            typeError ( strErr "inferFunRange succeeded" ∷ termErr goal
        ∷ [] )<br>
        <br>
        bar : Nat<br>
        bar = 0<br>
        <br>
        record R (A : Set) : Set₁ where<br>
          field<br>
            F : A → Set<br>
        <br>
          foo : (x : A) → F x → Set<br>
          foo = case bar of (λ _ → test-inferFunRange {!!})<br>
          {- Error:<br>
               A → Set !=&lt; Set of type Set₁<br>
               when checking that the expression F has type Set<br>
          -}<br>
        ```<br>
        <br>
        P.s. With apologies, this is crossposted <a
          href="https://github.com/UlfNorell/agda-prelude/issues/43">here</a>.<br>
      </code></div>
  </body>
</html>