Size constraint solver too eager in the presence of meta variables

[GoogleCodeExporter]

A size meta is set to i, but the user wants \inf. The early setting of this meta prevents the user from giving the goal.

Goal: Heap {i} p1 (r1-rank + suc (l2-rank + r2-rank))
Have: Heap {∞} p1 (r1-rank + suc (l2-rank + r2-rank))

Original issue reported on code.google.com by andreas....@gmail.com on 7 Dec 2013 at 10:23

Attachments:

• Issue992.agda

[andreasabel]

----------------------------------------------------------------------
-- Copyright: 2013, Jan Stolarek, Lodz University of Technology     --
--                                                                  --
-- License: See LICENSE file in root of the repo                    --
-- Repo address: https://github.com/jstolarek/dep-typed-wbl-heaps   --
--                                                                  --
----------------------------------------------------------------------

{-# OPTIONS --sized-types #-}
{-# OPTIONS --show-implicit #-}

open import Common.Size
open import Common.Prelude
open import Common.Equality

+0 : (a : Nat) → a + zero ≡ a -- see [0 is right identity of addition]
+0 zero    = refl
+0 (suc a) = cong suc (+0 a)

+suc : (a b : Nat) → suc (a + b) ≡ a + (suc b)
+suc zero b    = refl
+suc (suc a) b = cong suc (+suc a b)

data _≥_ : Nat → Nat → Set where
  ge0 : {y : Nat}                   → y     ≥ zero
  geS : {x : Nat} {y : Nat} → x ≥ y → suc x ≥ suc y

infixl 4 _≥_

-- Order datatype tells whether two numbers are in ≥ relation or
-- not. In that sense it is an equivalent of Bool datatype. Unlike
-- Bool however, Order supplies a proof of WHY the numbers are (or are
-- not) in the ≥ relation.
data Order : Nat → Nat → Set where
  ge : {x : Nat} {y : Nat} → x ≥ y → Order x y
  le : {x : Nat} {y : Nat} → y ≥ x → Order x y

-- order function takes two natural numbers and compares them,
-- returning the result of comparison together with a proof of the
-- result.
order : (a : Nat) → (b : Nat) → Order a b
order a       zero    = ge ge0
order zero    (suc b) = le ge0
order (suc a) (suc b) with order a b
order (suc a) (suc b) | ge ageb = ge (geS ageb)
order (suc a) (suc b) | le bgea = le (geS bgea)


Rank     = Nat
Priority = Nat

postulate

  makeT-lemma : (a b : Nat) →
    suc (a + b) ≡ suc (b + a)

  proof-1a : (l1 r1 l2 r2 : Nat) →
    suc ( l1 + (r1 + suc (l2 + r2))) ≡ suc ((l1 + r1) + suc (l2 + r2))

  proof-2a : (l1 r1 l2 r2 : Nat) →
    suc (l2 + (r2  + suc (l1 + r1))) ≡ suc ((l1 + r1) + suc (l2 + r2))

  proof-1b : (l1 r1 l2 r2 : Nat) →
    suc ((r1 + suc (l2 + r2)) + l1) ≡ suc ((l1 + r1) + suc (l2 + r2))

  proof-2b : (l1 r1 l2 r2 : Nat) →
    suc ((r2 + suc (l1 + r1)) + l2) ≡ suc ((l1 + r1) + suc (l2 + r2))


data Heap : {i : Size} → Priority → Rank → Set where
  empty : {i : Size} {b : Priority} → Heap {↑ i} b zero
  node  : {i : Size} {b : Priority} → (p : Priority) → p ≥ b → {l r : Rank} → l ≥ r →
          Heap {i} p l → Heap {i} p r → Heap {↑ i} b (suc (l + r))

merge : {i j : Size} {b : Priority} {l r : Rank} → Heap {i} b l → Heap {j} b r
      → Heap {∞} b (l + r)
merge empty h2 = h2 -- See [merge, proof 0a]
merge {_} .{_} {b} {suc l} {zero} h1 empty
          = subst (Heap b)
                  (sym (+0 (suc l)))  -- See [merge, proof 0b]
                  h1
merge .{_} .{_} .{b} {suc .(l1-rank + r1-rank)} {suc .(l2-rank + r2-rank)}
  (node {_} .{b} p1 p1≥b {l1-rank} {r1-rank} l1≥r1 l1 r1)
  (node {_}  {b} p2 p2≥b {l2-rank} {r2-rank} l2≥r2 l2 r2)
  with order p1 p2
  | order l1-rank (r1-rank + suc (l2-rank + r2-rank))
  | order l2-rank (r2-rank + suc (l1-rank + r1-rank))
merge .{↑ i} .{↑ j}  .{b} {suc .(l1-rank + r1-rank)} {suc .(l2-rank + r2-rank)}
  (node {i}.{b} p1 p1≥b {l1-rank} {r1-rank} l1≥r1 l1 r1)
  (node {j} {b} p2 p2≥b {l2-rank} {r2-rank} l2≥r2 l2 r2)
  | le p1≤p2
  | ge l1≥r1+h2
  | _
  = subst (Heap b)
          (proof-1a l1-rank r1-rank l2-rank r2-rank) -- See [merge, proof 1a]
          (node p1 p1≥b l1≥r1+h2 l1 {!merge {i}{↑ j} r1 (node p2 p1≤p2 l2≥r2 l2 r2)!}) --(merge r1 (node p2 p1≤p2 l2≥r2 l2 r2)))
merge .{↑ i} .{↑ j} .{b} {suc .(l1-rank + r1-rank)} {suc .(l2-rank + r2-rank)}
  (node {i} .{b} p1 p1≥b {l1-rank} {r1-rank} l1≥r1 l1 r1)
  (node {j}  {b} p2 p2≥b {l2-rank} {r2-rank} l2≥r2 l2 r2)
  | le p1≤p2
  | le l1≤r1+h2
  | _
  = subst (Heap b)
          (proof-1b l1-rank r1-rank l2-rank r2-rank) -- See [merge, proof 1b]
          (node p1 p1≥b l1≤r1+h2 (merge {i}{↑ j} r1 (node p2 p1≤p2 l2≥r2 l2 r2)) l1)
merge .{↑ i} .{↑ j}  .{b} {suc .(l1-rank + r1-rank)} {suc .(l2-rank + r2-rank)}
  (node {i} .{b} p1 p1≥b {l1-rank} {r1-rank} l1≥r1 l1 r1)
  (node {j}  {b} p2 p2≥b {l2-rank} {r2-rank} l2≥r2 l2 r2)
  | ge p1≥p2
  | _
  | ge l2≥r2+h1
  = subst (Heap b)
          (proof-2a l1-rank r1-rank l2-rank r2-rank) -- See [merge, proof 2a]
          (node p2 p2≥b l2≥r2+h1 l2 (merge {j}{↑ i} r2 (node p1 p1≥p2 l1≥r1 l1 r1)))
merge .{↑ i} .{↑ j}  .{b} {suc .(l1-rank + r1-rank)} {suc .(l2-rank + r2-rank)}
  (node {i} .{b} p1 p1≥b {l1-rank} {r1-rank} l1≥r1 l1 r1)
  (node {j}  {b} p2 p2≥b {l2-rank} {r2-rank} l2≥r2 l2 r2)
  | ge p1≥p2
  | _
  | le l2≤r2+h1
  = subst (Heap b)
          (proof-2b l1-rank r1-rank l2-rank r2-rank) -- See [merge, proof 2b]
          (node p2 p2≥b l2≤r2+h1 (merge r2 (node p1 p1≥p2 l1≥r1 l1 r1)) l2)

[nad]

Here is a shorter test case:

open import Agda.Builtin.Size

data D : (i : Size) → Set where
  c  : (i : Size) → D i → D i → D (↑ i)

postulate
  f : (i : Size) → D i → D ω

g : (i : Size) (x : D i) → D ω
g i x = c _ x {!f i x!}

Error message when an attempt is made to "give" the expression in the hole:

ω !=< i of type Size
when checking that the expression f i x has type D i

[andreasabel]

Agda picks the smallest solution, i, for the size meta, but this is incomplete, we need to take the variance into account.

[andreasabel]

Another case (lifted from #6002):

{-# OPTIONS --sized-types #-}

open import Agda.Builtin.Size

record Thunk (F : Size → Set₁) i : Set₁ where
  coinductive
  field force : (j : Size< i) → F j

open Thunk

data Embed : ∀ i → Thunk (λ _ → Set) i → Set where
  [_] : ∀ {i} {A : Thunk (λ _ → Set) ?} → A .force i → Embed (↑ i) A

The ? has solution ↑ i but defaults to ∞, leading to error:

Cannot solve size constraints
↑ i =< ↑ i : Size
  (blocked on any(_i_12, _i_15), belongs to problems 14, 16)
↑ i =< ↑ i : Size (blocked on _i_15, belongs to problem 17)
∞ =< ↑ i : Size (blocked on any(_i_15, _16), belongs to problem 17)
↑ i =< ↑ i : Size (blocked on _i_12, belongs to problems 22, 24)
when checking that the expression A has type
Thunk (λ _ → Set) (↑ i)