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