[Agda] "metavariable" message

[Sergei Meshveliani]

People,
I have the two questions about the below program.

1) Why the checker reports about "metavariable" ?

   (Agda 2.3.2.2 MAlonzo).  

2) How to prove  toDgs'-suc=toDgs-suc ?

The statement looks as trivial, 
and  " → blRefl"  needs to be sufficient in the last branch.  
But it fails.

Thank you in advance for explanation,

------
Sergei


--------------------------------------------------------------
open import Function using (_$_; _∘_; case_of_)
open import Relation.Binary using
     (IsEquivalence; module IsEquivalence; Setoid;
      module Setoid; DecSetoid; module DecSetoid;
      DecTotalOrder; module DecTotalOrder
     )
open import Relation.Binary.PropositionalEquality as PE
                                                  using (_≡_)
open import Data.Empty      using (⊥; ⊥-elim)
open import Data.Unit       using (⊤)
open import Data.Fin as Fin using (Fin)
                            renaming (zero to 0b; suc to sucF)
import Data.Fin.Props as FinP using (decSetoid)
open import Data.Digit using (Bit)
open import Data.Bin   using (Bin⁺)
open import Data.Digit using (toDigits; fromDigits)
open import Data.Product    using (_×_; _,_; proj₁; proj₂; ∃)
open import Data.Nat as Nat using (ℕ; suc)
                            renaming (decTotalOrder to natDTO)
open import Data.List     using (List; []; _∷_)
open import Relation.Binary.List.Pointwise as LP using ()

-------------------------------------------------------------------             
bitDecSetoid = FinP.decSetoid 2
open DecSetoid bitDecSetoid using () renaming (setoid to bitSetoid)
blSetoid = LP.setoid bitSetoid
open Setoid blSetoid using ()
                  renaming (_≈_ to _=l_; isEquivalence to blEquiv)
open IsEquivalence blEquiv using ()
                           renaming (refl to blRefl; sym to blSym)

postulate anything : ∀ {a} {A : Set a} → A  -- for debug  

toDgs = proj₁ ∘ toDigits 2

toDigits' : (n : ℕ) → ∃ \ (bs : Bin⁺) → fromDigits bs ≡ n
toDigits' n  with  toDigits 2 n

... | ([]      , eq) =  ([]     , eq)  -- inaccessible 
... | (0b ∷ [] , eq) =  ([]     , eq)
... | (b ∷ bs  , eq) =  (b ∷ bs , eq)
--
-- It differs from  toDigits  only at  n = 0.

toDgs' = proj₁ ∘ toDigits'

toDgs'-suc=toDgs-suc : ∀ n → toDgs' (suc n) =l toDgs (suc n)
toDgs'-suc=toDgs-suc 0       = blRefl
toDgs'-suc=toDgs-suc (suc n) =  
  case
      toDigits 2 (suc (suc n))
  of \
  { ([]                    , ())
  ; (0b ∷ []               , ())
  ; ((sucF 0b) ∷ []        , ())
  ; ((sucF (sucF ())) ∷ [] , _ )
  ; (b ∷ b' ∷ bs           , _ ) →
         let gl : toDgs' (suc $ suc n) =l (b ∷ b' ∷ bs)
                                         -- toDgs (suc $ suc n) 
             gl = anything
         in  gl
  }