Forcing too early results in a failure to solve constraints.

ForcingErrorOkasakiCatList.idr

%default total

interface Queue (q: Type -> Type) where   
  empty : q a 
  isEmpty : q a -> Bool
  snoc : q a -> a -> q a 
  head : q a -> a
  tail : q a -> q a 

data CatList : (Type -> Type) -> Type -> Type where
  E : CatList q a 
  C : {q : Type -> Type} -> a -> q (Lazy (CatList q a)) -> CatList q a 

link : (Queue q) => CatList q a -> Lazy (CatList q a) -> CatList q a 
link E s = s 
link (C x xs) s = C x (snoc xs s) -- can't solve constraint between 
                                  -- Lazy (CatList q a) and CatList q a