<div dir="ltr"><div>Imagine you want to have a type level function that calculates the element-wise OR on two bitstrings, encoded as length-indexed vectors filled with Bools (this is a simplification of something I need for a project). The vectors should be "aligned to the right" as it were, such that the new right-most value is True if the right-most value of the first vector OR the right-most value of the second vector was True.<br></div><div><br></div><div>Example (replacing True and False with 1 and 0 for readability):</div><div>ElementwiseOr [1,0,1,1] [0,1,1,0,0,0,0,1]</div><div>= [0,1,1,0,1,0,1,1]<br></div><div><br></div><div>Its type would be something like</div><div>ElementwiseOr :: Vec n Bool -> Vec m Bool -> Vec (Max n m) Bool<br></div><div><br></div><div>I have written the following code:</div><div><br></div><div>---------------------------------------------------------------------------</div><div>{-# LANGUAGE TypeFamilies, GADTs, DataKinds, StandaloneKindSignatures,<br>             PolyKinds, TypeOperators, RankNTypes, TypeApplications,<br>             UndecidableInstances #-}<br><br>import Data.Kind<br>import Data.Type.Equality<br><br>data Nat = Z | S Nat<br><br>infixr 5 :<<br><br>type Vec :: Nat -> Type -> Type<br>data Vec n a where<br>  Nil :: Vec Z a<br>  (:<) :: a -> Vec n a -> Vec (S n) a<br><br>type Cong :: forall f -> a :~: b -> f a :~: f b<br>type family Cong f p where<br>  Cong f Refl = Refl<br><br>type Max :: Nat -> Nat -> Nat<br>type family Max n m where<br>  Max Z m = m<br>  Max n Z = n<br>  Max (S n) (S m) = S (Max n m)</div><div>
<div><br></div><div>-- The reason for this slightly convoluted Ordering type is that it seems</div><div>-- to make the "right-alignment" easier.<br></div><div>type NatOrdering :: Ordering -> Nat -> Nat -> Type<br>data NatOrdering o n m where<br>  NOLTE :: NatOrdering EQ n m -> NatOrdering LT n (S m)<br>  NOLTS :: NatOrdering LT n m -> NatOrdering LT n (S m)<br>  NOEQZ :: NatOrdering EQ Z Z<br>  NOEQS :: NatOrdering EQ n m -> NatOrdering EQ (S n) (S m)<br>  NOGTE :: NatOrdering EQ n m -> NatOrdering GT (S n) m<br>  NOGTS :: NatOrdering GT n m -> NatOrdering GT (S n) m</div>

<br>type MaxSIsSMaxEQ<br>  :: forall n m . NatOrdering EQ n m -> Max n (S m) :~: S (Max n m)<br>type family MaxSIsSMaxEQ o where<br>  MaxSIsSMaxEQ NOEQZ = Refl<br>  MaxSIsSMaxEQ (NOEQS o) = Cong S (MaxSIsSMaxEQ o)<br><br>type TransportVec :: n :~: m -> Vec n a -> Vec m a<br>type family TransportVec p v where<br>  TransportVec Refl v = v<br><br>type ElementwiseOr<br>  :: NatOrdering o n m -> Vec n Bool -> Vec m Bool -> Vec (Max n m) Bool<br>type family ElementwiseOr o u v where<br>  ElementwiseOr (NOLTE o) u (s :< v) =<br>    TransportVec (MaxSIsSMaxEQ o) (s :< ElementwiseOr o u v) -- XXX<br>  -- other equations ommitted</div><div>---------------------------------------------------------------------------</div><div><br></div><div>To me, the equation at the end marked with XXX seems like it should work. However, it produces the following error:</div><div><br></div><div>    • Couldn't match kind: Max n ('S m)<br>                     with: 'S (Max n m)<br>      Expected kind ‘'S (Max n m) :~: 'S (Max n m)’,<br>        but ‘MaxSIsSMaxEQ o’ has kind ‘Max n ('S m) :~: 'S (Max n m)’<br>    • In the first argument of ‘TransportVec’, namely<br>        ‘(MaxSIsSMaxEQ o)’</div><div><br></div><div>So it expects something of kind `S (Max n m) :~: S (Max n m)` - it seems like Refl fits that bill, but that doesn't work either, because replacing (MaxSIsSMaxEQ o) with Refl means that TransportVec returns a type of the wrong kind, producing a very similar error.<br><br></div><div>I suspect the reason this doesn't work is because type equality isn't equipped to properly handle type family applications. I could potentially work around this if I defined Max as<br><br></div><div>data Max n m r where</div><div>  MaxZZ :: Max Z Z Z</div><div>  MaxSZ :: Max (S n) Z (S n)</div><div>  MaxZS :: Max Z (S m) (S m)</div><div>  MaxSS :: Max n m r -> Max (S n) (S m) (S r)<br></div><div><br></div><div>However, dealing with a proof object like this is a lot less convenient than just being able to use a type family for most purposes, so I'd like to avoid this if possible.</div><div><br></div><div>Is there a way to make this work while sticking with type families?</div><div><br></div><div>Thanks</div><div><br></div><div>Jakob<br></div></div>