@@ -59,16 +59,16 @@ implementation (DecEq t, DecEq (HVect ts)) => DecEq (HVect (t::ts)) where
5959 decEq (z::xs) (z::ys) | Yes Refl | No ctr = No (ctr . hvectInjective2)
6060 decEq (x::xs) (y::ys) | No ctr = No (ctr . hvectInjective1)
6161
62−interface Shows (k : Nat) (ts : Vect k Type) where
62+interface Shows (ts : Vect k Type) where
6363 shows : HVect ts -> Vect k String
6464
65−implementation Shows Z [] where
65+implementation Shows [] where
6666 shows [] = []
6767
68−implementation (Show t, Shows k ts) => Shows (S k) (t::ts) where
68+implementation (Show t, Shows ts) => Shows (t::ts) where
6969 shows (x::xs) = show x :: shows xs
7070
71−implementation (Shows k ts) => Show (HVect ts) where
71+implementation (Shows ts) => Show (HVect ts) where
7272 show xs = "[" ++ (pack . intercalate [','] . map unpack . toList $ shows xs) ++ "]"
7373
7474||| Extract an arbitrary element of the correct type.