[Agda] Agda2 beginner's question

[kahl at cas.mcmaster.ca]

Dear Agda list,

  I know Haskell, including GADTs, and have used Isabelle before;
now I am just starting to try to get going with Agda2
and hit a serious roadblock in trying to unwrap a Data.Vec.Group
from the standard library (lib-0.2) to get at the enclosed Vec (Vec ...).

Since my ``group'' application appears to type check,
I would not have expected to be asked to prove

  concat xss = allFin (n * m)

before I can bind ``xss'' in the concat' pattern.
And even if I really have to do it, I have no idea how to start...


What am I overlooking?


Wolfram


----
module Matrix where

open import Data.Nat
open import Data.Vec
open import Data.Function using (_$_)
open import Data.Fin using (toℕ)

Matrix : Set → ℕ → ℕ → Set
Matrix A m n = Vec (Vec A n) m


transpose : ∀ {A m n} → Matrix A m n → Matrix A n m
transpose [] = replicate []
transpose (xs ∷ xss) = zipWith _∷_ xs (transpose xss)


mat1 : (m : ℕ) → (n : ℕ) → Matrix ℕ m n
mat1 m n with group n m (allFin (n * m))
mat1 m n | concat' xss  = map (map toℕ) xss