{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE LinearTypes #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE Unsafe #-}
module Generics.Linear.Unsafe.ViaGHCGenerics
( GHCGenerically(..)
, GHCGenerically1(..)
) where
import Data.Coerce (Coercible, coerce)
import Data.Kind (Type)
import Generics.Linear
import qualified GHC.Generics as G
import Unsafe.Coerce
import GHC.Exts (Any)
import GHC.TypeLits (TypeError, ErrorMessage (..))
newtype GHCGenerically a = GHCGenerically { forall a. GHCGenerically a -> a
unGHCGenerically :: a }
instance G.Generic a => Generic (GHCGenerically a) where
type Rep (GHCGenerically a) = G.Rep a
to :: forall p (m :: Multiplicity).
Rep (GHCGenerically a) p %m -> GHCGenerically a
to = (Rep a p -> GHCGenerically a) %1 -> Rep a p %m -> GHCGenerically a
forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %1 -> a %q -> b
toLinear (a -> GHCGenerically a
forall a. a -> GHCGenerically a
GHCGenerically (a -> GHCGenerically a)
-> (Rep a p -> a) -> Rep a p -> GHCGenerically a
forall b c (p :: * -> * -> *) a.
Coercible b c =>
p b c -> (a -> b) -> a -> c
#. Rep a p -> a
forall a x. Generic a => Rep a x -> a
G.to)
from :: forall p (m :: Multiplicity).
GHCGenerically a %m -> Rep (GHCGenerically a) p
from = (GHCGenerically a -> Rep a p) %1 -> GHCGenerically a %m -> Rep a p
forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %1 -> a %q -> b
toLinear (a -> Rep a p
forall a x. Generic a => a -> Rep a x
G.from (a -> Rep a p)
-> (GHCGenerically a -> a) -> GHCGenerically a -> Rep a p
forall a b c (p :: * -> * -> *).
Coercible a b =>
(b -> c) -> p a b -> a -> c
.# GHCGenerically a -> a
forall a. GHCGenerically a -> a
unGHCGenerically)
toLinear
:: forall a b p q.
(a %p-> b) %1-> (a %q-> b)
toLinear :: forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %1 -> a %q -> b
toLinear a %p -> b
f = case forall {k} (a :: k) (b :: k). UnsafeEquality a b
forall (a :: Multiplicity) (b :: Multiplicity). UnsafeEquality a b
unsafeEqualityProof @p @q of
UnsafeEquality p q
UnsafeRefl -> a %p -> b
a %q -> b
f
infixr 9 #.
(#.) :: Coercible b c => p b c -> (a -> b) -> a -> c
#. :: forall b c (p :: * -> * -> *) a.
Coercible b c =>
p b c -> (a -> b) -> a -> c
(#.) p b c
_ = (a -> b) -> a -> c
coerce
infixl 8 .#
(.#) :: Coercible a b => (b -> c) -> p a b -> a -> c
b -> c
f .# :: forall a b c (p :: * -> * -> *).
Coercible a b =>
(b -> c) -> p a b -> a -> c
.# p a b
_ = (b -> c) -> a -> c
coerce b -> c
f
type GHCGenerically1 :: forall k. (k -> Type) -> k -> Type
newtype GHCGenerically1 f a = GHCGenerically1 { forall k (f :: k -> *) (a :: k). GHCGenerically1 f a -> f a
unGHCGenerically1 :: f a }
instance forall k (f :: k -> Type).
(forall (a :: k). G.Generic (f a)) => Generic1 (GHCGenerically1 f) where
type Rep1 (GHCGenerically1 (f :: k -> Type)) = MakeRep1 @k (G.Rep ((MarkOtherPars f) (LastPar :: k)))
to1 :: forall a m. Rep1 (GHCGenerically1 f) a %m-> GHCGenerically1 f a
to1 :: forall (p :: k) (m :: Multiplicity).
Rep1 (GHCGenerically1 f) p %m -> GHCGenerically1 f p
to1 = (Rep (f a) Any -> f a)
-> MakeRep1 (Rep (MarkOtherPars f LastPar)) a
%m -> GHCGenerically1 f a
forall a b. a -> b
unsafeCoerce (Rep (f a) Any -> f a
forall a x. Generic a => Rep a x -> a
G.to :: G.Rep (f a) Any -> f a)
from1 :: forall a m. GHCGenerically1 f a %m-> Rep1 (GHCGenerically1 f) a
from1 :: forall (p :: k) (m :: Multiplicity).
GHCGenerically1 f p %m -> Rep1 (GHCGenerically1 f) p
from1 = (f a -> Rep (f a) Any)
-> GHCGenerically1 f a
%m -> MakeRep1 (Rep (MarkOtherPars f LastPar)) a
forall a b. a -> b
unsafeCoerce (f a -> Rep (f a) Any
forall a x. Generic a => a -> Rep a x
G.from :: f a -> G.Rep (f a) Any)
data family LastPar :: k
data family OtherPar :: k -> k
type MakeRep1 :: forall k. (Type -> Type) -> k -> Type
type family MakeRep1 (rep :: Type -> Type) :: k -> Type where
MakeRep1 (M1 i c f) = M1 i c (MakeRep1 f)
MakeRep1 (x :+: y) = MakeRep1 x :+: MakeRep1 y
MakeRep1 (x :*: y) = MakeRep1 x :*: MakeRep1 y
MakeRep1 U1 = U1
MakeRep1 V1 = V1
MakeRep1 (Rec0 c) = MakeRep1Field (Rec0 (Unmark c)) Par1 c
type MarkOtherPars :: forall k. k -> k
type family MarkOtherPars (f :: k) :: k where
MarkOtherPars ((f :: j -> k) (a :: j)) = MarkOtherPars f (OtherPar a)
MarkOtherPars f = f
type Unmark :: forall k. k -> k
type family Unmark (f :: k) :: k where
Unmark LastPar = TypeError ('Text "Cannot create Generic1 instance: the last parameter appears in an invalid location.")
Unmark (OtherPar a) = a
Unmark ((f :: j -> k) (a :: j)) = Unmark f (Unmark a)
Unmark a = a
type MakeRep1Field :: forall j k. (k -> Type) -> (j -> Type) -> j -> k -> Type
type family MakeRep1Field fk acc c where
MakeRep1Field fk (acc :: k -> Type) (LastPar :: k) = acc
MakeRep1Field fk (_ :: b -> Type) (OtherPar _) = fk
MakeRep1Field fk (acc :: b -> Type) ((f :: a -> b) (x :: a)) = MakeRep1Field fk (acc :.: Unmark f) x
MakeRep1Field fk _ _ = fk