Исправление qnikst, (текущая версия) :
Если ещё будут идеи, как использовать с этим KnowNat - пиши, а то смотри:
> data Proof2D :: (Nat -> *) -> * where
> Proof2D :: Dict (KnownNat n) -> c n -> Proxy n -> Proof2D c
> instance Show (Proof2D c) where
> show (Proof2D _ _ k) = show (natVal k)
Min.lhs:22:34:
No instance for (KnownNat n) arising from a use of ‘natVal’
Possible fix:
add (KnownNat n) to the context of
the data constructor ‘Proof2D’
or the instance declaration
это поидее через reflection может решиться, но я его не умею :/
Исходная версия qnikst, :
Если ещё будут идеи, как использовать с этим KnowNat - пиши, а то смотри:
> data Proof2D :: (Nat -> *) -> * where
> Proof2D :: Dict (KnownNat n) -> c n -> Proxy n -> Proof2D c
> instance Show (Proof2D c) where
> show (Proof2D _ _ k) = show (natVal k)
Min.lhs:22:34:
No instance for (KnownNat n) arising from a use of ‘natVal’
Possible fix:
add (KnownNat n) to the context of
the data constructor ‘Proof2D’
or the instance declaration
это поидее через reify может решиться, но я его не умею :/