Hello
What is the correct way to transform code that uses record selection
with TypeEq (like HList) to associated types? I keep running into
problems with overlapping type families which is not allowed unless
they match.
The fundep code:
class Select rec label val | rec label -> val
instance TypeEq label label True => Select (Label label val :+: rest) label val
instance (Select tail field val) => Select (any :+: tail) field val
And a conversion attempt:
class SelectT rec label where
type S rec label
instance TypeEq label label True => SelectT (Label label val :+: rest) label
where
type S (Label label val :+: rest) label = val
instance (SelectT tail field) => SelectT (any :+: tail) field where
type S (any :+: tail) field = S tail field
which fails with:
Conflicting family instance declarations:
type instance S (Label label val :+: rest) label
-- Defined at t.hs:19:9
type instance S (any :+: tail) field -- Defined at t.hs:23:9
How is it possible to get the TypeEq constraint into the type family?
Attached is a complete example that illustrates the problem.
- Taru Karttunen
{-# LANGUAGE
UndecidableInstances, OverlappingInstances, FunctionalDependencies,
TypeFamilies, TypeOperators, EmptyDataDecls, GADTs, MultiParamTypeClasses,
FlexibleInstances
#-}
-- Fundeps - this works
class Select rec label val | rec label -> val
instance TypeEq label label True => Select (Label label val :+: rest) label val
instance (Select tail field val) => Select (any :+: tail) field val
-- Associated types
class SelectT rec label where
type S rec label
instance TypeEq label label True => SelectT (Label label val :+: rest) label where
type S (Label label val :+: rest) label = val
-- THIS FAILS (comment to get this to compile):
instance (SelectT tail field) => SelectT (any :+: tail) field where
type S (any :+: tail) field = S tail field
{-
ERROR:
Conflicting family instance declarations:
type instance S (Label label val :+: rest) label
-- Defined at t.hs:19:9
type instance S (any :+: tail) field -- Defined at t.hs:23:9
-}
-- Support code, to get it compile
data True
data False
type family TypeEqR a b
type instance TypeEqR a a = True
class TypeEq a b result
instance (TypeEqR a b ~ isEq, Proxy2 isEq result) => TypeEq a b result
class Proxy2 inp out
instance (result ~ True) => Proxy2 True result
instance (result ~ False) => Proxy2 notTrue result
data End
data (:+:) a b
infixr :+:
newtype Rec wrap rtype = Rec (OuterWrap wrap (R wrap rtype))
type family InnerWrap wrap t :: *
type family OuterWrap wrap t :: *
data R wrap rtype where
End :: R wrap End
(:+:) :: InnerWrap wrap x -> R wrap xs -> R wrap (x :+: xs)
data Label l t
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
