Problem.hs

{-# LANGUAGE AllowAmbiguousTypes #-}  

module Problem where

import Clash.Prelude

id1                                                                                                       
  :: forall n
   . ( KnownNat n
     , 1 <= (CLog 2 (n+2))
     ) 
  => Vec (CLog 2 (n+2)) Bool                            
  -> Vec (CLog 2 (n+2)) Bool
id1 v = id2 @n v  

id2                                                                                                 
  :: forall n
   . ( KnownNat n
     , 1 <= (CLog 2 (n+2)) 
     ) 
  => Vec (CLog 2 (n+2)) Bool
  -> Vec (CLog 2 (n+2)) Bool
id2 = id