<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 -> eq</div><div>instance TypeEq a a True</div><div>-- instance TypeEq a b False</div><div>instance eq ~ False => TypeEq a b eq</div><div><br></div>
<div>f :: TypeEq Int Int True => 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 'True<br>
</div><div> arising from a use of `f'</div><div> Matching instances:</div><div> instance TypeEq k a a 'True -- Defined at Test.hs:14:24</div><div> instance eq ~ 'False => 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"><<a href="mailto:alexey.skladnoy@gmail.com" target="_blank">alexey.skladnoy@gmail.com</a>></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 <<a href="mailto:dasuraga@gmail.com">dasuraga@gmail.com</a>> wrote:<br>
> I think it might be impossible with type families. I don't think it's<br>
> possible to differentiate with type families something like T a a, and T a<br>
> b, with b different from a.<br>
><br>
</div>It'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's possible to use overlapping instances and fundeps.<br>
Implementation of type level equality is simple and it's only<br>
instances which need ovelap.<br>
<br>
-- | Type class for type equality.<br>
class TypeEq (a :: α) (b :: α) (eq :: Bool) | a b -> eq<br>
instance TypeEq a a True<br>
instance eq ~ False => TypeEq a b eq<br>
<br>
<br>
Implementation of lookup by key is relatively straightforward. Note<br>
that it doesn't check that key is unique.<br>
<br>
data k :> v<br>
infix 6 :><br>
<br>
-- | Lookup type for given key<br>
class TyLookup (map :: [*]) (k :: *) (v :: *) | map k -> v where<br>
<br>
class TyLookupCase (map :: [*]) (k :: *) (v :: *) (eq :: Bool) | map k<br>
eq -> v where<br>
<br>
instance ( TypeEq k k' eq<br>
, TyLookupCase (k :> v ': xs) k' v' eq<br>
) => TyLookup (k :> v ': xs) k' v' where<br>
<br>
instance TyLookupCase (k :> v ': xs) k v True where<br>
instance TyLookup xs k v => TyLookupCase (k' :> v' ': xs) k v False where<br>
</blockquote></div><br></div>