search

agda / agda

Agda is a dependently typed programming language / interactive theorem prover.
https://wiki.portal.chalmers.se/agda/pmwiki.php
Other
2.41k stars 339 forks source link

Sort metas produce ill-typed reflected terms when quoted #7187

Closed UlfNorell closed 3 months ago

UlfNorell commented 3 months ago 
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.

UlfNorell commented 3 months ago

Culprit is this (introduced in 9d6a6540aa4 by @jespercockx) https://github.com/agda/agda/blob/d6e0844c2d686e5bc25c3edeeb9dd4aa92be0b3e/src/full/Agda/TypeChecking/Quote.hs#L182 which builds a Term instead of a Sort.

My proposed fix is to return unsupportedSort instead. The alternative is to add a meta constructor to reflected sorts.