Hi Aleksey,
Unfortunately, your solution does not work for me (ghc 7.6.2). I reduced
the problem to:
-- | Type class for type equality.
class TypeEq (a :: α) (b :: α) (eq :: Bool) | a b -> eq
instance TypeEq a a True
-- instance TypeEq a b False
instance eq ~ False => TypeEq a b eq
f :: TypeEq Int Int True => Int
f = 1
When I try to invoke f, I get overlapping instances error:
Overlapping instances for TypeEq * Int Int 'True
arising from a use of `f'
Matching instances:
instance TypeEq k a a 'True -- Defined at Test.hs:14:24
instance eq ~ 'False => TypeEq k a b eq -- Defined at Test.hs:16:10
Thanks.
On Wed, Feb 27, 2013 at 12:17 PM, Aleksey Khudyakov <
alexey.sklad...@gmail.com> wrote:
> On 27 February 2013 12:01, Raphael Gaschignard <dasur...@gmail.com> wrote:
> > I think it might be impossible with type families. I don't think it's
> > possible to differentiate with type families something like T a a, and T
> a
> > b, with b different from a.
> >
> It's indeed impossible to write such type function using type
> families. It will be possible with new closed type familes (they are
> in GHC head already).
>
> But for now it's possible to use overlapping instances and fundeps.
> Implementation of type level equality is simple and it's only
> instances which need ovelap.
>
> -- | Type class for type equality.
> class TypeEq (a :: α) (b :: α) (eq :: Bool) | a b -> eq
> instance TypeEq a a True
> instance eq ~ False => TypeEq a b eq
>
>
> Implementation of lookup by key is relatively straightforward. Note
> that it doesn't check that key is unique.
>
> data k :> v
> infix 6 :>
>
> -- | Lookup type for given key
> class TyLookup (map :: [*]) (k :: *) (v :: *) | map k -> v where
>
> class TyLookupCase (map :: [*]) (k :: *) (v :: *) (eq :: Bool) | map k
> eq -> v where
>
> instance ( TypeEq k k' eq
> , TyLookupCase (k :> v ': xs) k' v' eq
> ) => TyLookup (k :> v ': xs) k' v' where
>
> instance TyLookupCase (k :> v ': xs) k v True where
> instance TyLookup xs k v => TyLookupCase (k' :> v' ': xs) k v False where
>
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
