<div dir="ltr">Hi Aleksey,<div style><br></div><div style>Unfortunately, your solution does not work for me (ghc 7.6.2). I reduced the problem to:</div><div style><div><br></div><div>-- | Type class for type equality.</div>

<div>class  TypeEq (a :: α) (b :: α) (eq :: Bool) | a b -&gt; eq</div><div>instance               TypeEq a a True</div><div>-- instance TypeEq a b False</div><div>instance eq ~ False =&gt; TypeEq a b eq</div><div><br></div>

<div>f :: TypeEq Int Int True =&gt; Int</div><div>f = 1</div><div><br></div><div style>When I try to invoke f, I get overlapping instances error:</div><div style><div>    Overlapping instances for TypeEq * Int Int &#39;True<br>

</div><div>      arising from a use of `f&#39;</div><div>    Matching instances:</div><div>      instance TypeEq k a a &#39;True -- Defined at Test.hs:14:24</div><div>      instance eq ~ &#39;False =&gt; TypeEq k a b eq -- Defined at Test.hs:16:10</div>

<div><br></div><div style>Thanks.</div></div></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Wed, Feb 27, 2013 at 12:17 PM, Aleksey Khudyakov <span dir="ltr">&lt;<a href="mailto:alexey.skladnoy@gmail.com" target="_blank">alexey.skladnoy@gmail.com</a>&gt;</span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im">On 27 February 2013 12:01, Raphael Gaschignard &lt;<a href="mailto:dasuraga@gmail.com">dasuraga@gmail.com</a>&gt; wrote:<br>


&gt; I think it might be impossible with type families. I don&#39;t think it&#39;s<br>
&gt; possible to differentiate with type families something like T a a, and T a<br>
&gt; b, with b different from a.<br>
&gt;<br>
</div>It&#39;s indeed impossible to write such type function using type<br>
families. It will be possible with new closed type familes (they are<br>
in GHC head already).<br>
<br>
But for now it&#39;s possible to use overlapping instances and fundeps.<br>
Implementation of type level equality is simple and it&#39;s only<br>
instances which need ovelap.<br>
<br>
-- | Type class for type equality.<br>
class  TypeEq (a :: α) (b :: α) (eq :: Bool) | a b -&gt; eq<br>
instance               TypeEq a a True<br>
instance eq ~ False =&gt; TypeEq a b eq<br>
<br>
<br>
Implementation of lookup by key is relatively straightforward. Note<br>
that it doesn&#39;t check that key is unique.<br>
<br>
data k :&gt; v<br>
infix 6 :&gt;<br>
<br>
-- | Lookup type for given key<br>
class TyLookup (map :: [*]) (k :: *) (v :: *) | map k -&gt; v where<br>
<br>
class TyLookupCase (map :: [*]) (k :: *) (v :: *) (eq :: Bool) | map k<br>
eq -&gt; v where<br>
<br>
instance ( TypeEq k k&#39; eq<br>
         , TyLookupCase (k :&gt; v &#39;: xs) k&#39; v&#39; eq<br>
         ) =&gt; TyLookup  (k :&gt; v &#39;: xs) k&#39; v&#39; where<br>
<br>
instance                     TyLookupCase (k  :&gt; v  &#39;: xs) k v True  where<br>
instance TyLookup xs k v =&gt; TyLookupCase (k&#39; :&gt; v&#39; &#39;: xs) k v False where<br>
</blockquote></div><br></div>