module HAssociativity where

open import Data.List

postulate View : List Set -> Set -> Set

open import Relation.Binary.PropositionalEquality

assoc-++ : ∀ (a b c : List Set) -> (a ++ b) ++ c ≡ a ++ b ++ c
assoc-++ [] b c = refl
assoc-++ (x ∷ a) b c = cong (_∷_ x) (assoc-++ a b c)

data HList : List Set -> Set₁ where
  [] : HList []
  _∷_ : ∀ {xs x} -> x -> (ts : HList xs) -> HList (x ∷ xs)

infixr 7 _∷_

_+++_ : ∀ {xs ys} -> HList xs -> HList ys -> HList (xs ++ ys)
[] +++ bs = bs
(a ∷ as) +++ bs = a ∷ (as +++ bs)

infixr 5 _+++_

open import Relation.Binary.HeterogeneousEquality
import Relation.Binary.HeterogeneousEquality as H

-- I am trying to prove that _+++_ is associative.
-- I need Heterogeneous Equality because the indexes are different due to ++ associativity.
assoc-+++ : ∀ {xs ys zs} (a : HList xs) (b : HList ys) (c : HList zs) -> a +++ b +++ c ≅ (a +++ b) +++ c
assoc-+++ [] b c = refl
assoc-+++ {_ ∷ xs} {ys} {zs} (x ∷ a) b c = H.cong (_∷_ x) {!assoc-+++ {xs} {ys} {zs} a b c!} -- (xs +++ ys) != xs (needs associativity)

-- (xs ++ ys) ++ ws != w when checking that the type ... of the generated with function is well formed 
-- is the error message raised in 1) , 2) and 3)
-- From the discussion at http://code.google.com/p/agda/issues/detail?id=206 
-- I don't think that this is a bug.

-- 1)
-- assoc-+++ {x ∷ xs} {ys} {zs} (t ∷ a) b c with (xs ++ ys) ++ zs | assoc-++ xs ys zs
-- ... | r | p = H.cong (_∷_ t) {!assoc-+++ a b c!}

-- 2)
-- assoc-+++ {x ∷ xs} {ys} {zs} (t ∷ a) b c 
--   rewrite (assoc-++ xs ys zs) = ?

-- 3) 
-- assoc-+++ {x ∷ xs} {ys} {zs} (t ∷ a) b c with (xs ++ ys) ++ zs | assoc-++ xs ys zs | a +++ b +++ c | (assoc-+++ a b c)
-- ... | p | q | r | s  = {!!}