<div dir="ltr"><div>Hi Cafe,</div><div><br></div><div>I'm trying to do some basic type level tricks, I wonder whether it is possible to get ``vZipWith`` in below code snippet working:</div><div><br></div><div>{-# LANGUAGE DataKinds #-}</div><div>{-# LANGUAGE PolyKinds #-}</div><div>{-# LANGUAGE KindSignatures #-}</div><div>{-# LANGUAGE TypeOperators #-}</div><div>{-# LANGUAGE TypeFamilies #-}</div><div>{-# LANGUAGE ScopedTypeVariables #-}</div><div>{-# LANGUAGE RankNTypes #-}</div><div>{-# LANGUAGE GADTs #-}</div><div>{-# LANGUAGE StandaloneDeriving #-}</div><div>{-# LANGUAGE UndecidableInstances #-}</div><div>{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}</div><div><br></div><div>import GHC.TypeLits</div><div>import Data.Proxy</div><div><br></div><div>data Vect :: (Nat -> * -> *) where</div><div>  VNil :: Vect 0 a</div><div>  VCons :: a -> Vect n a -> Vect (1+n) a</div><div><br></div><div>deriving instance (Show a) => Show (Vect n a)</div><div><br></div><div>vlength :: forall n a . KnownNat n => Vect n a -> Integer</div><div>vlength _ = natVal (Proxy :: Proxy n)</div><div><br></div><div>vconcat :: Vect n a -> Vect m a -> Vect (n+m) a         -- Need type checker plugin</div><div>vconcat VNil ys = ys</div><div>vconcat xs VNil = xs</div><div>vconcat (VCons x xs) ys = VCons x (vconcat xs ys)</div><div><br></div><div><span style="line-height:1.5">type family Min3 (t :: Bool) (m :: Nat) (n :: Nat) :: Nat</span><br></div><div><br></div><div>type instance Min3 'True m n = m</div><div>type instance Min3 'False m n = n</div><div>type Min m n = Min3 (m <=? n) m n</div><div><br></div><div>vZipWith :: (a -> b -> c) -> Vect m a -> Vect n b -> Vect (Min m n) c</div><div>vZipWith f VNil _ = VNil</div><div>vZipWith f _ VNil = VNil</div><div>vZipWith f (VCons x xs) (VCons y ys) = f x y `VCons` vZipWith f xs ys</div><div><br></div><div><br></div><div>As I got errors:</div><div><br></div><div><div>/home/wangbj/downloads/stack/vect/src/Vect.hs:51:21:</div><div>    Could not deduce (Min3 (m <=? 0) m 0 ~ 0)</div><div>    from the context (n ~ 0)</div><div>      bound by a pattern with constructor</div><div>                 VNil :: forall a. Vect 0 a,</div><div>               in an equation for ‘vZipWith’</div><div>      at /home/wangbj/downloads/stack/vect/src/Vect.hs:51:14-17</div><div>    Expected type: Vect (Min m n) c</div><div>      Actual type: Vect 0 c</div><div>    Relevant bindings include</div><div>      vZipWith :: (a -> b -> c)</div><div>                  -> Vect m a -> Vect n b -> Vect (Min m n) c</div><div>        (bound at /home/wangbj/downloads/stack/vect/src/Vect.hs:50:1)</div><div>    In the expression: VNil</div><div>    In an equation for ‘vZipWith’: vZipWith f _ VNil = VNil</div><div><br></div><div>/home/wangbj/downloads/stack/vect/src/Vect.hs:52:40:</div><div>    Could not deduce (Min3 (m <=? n) m n</div><div>                      ~ (1 + Min3 (n1 <=? n2) n1 n2))</div><div>    from the context (m ~ (1 + n1))</div><div>      bound by a pattern with constructor</div><div>                 VCons :: forall a (n :: Nat). a -> Vect n a -> Vect (1 + n) a,</div><div>               in an equation for ‘vZipWith’</div><div>      at /home/wangbj/downloads/stack/vect/src/Vect.hs:52:13-22</div><div>    or from (n ~ (1 + n2))</div><div>      bound by a pattern with constructor</div><div>                 VCons :: forall a (n :: Nat). a -> Vect n a -> Vect (1 + n) a,</div><div>               in an equation for ‘vZipWith’</div><div>      at /home/wangbj/downloads/stack/vect/src/Vect.hs:52:26-35</div><div>    Expected type: Vect (Min m n) c</div><div>      Actual type: Vect (1 + Min n1 n2) c</div><div>    Relevant bindings include</div><div>      ys :: Vect n2 b</div><div>        (bound at /home/wangbj/downloads/stack/vect/src/Vect.hs:52:34)</div><div>      xs :: Vect n1 a</div><div>        (bound at /home/wangbj/downloads/stack/vect/src/Vect.hs:52:21)</div><div>      vZipWith :: (a -> b -> c)</div><div>                  -> Vect m a -> Vect n b -> Vect (Min m n) c</div><div>        (bound at /home/wangbj/downloads/stack/vect/src/Vect.hs:50:1)</div><div>    In the expression: f x y `VCons` vZipWith f xs ys</div><div>    In an equation for ‘vZipWith’:</div><div>        vZipWith f (VCons x xs) (VCons y ys)</div><div>          = f x y `VCons` vZipWith f xs ys</div><div>Failed, modules loaded: none.</div></div><div><br></div><div>Also I tried <a href="https://github.com/yav/type-nat-solver">https://github.com/yav/type-nat-solver</a> but got error like:</div><div><br></div><div><div>*** Exception: user error (Unexpected result from the SMT solver:</div><div>  Expected: success</div><div>  Result: (error "line 57 column 16: unknown constant tn_0" )</div><div><br></div></div><div>Which I have no idea what it really means.</div><div><br></div><div>Is there any way to get ``vZipWith`` working without too much hassle?</div><div><br></div><div>Thanks</div><div>baojun</div><div><br></div></div>