Thanks for your answers, Anthony and Erik.<br><br>I&#39;ll try with fundeps. I know about HList, but back at the time when I looked at it I found quite complex.<br><br>Anthony, the link you gave me [1] tends to show that actually Bool type is promoted.<br>


<br><span style="font-family:courier new,monospace">type family Member x (l :: [*]) :: Bool</span><br><span style="font-family:courier new,monospace">type instance Member x (x &#39;: xs) = True</span><br>works.<br>So if I understand well, unlike what I thought when I saw the compilation fail, the two x&#39;s type variables are actually unified, but then the second instance<br>

<span style="font-family:courier new,monospace">type instance Member x (y &#39;: xs) = True</span><br>encompasses the first, so GHC refuses to handle it (as it would at the value level with regular case expressions).<br>
So yes, [1] is exactly what I was trying to do.<br>
<br>Out of curiosity, I tried with Int, and it works too, I can express:<br><span style="font-family:courier new,monospace">type family Something a :: Int</span><br>But then, the following doesn&#39;t compile<br><span style="font-family:courier new,monospace">type instance Something String = 42</span><br>


( <span style="font-family:courier new,monospace"><span style="font-family:arial,helvetica,sans-serif">The wild guess</span> &#39;42</span> does not either ) So I guess we don&#39;t have type-level integers for now. How are promoted Ints usable then?<br>

<br><br><a href="http://hackage.haskell.org/trac/ghc/wiki/NewAxioms" target="_blank">[1] http://hackage.haskell.org/trac/ghc/wiki/NewAxioms</a><br><br>
<br><div class="gmail_quote">2012/6/8 AntC <span dir="ltr">&lt;<a href="mailto:anthony_clayden@clear.net.nz" target="_blank">anthony_clayden@clear.net.nz</a>&gt;</span><br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">


Yves Parès &lt;yves.pares &lt;at&gt; <a href="http://gmail.com" target="_blank">gmail.com</a>&gt; writes:<br>
<br>
&gt;<br>
&gt; The doc page <a href="http://www.haskell.org/ghc/docs/7.4.1/html/users_guide/kind-" target="_blank">http://www.haskell.org/ghc/docs/7.4.1/html/users_guide/kind-</a><br>
<div>polymorphism-and-promotion.html#promotion show that lists are now usable as<br>
</div>types.So I&#39;m trying to make a type level function to test if a type list<br>
<div>contains a type. Unless I&#39;m wrong, that calls to the use of a type family.<br>
<br>
{-# LANGUAGE DataKinds, TypeOperators, KindSignatures, TypeFamilies #-}<br>
data HBool = HTrue | HFalse<br>
  -- Mandatory as Bool type is not currently promoted to a kind<br>
<br>
type family Member x (l :: [*]) :: HBool<br>
<br>
type instance Member x (x &#39;: xs) = HTrue<br>
type instance Member x (y &#39;: xs) = Member x xs<br>
type instance Member x (y &#39;: &#39;[]) = HFalse<br>
<br>
&gt;But the compiler complains about my instance conflicting.<br>
<br>
</div>Hi Yves, always when you&#39;re asking a question like this, give the error<br>
message in full -- usually it will explain what&#39;s wrong.<br>
<br>
In this case I can guess: you have overlapping instances (the first overlaps<br>
the second, the third overlaps the second), which are not allowed for type<br>
functions (currently -- unless the equations are confluent).<br>
<br>
There&#39;s some early work on introducing overlaps to type functions (in a<br>
controlled way). <a href="http://hackage.haskell.org/trac/ghc/wiki/NewAxioms" target="_blank">http://hackage.haskell.org/trac/ghc/wiki/NewAxioms</a><br>
<br>
And as it happens, several threads are going on in the lists re options and<br>
implications.<br>
<div><br>
&gt; Is what I&#39;m trying to do feasible?<br>
<br>
</div>Promoted lists are really just the same as HLists, but using the standard<br>
Haskell syntax.<br>
<br>
A membership test is feasible with FunDeps (because they do allow overlaps),<br>
but I guess you know the HList stuff, judging from your HBool. It&#39;s feasible<br>
using type equality constraints to achieve the same as HList (so ~ is<br>
equivalent to HList&#39;s TypeCast), also with overlaps.<br>
<div><br>
<br>
&gt;Second question: how can type level tuples (also mentioned in the doc page)<br>
be exploited? Aren&#39;t they redundant with type-level lists?<br>
<br>
</div>Type-level tuples are fixed length, and provide a flat structure (any element<br>
is equally accessible), whereas lists are expandable, with a nested structure<br>
that means you have to scan down the structure to get to the element you want.<br>
<br>
AntC<br>
<br>
<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org" target="_blank">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
</blockquote></div><br>