帰納的定義型

Question

次のスニペットのための（番組の）実装を（https://stackoverflow.com/a/37461290/2129302）から検索された：

tensor : Vect n Nat -> Type -> Type 
tensor []  a = a 
tensor (m :: ms) a = Vect m (tensor ms a) 

私は次のように定義したいと思います：

mkStr : (Show a) => tensor shape a -> String 
mkStr x = show x 

しかし、その代わりに、この次のエラーが返されます。

Can't find implementation for Show (tensor shape a) 

ただし、REPLでは「show [some tensor value .. 。] "なぜこれがあり、それを修正するために何ができますか？

Answer 1

aが表示されていません。tensor shape aと表示されています。したがって、次のように動作し、次の方法で型を記述する必要があります。

mkStr : (Show (tensor shape a)) => tensor shape a -> String 
mkStr x = show x