# The --without-K option generates unsolved metas #1775

Closed
opened this Issue Jan 13, 2016 · 6 comments

Projects
None yet
2 participants
Member

### asr commented Jan 13, 2016

 This issue was found while using the `--without-K` option on the standard library. Only the `Data/Fin/Dec.agda` file has this issue. The B.agda file: ```module B where data Bool : Set where true : Bool false : Bool data ℕ : Set where zero : ℕ suc : (n : ℕ) → ℕ data Fin : ℕ → Set where zero : {n : ℕ} → Fin (suc n) suc : {n : ℕ} (i : Fin n) → Fin (suc n) infixr 5 _∷_ data Vec {a} (A : Set a) : ℕ → Set a where [] : Vec A zero _∷_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (suc n) infix 4 _[_]=_ data _[_]=_ {a} {A : Set a} : {n : ℕ} → Vec A n → Fin n → A → Set a where here : ∀ {n} {x} {xs : Vec A n} → x ∷ xs [ zero ]= x there : ∀ {n} {i} {x y} {xs : Vec A n} (xs[i]=x : xs [ i ]= x) → y ∷ xs [ suc i ]= x Subset : ℕ → Set Subset = Vec Bool infix 4 _∈_ _∈_ : ∀ {n} → Fin n → Subset n → Set x ∈ p = p [ x ]= true drop-there : ∀ {s n x} {p : Subset n} → suc x ∈ s ∷ p → x ∈ p drop-there (there x∈p) = x∈p``` The A.agda file: ```{-# OPTIONS --without-K #-} module A where open import B _∘_ : ∀ {a b c} {A : Set a} {B : A → Set b} {C : {x : A} → B x → Set c} → (∀ {x} (y : B x) → C y) → (g : (x : A) → B x) → ((x : A) → C (g x)) f ∘ g = λ x → f (g x) data ⊥ : Set where infix 3 ¬_ ¬_ : ∀ {ℓ} → Set ℓ → Set ℓ ¬ P = P → ⊥ data Dec {p} (P : Set p) : Set p where yes : ( p : P) → Dec P no : (¬p : ¬ P) → Dec P infix 4 _∈?_ _∈?_ : ∀ {n} x (p : Subset n) → Dec (x ∈ p) zero ∈? true ∷ p = yes here zero ∈? false ∷ p = no λ() suc n ∈? s ∷ p with n ∈? p ... | yes n∈p = yes (there n∈p) ... | no n∉p = no (n∉p ∘ drop-there)``` The issue: ```\$ agda A.agda Checking A (/tmp/A.agda). Checking B (/tmp/B.agda). Finished B. Finished A. Unsolved metas at the following locations: /tmp/A.agda:28,26-27``` I had used the `--without-K` option on the standard library without problems some time ago.

Contributor

### jespercockx commented Jan 13, 2016

 This is due to the new unifier that's still missing a feature to generalize the datatype over the datatype indices when applying injectivity. Specifically, the unifier gets stuck on the following unification problem ``````new unifyState: UnifyState variable tel: {.n : ℕ} (p₁ : Vec Bool .n) {xs : Vec Bool .n} flexible vars: [0, 1, 2] equation tel: (_ : Vec Bool (suc .n₁)) equations: true ∷ xs =?= false ∷ p₁ `````` The unifier needs to generalize the equation over the index `(suc .n₁)`, but I haven't implemented this yet. I was secretly hoping this feature wouldn't be necessary in most cases, but here you found a nice motivating example for implementing it. I have the theory for it (mostly) worked out, so I'll see if I can get it to work.

Contributor

### jespercockx commented Jan 13, 2016

 Another example of this problem occurs when you enable --without-K on test/Succeed/Issue291.agda. You get an unsolved meta: `Is empty: Val .s (π₁ ∙ .M) [ at /home/jesper/agda/test/Succeed/Issue291.agda:41,8-10 ]`
Member

### asr commented Jan 13, 2016

 Good to know you are testing the new unifier :-)

Member

### asr commented Feb 13, 2016

 Removed the `bug` label. The `regression` label is enough.

Member

### asr commented Feb 16, 2016

 Removed the `bug` label. The `regression` label is enough. Please ignore this comment.

Closed

### jespercockx added a commit to jespercockx/agda that referenced this issue Jun 23, 2016

``` [ agda#1775 ] Added test case ```
``` 11025f0 ```

### jespercockx added a commit to jespercockx/agda that referenced this issue Jun 23, 2016

``` [ agda#1775 ] Added another test case ```
``` 8531f38 ```

### jespercockx added a commit to jespercockx/agda that referenced this issue Jun 23, 2016

``` [ agda#1775 ] Added test case ```
``` b993d8a ```

### jespercockx added a commit to jespercockx/agda that referenced this issue Jun 23, 2016

``` [ agda#1775 ] Added another test case ```
``` bc2bf7e ```

Closed

Merged

Contributor

### jespercockx commented Jul 5, 2016

 Fixed by 7b73c1c