module Data.Ruin.All (module Data.Ruin.All) where
import Control.DeepSeq (NFData(..))
import Data.Binary (Binary)
import Data.Data (Data)
import Data.Char (isSpace)
import Data.Functor.Compose
import Data.Functor.Identity
import Data.Kind
import Data.Serialize (Serialize)
import GHC.Exts (Constraint)
import GHC.Prim (Proxy#,proxy#)
import GHC.Generics
import GHC.TypeLits hiding (type (*))
import qualified Language.Haskell.TH as TH
import Language.Haskell.TH.Syntax (Lift(lift))
import Data.Ruin.Eval
import Data.Ruin.Internal
import Data.Ruin.Hoid
data Pair (l :: *) (r :: *) = MkPair l r
deriving (Lift)
instance (NFData l,NFData r) => NFData (Pair l r) where
rnf (MkPair l r) = rnf (l,r)
unPair :: Pair l r -> (l,r)
unPair (MkPair l r) = (l,r)
data Loc = Here | L Loc | R Loc
type family Find (rc :: *) (s :: Symbol) :: Maybe Loc where
Find (Pair l r) s = SearchBoth (Find l s) (Find r s)
Find rc s = FindViaFields (Fields rc) s
type family SearchBoth (l :: Maybe Loc) (r :: Maybe Loc) :: Maybe Loc where
SearchBoth ('Just loc) _ = 'Just ('L loc)
SearchBoth _ ('Just loc) = 'Just ('R loc)
SearchBoth _ _ = 'Nothing
type family FindViaFields (fields :: [(Symbol,*)]) (s :: Symbol) :: Maybe Loc where
FindViaFields '[] s = 'Nothing
FindViaFields ( '(s,ty) ': ss) s = 'Just 'Here
FindViaFields ( '(s1,ty) ': ss) s2 = FindViaFields ss s2
instance MightHave (Pair l r) (Find (Pair l r) s) (Pair l r) s (FieldType s (Pair l r)) => Has s (Pair l r) where
type FieldType s (Pair l r) = PairFieldType (Find (Pair l r) s) (Pair l r) s
extricate1 = \_ -> fmap (undub (mkLabel @s)) . mightExtricate1 @(Pair l r) @(Find (Pair l r) s)
type family PairFieldType (ml :: Maybe Loc) (rc :: *) (s :: Symbol) :: * where
PairFieldType ('Just 'Here) rc s = FieldType s rc
PairFieldType ('Just ('L loc)) (Pair l r) s = PairFieldType ('Just loc) l s
PairFieldType ('Just ('R loc)) (Pair l r) s = PairFieldType ('Just loc) r s
class MightHave
(top :: *)
(mloc :: Maybe Loc)
(rc :: *)
(s :: Symbol) (a :: *)
where
mightExtricate1 :: rc -> Eval (s :@ a)
type family Render (t :: *) :: ErrorMessage where
Render (Pair l r) = Render l ':$$: 'Text " or in the type" ':$$: Render r
Render t = 'Text " " ':<>: 'ShowType t
type NoSuchField (s :: Symbol) (top :: *) =
'Text "ruin: Could not find a field `"
':<>: 'Text s
':<>: 'Text "' in the type"
':$$: Render top
instance TypeError (NoSuchField s top) => MightHave top 'Nothing rc s a where
mightExtricate1 = undefined
instance MightHave top ('Just loc) l s a => MightHave top ('Just ('L loc)) (Pair l r) s a where
mightExtricate1 = mightExtricate1 @top @('Just loc) . (\(MkPair l _) -> l)
instance MightHave top ('Just loc) r s a => MightHave top ('Just ('R loc)) (Pair l r) s a where
mightExtricate1 = mightExtricate1 @top @('Just loc) . (\(MkPair _ r) -> r)
instance (Has s rc,a ~ FieldType s rc) => MightHave top ('Just 'Here) rc s a where
mightExtricate1 = fmap (dub s) . extricate1 s
where
s = mkLabel @s
type NoBuildPair =
'Text "ruin: `"
':<>: 'ShowType Pair
':<>: 'Text "' cannot be an instance of `"
':<>: 'ShowType Build
':<>: 'Text "'"
instance TypeError NoBuildPair => Build (Pair l r) where
type Fields (Pair l r) = Fields l ++ DifferenceByFst (Fields r) (FieldNames l)
build = undefined
buildNonStrict = undefined
type Shape (Pair l r) o = (Hoid Pair o,ZipShape (Pair l r) o)
type DisjointFields (a :: *) (b :: *) = MustBeDisjoint a b (Intersection (FieldNames a) (FieldNames b))
type family MustBeDisjoint (a :: *) (b :: *) (ss :: [Symbol]) :: Constraint where
MustBeDisjoint a b '[] = ()
MustBeDisjoint a b ss = TypeError (
'Text "ruin: The record types "
':$$: 'Text " " ':<>: 'ShowType a
':$$: 'Text "and"
':$$: 'Text " " ':<>: 'ShowType b
':$$: 'Text "must be disjoint, but both have these fields: " ':<>: 'ShowType ss
)
infixr 3 <@, `MkPair`
(<@) :: l -> r -> Pair l r
(<@) = MkPair
type FieldNames (t :: *) = MapFst (Fields t)
class Gives (s :: Symbol) (a :: *) (i :: * -> *) (rc :: *) where get :: rc -> Compose Eval i a
type family GivesThis (field :: (Symbol,*)) (i :: * -> *) (rc :: *) :: Constraint where
GivesThis f i rc = Gives (Fst f) (Snd f) i rc
type family GivesThese (fields :: [(Symbol,*)]) (i :: * -> *) (rc :: *) :: Constraint where
GivesThese '[] i rc = ()
GivesThese (f ': fs) i rc = (GivesThis f i rc,GivesThese fs i rc)
newtype GiveAllItHas rc = MkGiveAllItHas rc
instance (Applicative i,a ~ FieldType s rc,Has s rc) => Gives s a i (GiveAllItHas rc) where
get = \(MkGiveAllItHas rc) -> Compose $ pure <$> extricate1 (mkLabel @s) rc
newtype GiveAllItHasA rc = MkGiveAllItHasA rc
instance (i a ~ FieldType s rc,Has s rc) => Gives s a i (GiveAllItHasA rc) where
get = \(MkGiveAllItHasA rc) -> Compose $ extricate1 (mkLabel @s) rc
type rc `IsSubtypeOf` t = GivesThese (Fields t) Identity (GiveAllItHas rc)
class Build (t :: *) where
type Fields (t :: *) :: [(Symbol,*)]
type Fields t = GenericFields t
build :: (Applicative i,GivesThese (Fields t) i rc) => rc -> Compose Eval i t
buildNonStrict :: GivesThese (Fields t) Identity rc => rc -> t
default buildNonStrict ::
( Fields t ~ GenericFields t
, Generic t
, GenericBuild t (Rep t)
, GivesThese (Fields t) Identity rc
)
=> rc -> t
buildNonStrict = genericBuildNonStrict
type Shape (t :: *) (o :: *) :: Constraint
type Shape t o = GenericShape t o
type UnifyShape l r = (Shape l r,Shape r l)
asShapeOf :: UnifyShape l r => l -> r -> l
asShapeOf = const
type family UnifyFieldTypes (ss :: [Symbol]) (t :: *) (h :: *) :: Constraint where
UnifyFieldTypes '[] _ _ = ()
UnifyFieldTypes (s ': ss) t h = (FieldType s t ~ FieldType s h,UnifyFieldTypes ss t h)
asFieldTypesOf :: UnifyFieldTypes (FieldNames t) t rc => t -> proxy rc -> t
asFieldTypesOf = const
type family GenericShape (t :: k) (o :: *) :: Constraint where
GenericShape (f _) o = GenericShape f o
GenericShape t o = Hoid t o
type family ZipShape (tup :: k) (o :: k) :: Constraint where
ZipShape (f a) (g b) = (ZipShape f g,Shape a b)
ZipShape _ _ = ()
rup :: forall t rc. (Build t,rc `IsSubtypeOf` t) => rc -> t
rup = runEval . rupEval
rupA :: forall t rc i. (Applicative i,Build t,GivesThese (Fields t) i (GiveAllItHasA rc)) => rc -> i t
rupA = runEval . getCompose . build . MkGiveAllItHasA
rupEval :: forall t rc. (Build t,rc `IsSubtypeOf` t) => rc -> Eval t
rupEval = fmap runIdentity . getCompose . build . MkGiveAllItHas
rupNonStrict :: forall t rc. (Build t,rc `IsSubtypeOf` t) => rc -> t
rupNonStrict = buildNonStrict . MkGiveAllItHas
type GenericFields t = GFields (Rep t)
genericBuild ::
forall t rc i.
( Fields t ~ GenericFields t
, Applicative i
, Generic t
, GenericBuild t (Rep t)
, GivesThese (Fields t) i rc
)
=> rc -> Compose Eval i t
genericBuild = fmap to . gRup @t
genericBuildNonStrict ::
forall t rc.
( Fields t ~ GenericFields t
, Generic t
, GenericBuild t (Rep t)
, GivesThese (Fields t) Identity rc
)
=> rc -> t
genericBuildNonStrict = to . gBuildNonStrict @t
type NoFun t =
'Text "ruin: There is no meaningful instance of `"
':<>: 'ShowType t
':<>: 'Text "' for functions."
':$$: 'Text " Perhaps you omitted an argument?"
instance TypeError (NoFun Build) => Build (a -> b) where
type Fields (a -> b) = TypeError (NoFun Build)
build = undefined
buildNonStrict = undefined
instance Build () where
build rc = genericBuild rc
buildNonStrict rc = genericBuildNonStrict rc
instance Build (s :@ a) where
type Fields (s :@ a) = '[ '(s,a) ]
build = fmap (dub mkLabel) . get @s
buildNonStrict = runCEI . build
type Shape (s :@ _) o = Hoid ((:@) s) o
instance Build a => Build (Tup1 a) where
type Fields (Tup1 a) = Fields a
build = fmap MkTup1 . build
buildNonStrict = MkTup1 . buildNonStrict
type Shape (Tup1 a) o = (Hoid Tup1 o,ZipShape (Tup1 a) o)
type family ShapeTup1 (a :: *) (o :: *) where
ShapeTup1 a (Tup1 oa) = Shape a oa
instance
( DisjointFields a b
, Lemma_AppendGivesThese (Fields a)
, Build a
, Build b
) => Build (a,b) where
type Fields (a,b) = Fields a ++ Fields b
build :: forall i rc. (Applicative i,GivesThese (Fields (a,b)) i rc) => rc -> Compose Eval i (a,b)
build rc =
(,)
<$> lemmaFst @(Fields a) (proxy# :: Proxy# i) (proxy# :: Proxy# (Fields b)) build rc
<*> lemmaSnd @(Fields a) (proxy# :: Proxy# i) (proxy# :: Proxy# (Fields b)) build rc
buildNonStrict rc =
( lemmaFst @(Fields a) (proxy# :: Proxy# Identity) (proxy# :: Proxy# (Fields b)) buildNonStrict rc
, lemmaSnd @(Fields a) (proxy# :: Proxy# Identity) (proxy# :: Proxy# (Fields b)) buildNonStrict rc )
type Shape (a,b) o = (Hoid (,) o,ZipShape (a,b) o)
instance Build ((a,b),c) => Build (a,b,c) where
type Fields (a,b,c) = Fields (a,b) ++ Fields c
build = \rc -> assoc <$> build rc
where
assoc ((a,b),c) = (a,b,c)
buildNonStrict = \rc -> assoc (buildNonStrict rc)
where
assoc ~(~(a,b),c) = (a,b,c)
type Shape (a,b,c) o = (Hoid (,,) o,ZipShape (a,b,c) o)
instance Build ((a,b),(c,d)) => Build (a,b,c,d) where
type Fields (a,b,c,d) = Fields (a,b) ++ Fields (c,d)
build = \rc -> assoc <$> build rc
where
assoc ((a,b),(c,d)) = (a,b,c,d)
buildNonStrict = \rc -> assoc (buildNonStrict rc)
where
assoc ~(~(a,b),~(c,d)) = (a,b,c,d)
type Shape (a,b,c,d) o = (Hoid (,,,) o,ZipShape (a,b,c,d) o)
instance Build ((a,b,c),(d,e)) => Build (a,b,c,d,e) where
type Fields (a,b,c,d,e) = Fields (a,b,c) ++ Fields (d,e)
build = \rc -> assoc <$> build rc
where
assoc ((a,b,c),(d,e)) = (a,b,c,d,e)
buildNonStrict = \rc -> assoc (buildNonStrict rc)
where
assoc ~(~(a,b,c),~(d,e)) = (a,b,c,d,e)
type Shape (a,b,c,d,e) o = (Hoid (,,,,) o,ZipShape (a,b,c,d,e) o)
instance Build ((a,b,c),(d,e,f)) => Build (a,b,c,d,e,f) where
type Fields (a,b,c,d,e,f) = Fields (a,b,c) ++ Fields (d,e,f)
build = \rc -> assoc <$> build rc
where
assoc ((a,b,c),(d,e,f)) = (a,b,c,d,e,f)
buildNonStrict = \rc -> assoc (buildNonStrict rc)
where
assoc ~(~(a,b,c),~(d,e,f)) = (a,b,c,d,e,f)
type Shape (a,b,c,d,e,f) o = (Hoid (,,,,,) o,ZipShape (a,b,c,d,e,f) o)
instance Build ((a,b,c,d),(e,f,g)) => Build (a,b,c,d,e,f,g) where
type Fields (a,b,c,d,e,f,g) = Fields (a,b,c,d) ++ Fields (e,f,g)
build = \rc -> assoc <$> build rc
where
assoc ((a,b,c,d),(e,f,g)) = (a,b,c,d,e,f,g)
buildNonStrict = \rc -> assoc (buildNonStrict rc)
where
assoc ~(~(a,b,c,d),~(e,f,g)) = (a,b,c,d,e,f,g)
type Shape (a,b,c,d,e,f,g) o = (Hoid (,,,,,,) o,ZipShape (a,b,c,d,e,f,g) o)
instance Build ((a,b,c,d),(e,f,g,h)) => Build (a,b,c,d,e,f,g,h) where
type Fields (a,b,c,d,e,f,g,h) = Fields (a,b,c,d) ++ Fields (e,f,g,h)
build = \rc -> assoc <$> build rc
where
assoc ((a,b,c,d),(e,f,g,h)) = (a,b,c,d,e,f,g,h)
buildNonStrict = \rc -> assoc (buildNonStrict rc)
where
assoc ~(~(a,b,c,d),~(e,f,g,h)) = (a,b,c,d,e,f,g,h)
type Shape (a,b,c,d,e,f,g,h) o = (Hoid (,,,,,,,) o,ZipShape (a,b,c,d,e,f,g,h) o)
class Lemma_AppendGivesThese (fs1 :: [(Symbol,*)]) where
lemmaFst :: GivesThese (fs1 ++ fs2) i rc => Proxy# i -> Proxy# fs2 -> (GivesThese fs1 i rc => rc -> a) -> rc -> a
lemmaSnd :: GivesThese (fs1 ++ fs2) i rc => Proxy# i -> Proxy# fs2 -> (GivesThese fs2 i rc => rc -> a) -> rc -> a
instance Lemma_AppendGivesThese '[] where
lemmaFst _ _ k = k
lemmaSnd _ _ k = k
instance Lemma_AppendGivesThese fs1 => Lemma_AppendGivesThese (f ': fs1) where
lemmaFst i fs2 k = lemmaFst @fs1 i fs2 k
lemmaSnd i fs2 k = lemmaSnd @fs1 i fs2 k
type t `IsSymmetricRecordOf` rc =
( t `IsSubtypeOf` rc
, NoExtraFields t rc (FieldNames t) (FieldNames rc)
)
type family NoExtraFields (t :: *) (rc :: *) (sts :: [Symbol]) (srcs :: [Symbol]) :: Constraint where
NoExtraFields _ rc '[] '[] = MustHaveNoExtras rc (Difference '[] '[])
NoExtraFields _ rc (f ': fs) '[] = MustHaveNoExtras rc (Difference '[] (f ': fs))
NoExtraFields _ rc '[] (src ': srcs) = MustHaveNoExtras rc (Difference (src ': srcs) '[])
NoExtraFields _ rc (f ': fs) (src ': srcs) = MustHaveNoExtras rc (Difference (src ': srcs) (f ': fs))
type family MustHaveNoExtras (rc :: *) (ss :: [Symbol]) :: Constraint where
MustHaveNoExtras rc '[] = ()
MustHaveNoExtras rc ss = TypeError (
'Text "ruin: The argument type"
':$$: 'Text " " ':<>: 'ShowType rc
':$$: 'Text "has unused fields: " ':<>: 'ShowType ss
)
rsym ::
(l `IsSymmetricRecordOf` r,Build r)
=> l -> r
rsym = rup
rto :: forall h t rc. (Hoid h t,rc `IsSymmetricRecordOf` t,Build t) => rc -> t
rto = hoid @h . rsym
rfrom :: forall h rc t. (Hoid h rc,rc `IsSymmetricRecordOf` t,Build t) => rc -> t
rfrom = rsym . hoid @h
prto :: forall h t rc. (Hoid h t,rc `IsSymmetricRecordOf` t,Build t) => Proxy# h -> rc -> t
prto _ = rto @h
prtoA ::
forall h t rc i.
(Hoid h t,Applicative i,SymmetricRecordsA t i rc,Build t)
=> Proxy# h
-> rc -> i t
prtoA _ = rtoA @h
prfrom :: forall h rc t. (Hoid h rc,rc `IsSymmetricRecordOf` t,Build t) => Proxy# h -> rc -> t
prfrom _ = rfrom @h
rsymA ::
(Applicative i,SymmetricRecordsA t i rc,Build t)
=> rc -> i t
rsymA = rupA
rtoA ::
forall h t rc i.
(Hoid h t,Applicative i,SymmetricRecordsA t i rc,Build t)
=> rc -> i t
rtoA = rsymA
rfromA ::
forall h rc t i.
(Hoid h rc,Applicative i,SymmetricRecordsA t i rc,Build t)
=> rc -> i t
rfromA = rsymA . hoid @h
type SymmetricRecordsA t i rc =
( GivesThese (Fields t) i (GiveAllItHasA rc)
, NoExtraFields t rc (FieldNames t) (FieldNames rc)
)
type family GFields (rep :: * -> *) :: [(Symbol,*)] where
GFields (M1 D c rep) = GFields rep
GFields (M1 C c rep) = GFields rep
GFields (M1 S ('MetaSel ('Just s) su ss ds) (K1 i c)) = '[ '(s,c) ]
GFields (l :*: r) = GFields l ++ GFields r
GFields U1 = '[]
class GenericBuild (top :: *) (rep :: * -> *) where
gRup :: (Applicative i,GivesThese (GFields rep) i rc) => rc -> Compose Eval i (rep x)
gBuildNonStrict :: GivesThese (GFields rep) Identity rc => rc -> rep x
type NoConstructors (dn :: Symbol) =
'Text "ruin: Cannot derive "
':<>: 'ShowType Build
':<>: 'Text " for `"
':<>: 'Text dn
':<>: 'Text "' because it doesn't have any constructors."
instance TypeError (NoConstructors dn) => GenericBuild top (M1 D ('MetaData dn mn pn nt) V1) where
gRup = undefined
gBuildNonStrict = undefined
type TooManyConstructors (dn :: Symbol) =
'Text "ruin: Cannot derive "
':<>: 'ShowType Build
':<>: 'Text " for `"
':<>: 'Text dn
':<>: 'Text "' because it has more than one constructor."
instance TypeError (TooManyConstructors dn) => GenericBuild top (M1 D ('MetaData dn mn pn nt) (l :+: r)) where
gRup = undefined
gBuildNonStrict = undefined
instance GenericBuildConArgs top dn rep => GenericBuild top (M1 D ('MetaData dn mn pn nt) (M1 C c rep)) where
gRup rc = (M1 . M1) <$> gRupConArgs @top @dn rc
gBuildNonStrict rc = M1 (M1 (gBuildNonStrictConArgs @top @dn rc))
class GenericBuildConArgs (top :: *) (dn :: Symbol) (rep :: * -> *) where
gRupConArgs :: (Applicative i,GivesThese (GFields rep) i rc) => rc -> Compose Eval i (rep x)
gBuildNonStrictConArgs :: GivesThese (GFields rep) Identity rc => rc -> rep x
instance (Lemma_AppendGivesThese (GFields l),GenericBuildConArgs top dn l,GenericBuildConArgs top dn r) => GenericBuildConArgs top dn (l :*: r) where
gRupConArgs :: forall i rc x. (Applicative i,GivesThese (GFields (l :*: r)) i rc) => rc -> Compose Eval i ((l :*: r) x)
gRupConArgs rc =
(:*:)
<$> lemmaFst @(GFields l) (proxy# :: Proxy# i) (proxy# :: Proxy# (GFields r)) (gRupConArgs @top @dn) rc
<*> lemmaSnd @(GFields l) (proxy# :: Proxy# i) (proxy# :: Proxy# (GFields r)) (gRupConArgs @top @dn) rc
gBuildNonStrictConArgs rc =
lemmaFst @(GFields l) (proxy# :: Proxy# Identity) (proxy# :: Proxy# (GFields r)) (gBuildNonStrictConArgs @top @dn) rc
:*: lemmaSnd @(GFields l) (proxy# :: Proxy# Identity) (proxy# :: Proxy# (GFields r)) (gBuildNonStrictConArgs @top @dn) rc
type NotBuildSyntax (dn :: Symbol) =
'Text "ruin: Cannot derive "
':<>: 'ShowType Build
':<>: 'Text " for `"
':<>: 'Text dn
':<>: 'Text "' because its definition doesn't use record type syntax."
instance TypeError (NotBuildSyntax dn) => GenericBuildConArgs top dn (M1 S ('MetaSel 'Nothing su ss ds) rep) where
gRupConArgs = undefined
gBuildNonStrictConArgs = undefined
instance (Has s top,rep ~ K1 i c) => GenericBuildConArgs top dn (M1 S ('MetaSel ('Just s) su ss ds) rep) where
gRupConArgs = fmap (M1 . K1) . get @s
gBuildNonStrictConArgs = M1 . K1 . runCEI . get @s
instance GenericBuildConArgs top dn U1 where
gRupConArgs _ = pure U1
gBuildNonStrictConArgs _ = U1
class Has (s :: Symbol) (t :: *) where
type FieldType s t :: *
type FieldType s t = GenericFieldType s t
extricate1 :: Label s -> t -> Eval (FieldType s t)
default extricate1 :: (Generic t,GBox (IsABox (Rep t)) t,GenericHas (Rep t) s (FieldType s t)) => Label s -> t -> Eval (FieldType s t)
extricate1 = genericExtricate1
type GenericFieldType s t = GFieldType (GFind (Rep t) s) (Rep t)
genericExtricate1 ::
forall s t.
(Generic t,GBox (IsABox (Rep t)) t,GenericHas (Rep t) s (FieldType s t))
=> Label s -> t -> Eval (FieldType s t)
genericExtricate1 = \_ t -> fmap (undub (mkLabel @s)) $ fromEval @(IsABox (Rep t)) t >>= gExtricate1
type family IsABox (rep :: * -> *) :: Bool where
IsABox (M1 D ('MetaData _ _ _ 'False) (M1 C c (M1 S s (K1 k a)))) = 'True
IsABox _ = 'False
class GBox (isABox :: Bool) (t :: *) where
fromEval :: t -> Eval (Rep t x)
instance Generic t => GBox 'False t where
fromEval = pure . from
instance Generic t => GBox 'True t where
fromEval t = t `seq` pure (from t)
type family GFieldType (ml :: Maybe Loc) (rep :: * -> *) :: * where
GFieldType ('Just 'Here) (M1 S ('MetaSel ('Just s) su ss ds) (K1 i c)) = c
GFieldType ('Just loc) (M1 i c rep) = GFieldType ('Just loc) rep
GFieldType ('Just ('L loc)) (l :*: r) = GFieldType ('Just loc) l
GFieldType ('Just ('R loc)) (l :*: r) = GFieldType ('Just loc) r
instance TypeError (NoFun Has) => Has s (a -> b) where
type FieldType s (a -> b) = TypeError (NoFun Has)
extricate1 = undefined
instance TypeError (NoSuchField s ()) => Has s () where
type FieldType s () = TypeError (NoSuchField s ())
extricate1 = undefined
infix 1 :@
newtype (s :: Symbol) :@ (a :: *) = Dub a
deriving (Binary,Data,Eq,Functor,Generic,Generic1,NFData,Ord,Serialize)
type family SingletonType (singleton :: *) :: * where SingletonType (_ :@ a) = a
type family FunctorType (fa :: *) :: * -> * where FunctorType (f _) = f
instance (s1 ~ s2) => Has s1 (s2 :@ a) where
type FieldType s1 (s2 :@ a) = a
extricate1 = \_ -> pure . undub mkLabel
instance (Lift a,KnownSymbol s) => Lift (s :@ a) where
lift (Dub a) =
[| dub (mkLabel :: Label $(TH.litT (TH.strTyLit s))) a |]
where
s = symbolVal' (proxy# :: Proxy# s)
instance (KnownSymbol s,Show a) => Show (s :@ a) where
showsPrec d (Dub a) = showParen (d > app_prec) $
prefix . showsPrec (app_prec+1) a
where
app_prec = 10
prefix
| hasEscapes || hasSpaces = showString "dub (mkLabel @" . showString s' . showString ") "
| otherwise = showString "dub #" . showString s . showString " "
s = symbolVal' (proxy# :: Proxy# s)
s' = show s
hasEscapes = s' /= '"' : s ++ ['"']
hasSpaces = any isSpace s
dub :: Label s -> a -> s :@ a
dub = \_ -> Dub
undub :: Label s -> s :@ a -> a
undub = \_ (Dub a) -> a
class GenericHas (rep :: * -> *) (s :: Symbol) (a :: *) where
gExtricate1 :: rep x -> Eval (s :@ a)
instance GArgsHas dn (GFind conargs s) conargs s a => GenericHas (M1 D ('MetaData dn mn pn nt) (M1 C c conargs)) s a where
gExtricate1 = gArgsExtricate1 @dn @(GFind conargs s) . unM1 . unM1
type Not1ConstructorMessage (dn :: Symbol) =
'Text "ruin: The type `"
':<>: 'Text dn
':<>: 'Text "' must have exactly one constructor to derive `"
':<>: 'ShowType Has
':<>: 'Text "'"
instance TypeError (Not1ConstructorMessage dn) => GenericHas (M1 D ('MetaData dn mn pn nt) (l :+: r)) s a where
gExtricate1 = undefined
instance TypeError (Not1ConstructorMessage dn) => GenericHas (M1 D ('MetaData dn mn pn nt) V1) s a where
gExtricate1 = undefined
type family GFind (rep :: * -> *) (s :: Symbol) :: Maybe Loc where
GFind (M1 S ('MetaSel ('Just s) su ss ds) rep) s = 'Just 'Here
GFind (M1 i c rep) s = GFind rep s
GFind (l :*: r) s = MergeLoc (GFind l s) (GFind r s)
GFind rep s = 'Nothing
type family MergeLoc (l :: Maybe Loc) (r :: Maybe Loc) :: Maybe Loc where
MergeLoc 'Nothing 'Nothing = 'Nothing
MergeLoc 'Nothing ('Just r) = 'Just ('R r)
MergeLoc ('Just l) _ = 'Just ('L l)
class GArgsHas (dn :: Symbol) (ml :: Maybe Loc) (rep :: * -> *) (s :: Symbol) (a :: *) where
gArgsExtricate1 :: rep x -> Eval (s :@ a)
type NoSuchSelector (dn :: Symbol) (s :: Symbol) =
'Text "ruin: The type `"
':<>: 'Text dn
':<>: 'Text "' must declare a record selector named `"
':<>: 'Text s
':<>: 'Text "' to derive `"
':<>: 'ShowType Has
':<>: 'Text " "
':<>: 'ShowType s
':<>: 'Text "'"
instance TypeError (NoSuchSelector dn s) => GArgsHas dn 'Nothing rep s a where
gArgsExtricate1 = undefined
instance (rep ~ K1 i a) => GArgsHas dn ('Just 'Here) (M1 S ('MetaSel ('Just s) su ss ds) rep) s a where
gArgsExtricate1 = pure . dub mkLabel . unK1 . unM1
instance GArgsHas dn ('Just loc) l s a => GArgsHas dn ('Just ('L loc)) (l :*: r) s a where
gArgsExtricate1 (l :*: _) = gArgsExtricate1 @dn @('Just loc) l
instance GArgsHas dn ('Just loc) r s a => GArgsHas dn ('Just ('R loc)) (l :*: r) s a where
gArgsExtricate1 (_ :*: r) = gArgsExtricate1 @dn @('Just loc) r
instance Has s a => Has s (Tup1 a) where
type FieldType s (Tup1 a) = FieldType s a
extricate1 s = \(MkTup1 x) -> extricate1 s x
instance (DisjointFields a b,Has s (Pair a b)) => Has s (a,b) where
type FieldType s (a,b) = FieldType s (Pair a b)
extricate1 s = extricate1 s . uncurry (<@)
instance Has s ((a,b),c) => Has s (a,b,c) where
type FieldType s (a,b,c) = FieldType s ((a,b),c)
extricate1 = \s -> extricate1 s . reassoc
where
reassoc (a,b,c) = ((a,b),c)
instance Has s ((a,b),(c,d)) => Has s (a,b,c,d) where
type FieldType s (a,b,c,d) = FieldType s ((a,b),(c,d))
extricate1 = \s -> extricate1 s . reassoc
where
reassoc (a,b,c,d) = ((a,b),(c,d))
instance Has s ((a,b,c),(d,e)) => Has s (a,b,c,d,e) where
type FieldType s (a,b,c,d,e) = FieldType s ((a,b,c),(d,e))
extricate1 = \s -> extricate1 s . reassoc
where
reassoc (a,b,c,d,e) = ((a,b,c),(d,e))
instance Has s ((a,b,c),(d,e,f)) => Has s (a,b,c,d,e,f) where
type FieldType s (a,b,c,d,e,f) = FieldType s ((a,b,c),(d,e,f))
extricate1 = \s -> extricate1 s . reassoc
where
reassoc (a,b,c,d,e,f) = ((a,b,c),(d,e,f))
instance Has s ((a,b,c,d),(e,f,g)) => Has s (a,b,c,d,e,f,g) where
type FieldType s (a,b,c,d,e,f,g) = FieldType s ((a,b,c,d),(e,f,g))
extricate1 = \s -> extricate1 s . reassoc
where
reassoc (a,b,c,d,e,f,g) = ((a,b,c,d),(e,f,g))
instance Has s ((a,b,c,d),(e,f,g,h)) => Has s (a,b,c,d,e,f,g,h) where
type FieldType s (a,b,c,d,e,f,g,h) = FieldType s ((a,b,c,d),(e,f,g,h))
extricate1 = \s -> extricate1 s . reassoc
where
reassoc (a,b,c,d,e,f,g,h) = ((a,b,c,d),(e,f,g,h))
fieldLabelsOf :: forall t proxy. proxy t -> Labels (FieldNames t)
fieldLabelsOf _ = mkLabels @(FieldNames t)