<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 >> 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 !=< 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>