<div dir="ltr"><div><div><div><div><div>I have a datatype (called "Bob") that tracks whether a variable has been used or not.<br></div>I have an index datatype that points to multiple variables in the datatype Bob without depending on the datatype "Bob" so as to not become invalid when "Bob" changes to reflect the unavailability of a variable.<br><br></div>The datatype "Belongs" depends on an Index and Bob. It proves that all the variables pointed by the index are actually available.<br><br></div>Every time Bob, changes, a new Belongs datatype is needed. I want this proof to be generated by instance resolution.<br><br></div>I am not sure if this is possible when the index points to an infinite number of variables, ie if we have coinductive types. <br><br></div>Here is the example.<br><br>-------------------------<br><br>module Test where<br><br>open import Data.Bool<br>open import Size<br><br>mutual<br><br>  data Bob (i : Size) : Set where<br>    more : Bob i → Bool → Bob i<br>    none : Bob i<br>    twoPaths : Bob i → Bob i → Bob i<br>    inf : Bob∞ i → Bob i<br><br>  record Bob∞ (i : Size) : Set where<br>    coinductive<br>    field<br>      bob : {j : Size< i} → Bob j <br><br>open Bob∞<br><br>data Bel : Set where<br>  bel : Bel<br>  nbel : Bel<br>  <br>mutual<br><br>  data Index (i : Size) : Set where<br>    here : Index i<br>    more : Index i → Bel → Index i<br>    left : Index i → Index i<br>    right : Index i → Index i<br>    inf : Index∞ i → Index i<br>    <br>  record Index∞ (i : Size) : Set where<br>    coinductive<br>    field<br>      index : {j : Size< i} → Index j<br><br>open Index∞<br><br>mutual<br><br>  data Belongs {i : Size} : Index i → Bob i → Set where<br>    instance<br>      here : ∀{b} → Belongs here (more b true)<br>      moreBel : ∀{ind b} → {{is : Belongs ind b}} → Belongs (more ind bel) (more b true)<br>      morenBel : ∀{ind b bool} → {{is : Belongs ind b}} → Belongs (more ind nbel) (more b bool)<br>      left : ∀{ind bl br} → {{is : Belongs ind bl}} → Belongs (left ind) (twoPaths bl br)<br>      right : ∀{ind bl br} → {{is : Belongs ind br}} → Belongs (right ind) (twoPaths bl br)<br>      inf : ∀{ind∞ bob∞} → {{is∞ : Belongs∞ ind∞ bob∞}} → Belongs (inf ind∞) (inf bob∞)<br><br>  record Belongs∞ {i : Size} (ind∞ : Index∞ i) (bob∞ : Bob∞ i) : Set where<br>    coinductive<br>    field<br>      belongs : {j : Size< i} → Belongs (index ind∞) (bob bob∞)<br><br>open Belongs∞<br><br>mutual<br><br>  b : ∀{i} → Bob i<br>  b = more (inf b∞) true<br><br>  b∞ : ∀{i} → Bob∞ i<br>  bob b∞ = b<br><br><br>mutual<br><br>  ind : ∀{i} → Index i<br>  ind = more (inf ind∞) bel<br><br>  ind∞ : ∀{i} → Index∞ i<br>  index ind∞ = ind<br><br><br>data R : Set where<br>  r : R<br><br>test : {{bl : Belongs ind b}} → R<br>test = r<br><br><br>-- I want instance resolution to create this datatype.<br><br>mutual<br><br>  bl : {i : Size} → Belongs {i} ind b<br>  bl = moreBel {{inf {{bl∞}}}}<br><br>  bl∞ : {i : Size} → Belongs∞ {i} ind∞ b∞<br>  belongs bl∞ = bl <br><br><br>f : R<br>f = test<br><br></div>