Search code examples
proofagda

Agda Unresolved Metas

I have created a Tree datatype. And a get function that should retrieve a value from it. I now want to create a Proof that retrieving any Value from an Empty Tree will return "nothing".

(I emitted the get' and Tree' definitions as I don't think they are relevant. If they are needed I will include them)

    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

Running this code using "agda ./proofs.agda" I always run into

Unsolved metas at the following locations:
  .../src/proofs.agda:12,28-31

pointing to the get of gempty.

As I have used the get function in other parts of my project and there I could use it im assuming that the problem is directly in the proof declaration.

However, I am new to Agda and don't know how to resolve this issue. If you could point me in the right direction to fix my problem that would be much appreciated.

Edit: Minimal Example

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
Solution

  • Agda tells you the unsolved meta is:

    _A_27 : Set

    i.e. it doesn't know what type A is in the application of get. This makes sense as Tree.Empty can be a tree of any type. Therefore you have to pass the type A that you've declared at the start of the type, explicitly, either for the {A} parameter in get or the {A} parameter in Tree.Empty.

    Therefore either of the following works:

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

    or

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