<div dir="ltr">Hi folks!<div><br></div><div>I'm playing with GHC 8 and have the following type family definend:</div><div><br></div><div><div style="font-family:monospace,monospace">type family InsertSorted (gt :: k -> k -> Bool) (a :: k) (xs :: [k]) :: [k] where</div><div style="font-family:monospace,monospace">    InsertSorted f a '[] = '[a]</div><div style="font-family:monospace,monospace">    InsertSorted f a (x ': xs) = If (f a x) (x ': InsertSorted f a xs) (a ': x ': xs)</div><div style="font-family:monospace,monospace"><br></div><div><font face="arial, helvetica, sans-serif">With appropriate type functions, I can evaluate this in GHCi with `:kind!` and it does what I want:</font></div><div><font face="arial, helvetica, sans-serif"><br></font></div><div><div><font face="monospace, monospace">λ> :kind! InsertSorted GreaterThan One '[Two, Four]</font></div><div><font face="monospace, monospace">InsertSorted GreaterThan One '[Two, Four] :: [Face]</font></div><div><font face="monospace, monospace">= '['One, 'Two, 'Four]</font></div><div><font face="monospace, monospace">λ> :kind! InsertSorted GreaterThan Queen '[Two, Four]</font></div><div><font face="monospace, monospace">InsertSorted GreaterThan Queen '[Two, Four] :: [Face]</font></div><div><font face="monospace, monospace">= '['Two, 'Four, 'Queen]</font></div><div style="font-family:arial,helvetica,sans-serif"><br></div></div><div><font face="arial, helvetica, sans-serif">However, I get an error if I try to use this in a type signature. This code:</font></div><div><font face="arial, helvetica, sans-serif"><br></font></div><div><div><font face="monospace, monospace">data Deck (b :: [k]) where</font></div><div><font face="monospace, monospace">    Empty :: Deck '[]</font></div><div><font face="monospace, monospace">    (:::) :: CardT s f </font></div><div><font face="monospace, monospace">          -> Deck xs </font></div><div><font face="monospace, monospace">          -> Deck (InsertSorted GreaterThan '(s, f) xs)</font></div><div style="font-family:arial,helvetica,sans-serif"><br></div></div><div style="font-family:arial,helvetica,sans-serif">gives me this error:</div><div style="font-family:arial,helvetica,sans-serif"><br></div><div><div><font face="monospace, monospace">    • The type family ‘GreaterThan’ should have 2 arguments, but has been given</font></div><div><font face="monospace, monospace">none</font></div><div><font face="monospace, monospace">    • In the definition of data constructor ‘:::’</font></div><div><font face="monospace, monospace">      In the data type declaration for ‘Deck’</font></div><div style="font-family:arial,helvetica,sans-serif"><br></div></div><div><br>What's the best way to use higher order type families?</div><div><br></div><div>Thanks!</div><div>Matt Parsons</div><div><br></div><div>Here's the definitions I'm using for the above code:</div><div><div style="font-family:monospace,monospace"><br></div><div style="font-family:monospace,monospace">data Face </div><div style="font-family:monospace,monospace">    = One | Two | Three | Four | Five | Six | Seven | Eight | Nine </div><div style="font-family:monospace,monospace">    | Jack | Queen | King</div><div style="font-family:monospace,monospace">    deriving (Eq, Ord, Bounded, Enum) </div><div style="font-family:monospace,monospace"><br></div><div style="font-family:monospace,monospace">type family FaceOrd (a :: Face) (b :: Face) :: Ordering where</div><div style="font-family:monospace,monospace">    FaceOrd a a = 'EQ</div><div style="font-family:monospace,monospace">    FaceOrd a 'One = 'GT</div><div style="font-family:monospace,monospace">    FaceOrd 'One a = 'LT</div><div style="font-family:monospace,monospace">    FaceOrd a b = FaceOrd (PredFace a) (PredFace b)</div><div style="font-family:monospace,monospace"><br></div><div style="font-family:monospace,monospace">type family FaceGT (a :: Face) (b :: Face) :: Bool where</div><div style="font-family:monospace,monospace">    FaceGT a b = CompK a b == GT</div><div><br><div><font face="monospace, monospace">class GtK (a :: k) where</font></div><div><font face="monospace, monospace">    type GreaterThan (a :: k) (b :: k) :: Bool</font></div><br></div><div style="font-family:monospace,monospace">instance GtK (a :: Face) where</div><div style="font-family:monospace,monospace">    type GreaterThan a b = CompK a b == GT</div></div></div><div>
</div></div>