{"action":"created","issue":{"url":"https://api.github.com/repos/agda/agda/issues/2097","repository_url":"https://api.github.com/repos/agda/agda","labels_url":"https://api.github.com/repos/agda/agda/issues/2097/labels{/name}","comments_url":"https://api.github.com/repos/agda/agda/issues/2097/comments","events_url":"https://api.github.com/repos/agda/agda/issues/2097/events","html_url":"https://github.com/agda/agda/issues/2097","id":165167852,"number":2097,"title":"Suboptimal size solver suggestions","user":{"login":"mietek","id":166207,"avatar_url":"https://avatars.githubusercontent.com/u/166207?v=3","gravatar_id":"","url":"https://api.github.com/users/mietek","html_url":"https://github.com/mietek","followers_url":"https://api.github.com/users/mietek/followers","following_url":"https://api.github.com/users/mietek/following{/other_user}","gists_url":"https://api.github.com/users/mietek/gists{/gist_id}","starred_url":"https://api.github.com/users/mietek/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mietek/subscriptions","organizations_url":"https://api.github.com/users/mietek/orgs","repos_url":"https://api.github.com/users/mietek/repos","events_url":"https://api.github.com/users/mietek/events{/privacy}","received_events_url":"https://api.github.com/users/mietek/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":1,"created_at":"2016-07-12T20:05:46Z","updated_at":"2016-07-13T16:54:45Z","closed_at":null,"body":"Agda’s suggestions with regard to sizes are surprisingly poor, and optimising the sizes by hand gets old really fast.\r\n\r\nHere are some examples:\r\n\r\nFunction | Suggested size\r\n--------- | ---------------\r\n`cont` | `↑ (↑ ((↑ (↑ (↑ (↑ ω)))) ⊔ˢ (↑ (↑ m))))`\r\n`exch` | `↑ (↑ (↑ ((↑ (↑ (↑ (↑ (↑ ω))))) ⊔ˢ (↑ (↑ m)))))`\r\n`comp` | `↑ (↑ ((↑ ((↑ (↑ (↑ (↑ (↑ ω))))) ⊔ˢ (↑ m))) ⊔ˢ (↑ n)))`\r\n\r\nAfter removing some parentheses for readability:\r\n\r\nFunction | Suggested size | Optimal size\r\n--------- | --------------- | ------------\r\n`cont` | `↑ ↑ ((↑ ↑ ↑ ↑ ω) ⊔ˢ (↑ ↑ m))` | `↑ ↑ ↑ ↑ ↑ ↑ m`\r\n`exch` | `↑ ↑ ↑ ((↑ ↑ ↑ ↑ ↑ ω) ⊔ˢ (↑ ↑ m))` | `↑ ↑ ↑ ↑ ↑ ↑ ↑ ↑ m`\r\n`comp` | `↑ ↑ ((↑ ((↑ ↑ ↑ ↑ ↑ ω) ⊔ˢ (↑ m))) ⊔ˢ (↑ n))` | ?\r\n\r\nI’m unable to figure out the optimal size for `comp`.  My guess of `↑ ↑ ↑ ↑ ↑ ↑ ↑ ↑ (m ⊔ˢ n)` is rejected with a rather unhelpful error message.\r\n\r\n> Cannot solve size constraints\r\n> `.n ≤ _m_371 .m .n .A .B .C .Γ t u`\r\n> `.m ≤ _m_371 .m .n .A .B .C .Γ t u`\r\n> `_m_371 .m .n .A .B .C .Γ t u ≤ .m`\r\n> Reason: size constraint graph constrains size hypotheses\r\n> when checking the definition of `comp`\r\n\r\nThis is Agda 2.5.1.1.\r\n\r\n```agda\r\nmodule SizeBug3 where\r\n\r\nopen import Agda.Builtin.Size\r\n\r\ndata Cx (U : Set) : Set where\r\n  ⌀   : Cx U\r\n  _,_ : Cx U → U → Cx U\r\n\r\nmodule _ {U : Set} where\r\n  data _⊆_ : Cx U → Cx U → Set where\r\n    done : ⌀ ⊆ ⌀\r\n    skip : ∀ {A Γ Γ′} → Γ ⊆ Γ′ → Γ ⊆ (Γ′ , A)\r\n    keep : ∀ {A Γ Γ′} → Γ ⊆ Γ′ → (Γ , A) ⊆ (Γ′ , A)\r\n\r\n  data _∈_ (A : U) : Cx U → Set where\r\n    top : ∀ {Γ} → A ∈ (Γ , A)\r\n    pop : ∀ {C Γ} → A ∈ Γ → A ∈ (Γ , C)\r\n\r\n  mono∈ : ∀ {A Γ Γ′} → Γ ⊆ Γ′ → A ∈ Γ → A ∈ Γ′\r\n  mono∈ done     ()\r\n  mono∈ (skip η) i       = pop (mono∈ η i)\r\n  mono∈ (keep η) top     = top\r\n  mono∈ (keep η) (pop i) = pop (mono∈ η i)\r\n\r\n  refl⊆ : ∀ {Γ} → Γ ⊆ Γ\r\n  refl⊆ {⌀}     = done\r\n  refl⊆ {Γ , A} = keep refl⊆\r\n\r\ninfixr 3 _⊃_\r\ndata Ty : Set where\r\n  ι   : Ty\r\n  _⊃_ : Ty → Ty → Ty\r\n\r\ninfix 1 _⊢⟨_⟩_\r\ndata _⊢⟨_⟩_ (Γ : Cx Ty) : Size → Ty → Set where\r\n  var  : ∀ {m A}     → A ∈ Γ → Γ ⊢⟨ m ⟩ A\r\n  lam  : ∀ {m A B}   → Γ , A ⊢⟨ m ⟩ B → Γ ⊢⟨ ↑ m ⟩ A ⊃ B\r\n  app  : ∀ {m n A B} → Γ ⊢⟨ m ⟩ A ⊃ B → Γ ⊢⟨ n ⟩ A → Γ ⊢⟨ ↑ (m ⊔ˢ n) ⟩ B\r\n\r\nmono⊢ : ∀ {m A Γ Γ′} → Γ ⊆ Γ′ → Γ ⊢⟨ m ⟩ A → Γ′ ⊢⟨ m ⟩ A\r\nmono⊢ η (var i)   = var (mono∈ η i)\r\nmono⊢ η (lam t)   = lam (mono⊢ (keep η) t)\r\nmono⊢ η (app t u) = app (mono⊢ η t) (mono⊢ η u)\r\n\r\ndet : ∀ {m A B Γ} → Γ ⊢⟨ m ⟩ A ⊃ B → Γ , A ⊢⟨ ↑ m ⟩ B\r\ndet t = app (mono⊢ (skip refl⊆) t) (var top)\r\n\r\nccont : ∀ {m A B Γ} → Γ ⊢⟨ ↑ ↑ ↑ ↑ m ⟩ (A ⊃ A ⊃ B) ⊃ A ⊃ B\r\nccont = lam (lam (app (app (var (pop top)) (var top)) (var top)))\r\n\r\n-- cont : ∀ {m A B Γ} → (Γ , A) , A ⊢⟨ m ⟩ B → Γ , A ⊢⟨ ↑ (↑ ((↑ (↑ (↑ (↑ ω)))) ⊔ˢ (↑ (↑ m)))) ⟩ B\r\n-- cont : ∀ {m A B Γ} → (Γ , A) , A ⊢⟨ m ⟩ B → Γ , A ⊢⟨ ↑ ↑ ((↑ ↑ ↑ ↑ ω) ⊔ˢ (↑ ↑ m)) ⟩ B\r\ncont : ∀ {m A B Γ} → (Γ , A) , A ⊢⟨ m ⟩ B → Γ , A ⊢⟨ ↑ ↑ ↑ ↑ ↑ ↑ m ⟩ B\r\ncont t = det (app ccont (lam (lam t)))\r\n\r\ncexch : ∀ {m A B C Γ} → Γ ⊢⟨ ↑ ↑ ↑ ↑ ↑ m ⟩ (A ⊃ B ⊃ C) ⊃ B ⊃ A ⊃ C\r\ncexch = lam (lam (lam (app (app (var (pop (pop top))) (var top)) (var (pop top)))))\r\n\r\n-- exch : ∀ {m A B C Γ} → (Γ , A) , B ⊢⟨ m ⟩ C → (Γ , B) , A ⊢⟨ ↑ (↑ (↑ ((↑ (↑ (↑ (↑ (↑ ω))))) ⊔ˢ (↑ (↑ m))))) ⟩ C\r\n-- exch : ∀ {m A B C Γ} → (Γ , A) , B ⊢⟨ m ⟩ C → (Γ , B) , A ⊢⟨ ↑ ↑ ↑ ((↑ ↑ ↑ ↑ ↑ ω) ⊔ˢ (↑ ↑ m)) ⟩ C\r\nexch : ∀ {m A B C Γ} → (Γ , A) , B ⊢⟨ m ⟩ C → (Γ , B) , A ⊢⟨ ↑ ↑ ↑ ↑ ↑ ↑ ↑ ↑ m ⟩ C\r\nexch t = det (det (app cexch (lam (lam t))))\r\n\r\nccomp : ∀ {m A B C Γ} → Γ ⊢⟨ ↑ ↑ ↑ ↑ ↑ m ⟩ (B ⊃ C) ⊃ (A ⊃ B) ⊃ A ⊃ C\r\nccomp = lam (lam (lam (app (var (pop (pop top))) (app (var (pop top)) (var top)))))\r\n\r\n-- comp : ∀ {m n A B C Γ} → Γ , B ⊢⟨ m ⟩ C → Γ , A ⊢⟨ n ⟩ B → Γ , A ⊢⟨ ↑ (↑ ((↑ ((↑ (↑ (↑ (↑ (↑ ω))))) ⊔ˢ (↑ m))) ⊔ˢ (↑ n))) ⟩ C\r\n-- comp : ∀ {m n A B C Γ} → Γ , B ⊢⟨ m ⟩ C → Γ , A ⊢⟨ n ⟩ B → Γ , A ⊢⟨ ↑ ↑ ((↑ ((↑ ↑ ↑ ↑ ↑ ω) ⊔ˢ (↑ m))) ⊔ˢ (↑ n)) ⟩ C\r\ncomp : ∀ {m n A B C Γ} → Γ , B ⊢⟨ m ⟩ C → Γ , A ⊢⟨ n ⟩ B → Γ , A ⊢⟨ {!!} ⟩ C\r\ncomp t u = det (app (app ccomp (lam t)) (lam u))\r\n```"},"comment":{"url":"https://api.github.com/repos/agda/agda/issues/comments/232417660","html_url":"https://github.com/agda/agda/issues/2097#issuecomment-232417660","issue_url":"https://api.github.com/repos/agda/agda/issues/2097","id":232417660,"user":{"login":"andreasabel","id":1155218,"avatar_url":"https://avatars.githubusercontent.com/u/1155218?v=3","gravatar_id":"","url":"https://api.github.com/users/andreasabel","html_url":"https://github.com/andreasabel","followers_url":"https://api.github.com/users/andreasabel/followers","following_url":"https://api.github.com/users/andreasabel/following{/other_user}","gists_url":"https://api.github.com/users/andreasabel/gists{/gist_id}","starred_url":"https://api.github.com/users/andreasabel/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/andreasabel/subscriptions","organizations_url":"https://api.github.com/users/andreasabel/orgs","repos_url":"https://api.github.com/users/andreasabel/repos","events_url":"https://api.github.com/users/andreasabel/events{/privacy}","received_events_url":"https://api.github.com/users/andreasabel/received_events","type":"User","site_admin":false},"created_at":"2016-07-13T16:54:44Z","updated_at":"2016-07-13T16:54:44Z","body":"Mmh, I wonder how infinity sneaks in here.  We are almost lucky that Agda does not compute the maximum in these size expressions, otherwise we would only see the uninformative infinity."}}
{"actor":{"display_login":"andreasabel"}}