[Agda] Codata and "with" matching

[Shin-Cheng Mu]

Hi,

This is about an anomaly that confused me when we were
experimenting with codata. The following code uses
the standard library.

   ---

module Stream where

open import Data.Nat
open import Data.Function
open import Data.Product
open import Relation.Binary.PropositionalEquality

{- Define stream as codata -}

codata Stream (A : Set) : Set where
   _∷ˢ_ : A -> Stream A -> Stream A

{- head and tail -}

head : {A : Set} -> Stream A -> A
head (x ∷ˢ _) = x

tail : {A : Set} -> Stream A -> Stream A
tail (_ ∷ˢ xs) = xs

{- and unfold -}

unfoldˢ : {A B : Set} -> (B -> A × B) -> B -> Stream A
unfoldˢ f b with f b
...         | (a , b') ~ a ∷ˢ unfoldˢ f b'

{- Bisimulation. Well, this is only bisimulation specialised
    to streams. -}

codata _∼_ {A : Set} : Stream A -> Stream A -> Set where
   bisim : {xs ys : Stream A} -> head xs ≡ head ys ->
             tail xs ∼ tail ys -> xs ∼ ys

{- Now I would like to prove this unfold fusion rule -}

unfoldˢ-fusion : {A B C : Set} {f : B -> A × B} {h : C -> B} {g : C - 
 > A × C} ->
   (forall x -> f (h x) ≡ map-× id h (g x)) ->
   (forall x -> unfoldˢ f (h x) ∼ unfoldˢ g x)
unfoldˢ-fusion {f = f} {h = h} {g = g} fuse x ~ bisim {! !} {! !}

{- The two holes have (normalised) types:

    ?0 :  (.Relation.Binary.Core._≡_ (head (unfoldˢ f (h x) | f (h  
x)))
             (head (unfoldˢ g x | g x)))
    ?1 : (tail (unfoldˢ f (h x) | f (h x)) ∼ tail (unfoldˢ g x | g  
x))

    which seem to hint at performing a "with" matching on
    f (h x) or g x. Indeed it seems like the right thing to do
    to expand the definitions before we can prove that
    head (unfoldˢ f (h x)) equals head (unfoldˢ g x).

    However, after performing a "with":

    unfoldˢ-fusion {f = f} {h = h} {g = g} fuse x with f (h x)
    ... | (i , j) ~ bisim {! !} {! !}

    The types of the holes do not change at all:

    ?0 : (.Relation.Binary.Core._≡_ (head (unfoldˢ f (h x) | f (h  
x)))
           (head (unfoldˢ g x | g x)))
    ?1 : (tail (unfoldˢ f (h x) | f (h x)) ∼ tail (unfoldˢ g x | g  
x))

    Why isn't "with" refining the types?

Thanks!
-}