[Agda] Reflection: blockOnMeta after commitTC can cause a type error

[Martin Stone Davis]

|`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?

```
open import Prelude
open import Tactic.Reflection

macro
   test-inferFunRange : Tactic
   test-inferFunRange hole = do
     goal ← inferFunRange hole -|
     typeError ( strErr "inferFunRange succeeded" ∷ termErr goal ∷ [] )

bar : Nat
bar = 0

record R (A : Set) : Set₁ where
   field
     F : A → Set

   foo : (x : A) → F x → Set
   foo = case bar of (λ _ → test-inferFunRange {!!})
   {- Error:
        A → Set !=< Set of type Set₁
        when checking that the expression F has type Set
   -}
```

P.s. With apologies, this is crossposted here 
<https://github.com/UlfNorell/agda-prelude/issues/43>.
|
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160927/72fdec4a/attachment.html