Conversion reports an error even though a suitable meta instantiation could solve the constraint.

[UlfNorell]

From k...@cas.mcmaster.ca on May 19, 2012 22:14:25

What's the problem? Cut-and-pasted program examples are preferred over attachments (if reasonably short). The file exhibiting the problem is Data/SUList/ListSetMap/FinRel/Utils.lagda in the attachment (everything there has been cut down to at least close to the minimum).

It contains, as only hole, {! p₁ !} in the last line. Agsy accepts this, but the whole file does not type-check afterwards.

The interesting thing is that, if you turn sucKeys₀ and from-∈-sucKeys into postulates (commenting out their implementation), everything typechecks. What version of Agda are you using? On what operating system (if relevant)? The current development version of Agda on linux (gentoo). (I observed the problem first in 2.3.0, but have not tried the cut-down version again with Agda-2.3.0.)

Wolfram

Attachment: 2012-05_Agsy_inconsistency.tar.gz

Original issue: http://code.google.com/p/agda/issues/detail?id=651

[UlfNorell]

From k...@cas.mcmaster.ca on May 19, 2012 13:18:17

SUList'' stands forsorted unique list''; their parameterised implementation is used to implement

• non-empty sets in ListSet1,
• possibly empty sets in ListSet,
• relations as ListSet1-valued maps in ListSetMap. FinRel specialises this to elements taken from Fin types.

[UlfNorell]

From k...@cas.mcmaster.ca on May 19, 2012 13:38:14

I get it to type-check by introducing a local module parameterised over the two postulates. I guess that really proves that there is a problem...

private module From-∈-tabulate′ (sucKeys₀ : {n q : ℕ} {m : Maybe (Fin n)} → RawMap (ρ n) (ρ q) m → RawMap (ρ (suc n)) (ρ q) (sucM m)) (from-∈-sucKeys : {n q : ℕ} {a₀ : Fin n} {b₀ : Fin q} {es : LSM (ρ n) (ρ q)} → (Fin.suc a₀ , b₀) ∈ ( , sucKeys₀ {n} {q} (proj₂ es)) → (a₀ , b₀) ∈ es) where sucKeys′ : {n q : ℕ} → LSM (ρ n) (ρ q) → LSM (ρ (suc n)) (ρ q) sucKeys′ ( , s) = _ , sucKeys₀ s

tabulate′ : {n q : ℕ} → (Fin n → ListSet1.ListSet₁ (ρ q)) → LSM (ρ n) (ρ q)
tabulate′ {zero} {q} _ = emptyLSM  (ρ zero) (ρ q)
tabulate′ {suc m} {q} f = let p = tabulate′ {m} {q} (f ∘ Fin.suc)
               in  cons< (ρ (suc m)) (ρ q) Fin.zero (f Fin.zero) (sucKeys′ p) (zero<M {m} {proj₁ p})

from-∈-tabulate′  :  {n q : ℕ} {f : Fin n → ListSet1.ListSet₁ (ρ q)} {a₀ : Fin n} {b₀ : Fin q}
                  → (a₀ , b₀) ∈ tabulate′ f → ListSet1._∈_ (ρ q) b₀ (f a₀)
from-∈-tabulate′ {zero} {q} {f} {()} _
from-∈-tabulate′ {suc n} {q} {f} {Fin.zero} (∈head ._ .≡-refl _ ._ ._ , b₀∈Ta₀) = b₀∈Ta₀
from-∈-tabulate′ {suc zero} {q} {f} {Fin.zero} (∈tail ._ .≡-refl .tt () , b₀∈Ta₀)
from-∈-tabulate′ {suc zero} {q} {f} {suc ()} _
from-∈-tabulate′ {suc (suc n)} {q} {f} {Fin.zero} (∈tail ._ ._ ._ 0∈T′ , b₀∈Ta₀) =  ⊥-elim  (Map.<not∈′ (ρ (suc (suc n))) (ρ q) (s≤s z≤n) _ 0∈T′)
from-∈-tabulate′ {suc (suc n)} {q} {f} {suc a₁} (∈head ._ ._ () ._ ._ , b₀∈Ta₀)
from-∈-tabulate′ {suc (suc n)} {q} {f} {suc a₁} {b₀} (∈tail ._ ._ ._ a₀∈T′ , b₀∈Ta₀)
     = from-∈-tabulate′ {suc n} {q} {f ∘ Fin.suc} {a₁} p₂
  where
    p₁ : (Fin.suc a₁ , b₀) ∈ sucKeys′ {suc n} {q} (tabulate′ {suc n} {q} (f ∘ Fin.suc))
    p₁ = a₀∈T′ , b₀∈Ta₀
    p₂ : (a₁ , b₀) ∈ tabulate′ {suc n} {q} (f ∘ Fin.suc)
    p₂ = from-∈-sucKeys {suc n} {q} {a₁} {b₀} p₁ 

open From-∈-tabulate′ sucKeys₀ from-∈-sucKeys using (tabulate′ ; from-∈-tabulate′)

[UlfNorell]

From nils.anders.danielsson on May 21, 2012 05:27:57

If you want us to investigate this issue, please provide us with a small example.

The interesting thing is that, if you turn sucKeys₀ and from-∈-sucKeys into postulates (commenting out their implementation), everything typechecks.

I get it to type-check by introducing a local module parameterised over the two postulates. I guess that really proves that there is a problem...

No. If you turn a function into a postulate or parameter, then some constraints can become easier to solve.

Agsy accepts this, but the whole file does not type-check afterwards.

This sounds suspicious, though.

Status: InfoNeeded
Owner: freli...@gmail.com

[UlfNorell]

From andreas....@gmail.com on October 02, 2012 08:34:08

The title was a bit confusing, since it has nothing to do with Agsy (C-c C-a). It is a simple give (C-c C-SPC) that accepts the term.

Summary: "Give" accepts a term that does not type-check afterwards.
Owner: andreas....@gmail.com
Labels: Type-Defect Priority-High Interaction

[UlfNorell]

From andreas....@gmail.com on October 02, 2012 08:48:43

Well, if you give the last hidden argument, {t}, to p2, then it type-checks.

where t = tabulate′ {suc n} {q} (f ∘ Fin.suc) p₁ : (Fin.suc a₁ , b₀) ∈ sucKeys {suc n} {q} (tabulate′ {suc n} {q} (f ∘ Fin.suc)) p₁ = a₀∈T′ , b₀∈Ta₀ p₂ : (a₁ , b₀) ∈ tabulate′ {suc n} {q} (f ∘ Fin.suc) p₂ = from-∈-sucKeys {suc n} {q} {a₁} {b₀} {t} p₁

The thing is, when we have a meta instead of p1, then reduction of from-eps-sucKeys is blocked. Some how this allows Agda to solve for the unknown {t}. If p1 is supplied, then it fails to solve for {t}, which remains as a meta, leading to an error.

This is of course inconsistent behavior. Reporting an error is unsound. It should report unsolved constraints, since one side is blocked by a meta.

Summary: Conversion reports an error even though a suitable meta instantiation could solve the constraint.
Status: Accepted
Labels: -Priority-High -Interaction Priority-Medium Conversion