Hi Jan, One example is https://github.com/haskell/vector/issues/34
I see lots of potential uses in HList. For example in HZip.hs there's a Zip using type families: type family HZipR (x::[*]) (y::[*]) :: [*] type instance HZipR '[] '[] = '[] type instance HZipR (x ': xs) (y ': ys) = (x,y) ': HZipR xs ys If there was no need to write some additional type families that tell ghc how to find x and y given HZipR x y, then the version using TFs might be as good as the version using FDs (defined in HList.hs) I don't know how realistic this is but a constraint (HLength x ~ HLength y) would ideally have the same result as SameLength x y. Copy-paste into ghci: :set +t -XDataKinds -XFlexibleContexts -XTypeFamilies import Data.HList let desired = Proxy :: SameLength x '[(),()] => Proxy x let current = Proxy :: (HLength y ~ HLength '[(),()]) => Proxy y Prints desired :: Proxy '[y, y1] current :: HLength y ~ 'HSucc ('HSucc 'HZero) => Proxy y Regards, Adam On Mon, Feb 9, 2015 at 10:58 AM, Jan Stolarek <jan.stola...@p.lodz.pl> wrote: > Haskellers, > > I am finishing work on adding injective type families to GHC. I know that in > the past many people > have asked for this feature. If you have use cases for injective type > families I would appreciate > if you could show them to me. My implementation has some restrictions and I > want to see how > severe these restrictions are from a practical point of view. > > Janek > > --- > Politechnika Łódzka > > Treść tej wiadomości zawiera informacje przeznaczone tylko dla adresata. > Jeżeli nie jesteście Państwo jej adresatem, bądź otrzymaliście ją przez > pomyłkę > prosimy o powiadomienie o tym nadawcy oraz trwałe jej usunięcie. > _______________________________________________ > Haskell-Cafe mailing list > haskell-c...@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users