Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Showing content from https://github.com/agda/agda/issues/7187 below:

Sort metas produce ill-typed reflected terms when quoted · Issue #7187 · agda/agda · GitHub

open import Agda.Builtin.Reflection renaming (bindTC to _>>=_)
open import Agda.Builtin.Unit
open import Agda.Builtin.Nat
open import Agda.Builtin.List

macro
  `Nat : Term → TC ⊤
  `Nat hole = do
    ty ← inferType hole
    _  ← debugPrint "tactic" 10 (termErr ty ∷ [])
    unify hole (def (quote Nat) [])

boom : `Nat
boom = 1

We hit the impossible on line 462 in Unquote.hs trying to unquote (the Term) meta _13 [] as a sort. Meta 13 is the type of the hole we are trying to fill, and a sort meta.

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4