Agda中空树get操作返回nothing的证明遇未解决元变量问题

我定义了Tree数据类型和用于获取值的get函数，想要编写证明验证从空树中获取任意值均返回nothing。

最初的核心代码如下（省略get'与Tree'定义）：

data Tree (A : Set) : Set where 
        Empty : Tree A
        Nodes : Tree' A -> Tree A 

get : {A : Set} -> Positive -> Tree A -> Maybe A
get _ Empty = nothing
get p (Nodes n) = get' p n

data Positive : Set where 
        xH : Positive
        xI : Positive -> Positive
        xO : Positive -> Positive

gempty : (p : Positive) -> get p Tree.Empty ≡ nothing
gempty p = refl

运行agda ./proofs.agda时，始终遇到未解决元变量错误，错误指向gempty中的get位置。我在项目其他模块中可正常使用get函数，推测问题直接出在证明声明中。

以下是完整最小可复现示例：

open import Data.Maybe
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; cong-app)
open Eq.≡-Reasoning

data Tree' (A : Set) : Set where 
        node001 : Tree' A -> Tree' A

data Tree (A : Set) : Set where 
        Empty : Tree A
        Nodes : Tree' A -> Tree A 

data Positive : Set where 
    xH : Positive
    xI : Positive -> Positive
    xO : Positive -> Positive

get' : {A : Set} -> Positive -> Tree' A -> Maybe A 
get' xH (node001 _ ) = nothing
get' (xO q) (node001 _ )= nothing
get' (xI q) (node001 r )= get' q r

get : {A : Set} -> Positive -> Tree A -> Maybe A
get _ Empty = nothing
get p (Nodes n) = get' p n


gempty : {A : Set} -> ∀ (p : Positive) -> get p Tree.Empty ≡ nothing
gempty p = refl

解决方向 #

问题出在gempty的类型声明中：get p Tree.Empty里的Tree.Empty没有指定类型参数A，Agda无法推断出这个空树对应的类型，从而产生未解决元变量。

修正方法有两种：

1. 显式指定类型参数：
   在Tree.Empty后加上{A}，明确它属于Tree A类型：

   gempty : {A : Set} -> ∀ (p : Positive) -> get p (Tree.Empty {A}) ≡ nothing
   gempty p = refl
   

2. 让Agda通过上下文推断：
   把Tree.Empty写成Empty，利用get的类型参数上下文来推断A：

   gempty : {A : Set} -> ∀ (p : Positive) -> get p Empty ≡ nothing
   gempty p = refl
   

两种方法都能让Agda正确解析类型，消除未解决元变量错误，refl也能正常通过类型检查——因为get _ Empty的定义就是返回nothing，两者在定义上直接相等。

内容的提问来源于stack exchange，提问作者Max Podpera