I think there’s a bug in it, because you are coercing the label := ty to ty. Edit: or I guess you could just store the ty directly in the any when constructing these?
But my immediate thought was that you can do this safely with a GADT:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedRecordDot #-}
import GHC.Records
import GHC.TypeLits
import Data.Proxy
import Data.Kind
type (:=) :: Symbol -> Type -> Type
data label := ty = (KnownSymbol label) => Proxy label := ty
type Row :: [Type] -> Type
data Row xs where
RNil :: Row '[]
RCons :: x -> Row xs -> Row ((l := x) : xs)
instance HasField l (Row ((l := t) : e)) t where
getField (RCons x _) = x
{-# INLINE getField #-}
instance HasField l (Row (_0 : (l := t) : e)) t where
getField (RCons _ (RCons x _)) = x
{-# INLINE getField #-}
foo :: Row ["x" := Int, "y" := Int]
foo = RCons 1 (RCons 2 RNil)
bar :: Int
bar = foo.y
foo2 :: Row ["x" := Int, "x" := Int]
foo2 = RCons 1 (RCons 2 RNil)
bar2 :: Int
bar2 = foo2.x
I’m honestly surprised GHC does not complain about overlapping even if I use the same label name multiple times. Nevermind, it does:
Row.hs:36:8: error:
• Overlapping instances for HasField
"x" (Row '["x" := Int, "x" := Int]) Int
arising from selecting the field ‘x’
Matching instances:
instance HasField l (Row (_0 : (l := t) : e)) t
-- Defined at Row.hs:22:10
instance HasField l (Row ((l := t) : e)) t
-- Defined at Row.hs:18:10
• In the expression: foo2.x
In an equation for ‘bar2’: bar2 = foo2.x
|
36 | bar2 = foo2.x
| ^^^^^^