{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-unused-top-binds #-}
module Data.Generic.Labels.Internal.Errors
( AdaptLabelMessage
, CheckAdapt, CheckInject, CheckProject
)
where
import Data.Kind
( Constraint, Type )
import GHC.Generics
import GHC.TypeLits
( Symbol
, TypeError, ErrorMessage(..)
)
import Data.Generics.Product.Internal.GLens
( Eval, TyFun )
import Data.Label
( (:=) )
import Data.Type.Error
( ErrorIfAmbiguous, MessageIfNonEmpty, ThrowMessagesWithHeader )
import Data.Type.List
( (:++:), Intersect, Remove )
import Data.Type.Maybe
( CatMaybes )
import Data.Type.Multiplicity
( Mult ( None, One, Many ) )
import {-# SOURCE #-} Data.Generic.Labels
( Adapt(..), Inject(..), Project(..)
, UncheckedAdapt(..), UncheckedInject(..), UncheckedProject(..)
)
type AdaptLabelMessage :: Symbol -> Maybe Type -> Maybe Type -> Type -> Constraint
type family AdaptLabelMessage lbl mb_argTy mb_optTy allTy where
AdaptLabelMessage _ Nothing Nothing ty = ( () :: Constraint )
AdaptLabelMessage _ ( Just ty ) Nothing ty = ( () :: Constraint )
AdaptLabelMessage _ Nothing ( Just ty ) ty = ( () :: Constraint )
AdaptLabelMessage _ ( Just ty ) ( Just ty ) ty = ( () :: Constraint )
AdaptLabelMessage lbl ( Just a ) Nothing b =
TypeError
( Text "Mismatched types at label #" :<>: Text lbl :<>: Text "."
:$$: Text " Expected type: " :<>: ShowType b
:$$: Text " Provided type: " :<>: ShowType a
)
AdaptLabelMessage lbl Nothing ( Just o ) b =
TypeError
( Text "Mismatched types at label #" :<>: Text lbl :<>: Text "."
:$$: Text " Expected type: " :<>: ShowType b
:$$: Text " Optional type: " :<>: ShowType o
)
AdaptLabelMessage lbl ( Just a ) ( Just o ) b =
TypeError
( Text "Mismatched types at label #" :<>: Text lbl :<>: Text "."
:$$: Text " Expected type: " :<>: ShowType b
:$$: Text " Provided type: " :<>: ShowType a
:$$: Text " Optional type: " :<>: ShowType o
)
type CheckAdapt :: Type -> Type -> Type -> Constraint
type family CheckAdapt args opt all where
CheckAdapt a a a = ( () :: Constraint )
CheckAdapt a opt a = ( () :: Constraint )
CheckAdapt ( lbl := a ) ( lbl := o ) ( lbl := b ) =
( AdaptLabelMessage lbl ( Just a ) ( Just o ) b, a ~ b, o ~ b )
CheckAdapt ( lbl := a ) opt ( lbl := b ) =
( AdaptLabelMessage lbl ( Just a ) Nothing b, a ~ b )
CheckAdapt ( lbl1 := arg ) ( lbl2 := opt ) all =
( ProperAdapt arg opt all
( CollectLeaves ( S1 ( MetaSel ( Just lbl1 ) NoSourceUnpackedness NoSourceStrictness DecidedLazy ) ( Rec0 arg ) ) )
( CollectLeaves ( S1 ( MetaSel ( Just lbl2 ) NoSourceUnpackedness NoSourceStrictness DecidedLazy ) ( Rec0 opt ) ) )
( CollectLeaves ( Rep all ) )
, ErrorIfAmbiguous ( Rep all )
( TypeError
( Text "No instance for " :<>: ShowType ( Generic all )
:$$: Text "arising from the constraint " :<>: ShowType ( Adapt ( lbl1 := arg ) ( lbl2 := opt ) all )
)
)
( () :: Constraint )
)
CheckAdapt ( lbl := arg ) opt all =
( ProperAdapt arg opt all
( CollectLeaves ( S1 ( MetaSel ( Just lbl ) NoSourceUnpackedness NoSourceStrictness DecidedLazy ) ( Rec0 arg ) ) )
( CollectLeaves ( Rep opt ) )
( CollectLeaves ( Rep all ) )
, ErrorIfAmbiguous ( Rep opt )
( TypeError
( Text "No instance for " :<>: ShowType ( Generic opt )
:$$: Text "arising from the constraint " :<>: ShowType ( Adapt ( lbl := arg ) opt all )
)
)
( () :: Constraint )
, ErrorIfAmbiguous ( Rep all )
( TypeError
( Text "No instance for " :<>: ShowType ( Generic all )
:$$: Text "arising from the constraint " :<>: ShowType ( Adapt ( lbl := arg ) opt all )
)
)
( () :: Constraint )
)
CheckAdapt args ( lbl := opt ) all =
( ProperAdapt args opt all
( CollectLeaves ( Rep args ) )
( CollectLeaves ( S1 ( MetaSel ( Just lbl ) NoSourceUnpackedness NoSourceStrictness DecidedLazy ) ( Rec0 opt ) ) )
( CollectLeaves ( Rep all ) )
, ErrorIfAmbiguous ( Rep args )
( TypeError
( Text "No instance for " :<>: ShowType ( Generic args )
:$$: Text "arising from the constraint " :<>: ShowType ( Adapt args ( lbl := opt ) all )
)
)
( () :: Constraint )
, ErrorIfAmbiguous ( Rep all )
( TypeError
( Text "No instance for " :<>: ShowType ( Generic all )
:$$: Text "arising from the constraint " :<>: ShowType ( Adapt args ( lbl := opt ) all )
)
)
( () :: Constraint )
)
CheckAdapt args opt all =
( ProperAdapt args opt all
( CollectLeaves ( Rep args ) ) ( CollectLeaves ( Rep opt ) ) ( CollectLeaves ( Rep all ) )
, ErrorIfAmbiguous ( Rep args )
( TypeError
( Text "No instance for " :<>: ShowType ( Generic args )
:$$: Text "arising from the constraint " :<>: ShowType ( Adapt args opt all )
)
)
( () :: Constraint )
, ErrorIfAmbiguous ( Rep opt )
( TypeError
( Text "No instance for " :<>: ShowType ( Generic opt )
:$$: Text "arising from the constraint " :<>: ShowType ( Adapt args opt all )
)
)
( () :: Constraint )
, ErrorIfAmbiguous ( Rep all )
( TypeError
( Text "No instance for " :<>: ShowType ( Generic all )
:$$: Text "arising from the constraint " :<>: ShowType ( Adapt args opt all )
)
)
( () :: Constraint )
)
type CheckInject :: Type -> Type -> Constraint
type family CheckInject small big where
CheckInject a a = ( () :: Constraint )
CheckInject small big =
( ProperInjection small big ( CollectLeaves ( Rep small ) ) ( CollectLeaves ( Rep big ) )
, ErrorIfAmbiguous ( Rep small )
( TypeError
( Text "No instance for " :<>: ShowType ( Generic small )
:$$: Text "arising from the constraint " :<>: ShowType ( Inject small big )
)
)
( () :: Constraint )
, ErrorIfAmbiguous ( Rep big )
( TypeError
( Text "No instance for " :<>: ShowType ( Generic big )
:$$: Text "arising from the constraint " :<>: ShowType ( Inject small big )
)
)
( () :: Constraint )
)
type CheckProject :: Type -> Type -> Constraint
type family CheckProject big small where
CheckProject a a = ( () :: Constraint )
CheckProject big small =
( ProperProjection big small ( CollectLeaves ( Rep big ) ) ( CollectLeaves ( Rep small ) )
, ErrorIfAmbiguous ( Rep big )
( TypeError
( Text "No instance for " :<>: ShowType ( Generic big )
:$$: Text "arising from the constraint " :<>: ShowType ( Project big small )
)
)
( () :: Constraint )
, ErrorIfAmbiguous ( Rep small )
( TypeError
( Text "No instance for " :<>: ShowType ( Generic small )
:$$: Text "arising from the constraint " :<>: ShowType ( Project big small )
)
)
( () :: Constraint )
)
data Leaves =
Leaves
{ Leaves -> [(Symbol, Type)]
labelledLeaves :: [ ( Symbol, Type ) ]
, Leaves -> [Type]
unlabelledLeaves :: [ Type ]
}
type CollectLeaves :: ( Type -> Type ) -> Leaves
type family CollectLeaves f where
CollectLeaves ( S1 ( MetaSel ( Just lbl ) _ _ _ ) ( Rec0 ty ) ) =
'Leaves '[ '( lbl, ty ) ] '[]
CollectLeaves ( M1 _ _ ( Rec0 ( lbl := ty ) ) ) =
'Leaves '[ '( lbl, ty ) ] '[]
CollectLeaves ( M1 _ _ ( Rec0 ty ) ) =
'Leaves '[] '[ ty ]
CollectLeaves ( M1 _ _ a ) =
CollectLeaves a
CollectLeaves ( l :*: r ) =
MergeLeaves ( CollectLeaves l ) ( CollectLeaves r )
CollectLeaves ( l :+: r ) =
IntersectLeaves ( CollectLeaves l ) ( CollectLeaves r )
CollectLeaves U1 =
'Leaves '[] '[]
CollectLeaves V1 =
'Leaves '[] '[]
type ProperAdapt :: Type -> Type -> Type -> Leaves -> Leaves -> Leaves -> Constraint
type family ProperAdapt args opts all argLeaves optLeaves allLeaves where
ProperAdapt args opts all ( 'Leaves ls_args us_args ) ( 'Leaves ls_opts us_opts ) ( 'Leaves ls_all us_all ) =
ThrowMessagesWithHeader
( Text "No instance for "
:$$: Text " " :<>: ShowType ( Adapt args opts all )
:$$: Text ""
)
( CatMaybes
'[ MessageIfNonEmpty ShowTypeWithLabelSym us_args ( Text "Unexpected unlabelled arguments:" )
, MessageIfNonEmpty ShowTypeWithLabelSym us_opts ( Text "Unexpected unlabelled defaults:" )
, MessageIfNonEmpty ShowTypeWithLabelSym us_all ( Text "Unexpected unlabelled types in destination:" )
]
:++:
ValidAdaptMessages args opts all ( RelativePosition ls_opts ls_all ) ( RelativePosition ls_args ls_all )
)
data InjectOrProject
= InjectCase
| ProjectCase
type ProperInjection :: Type -> Type -> Leaves -> Leaves -> Constraint
type family ProperInjection small big smallLeaves bigLeaves where
ProperInjection small big ( 'Leaves ls_small us_small ) ( 'Leaves ls_big us_big ) =
ThrowMessagesWithHeader
( Text "No instance for "
:$$: Text " " :<>: ShowType ( Inject small big )
:$$: Text ""
)
( CatMaybes
'[ MessageIfNonEmpty ShowTypeWithLabelSym us_small ( Text "Unexpected unlabelled types in source:" )
, MessageIfNonEmpty ShowTypeWithLabelSym us_big ( Text "Unexpected unlabelled types in destination:" )
]
:++:
ValidRelativePositionMessages InjectCase ( RelativePosition ls_small ls_big )
)
type ProperProjection :: Type -> Type -> Leaves -> Leaves -> Constraint
type family ProperProjection big small bigLeaves smallLeaves where
ProperProjection big small ( 'Leaves ls_big us_big ) ( 'Leaves ls_small us_small ) =
ThrowMessagesWithHeader
( Text "No instance for "
:$$: Text " " :<>: ShowType ( Project big small )
:$$: Text ""
)
( CatMaybes
'[ MessageIfNonEmpty ShowTypeWithLabelSym us_big ( Text "Unexpected unlabelled types in source:" )
, MessageIfNonEmpty ShowTypeWithLabelSym us_small ( Text "Unexpected unlabelled types in destination:" )
]
:++:
ValidRelativePositionMessages ProjectCase ( RelativePosition ls_small ls_big )
)
type ValidAdaptMessages :: Type -> Type -> Type -> RelPos ty -> RelPos ty -> [ ErrorMessage ]
type family ValidAdaptMessages args opts all opt_all_relPos args_all_relPos where
ValidAdaptMessages args opts all ( 'RelPos optsNotInAll optsInAllDups allNotInOpt ) ( 'RelPos argsNotInAll argsInAllDups allNotInArgs ) =
CatMaybes
'[ MessageIfNonEmpty ShowTypeWithLabelSym argsNotInAll
( Text "The following provided types do not appear in the destination:" )
, MessageIfNonEmpty ShowTypeWithLabelSym optsNotInAll
( Text "The following optional types do not appear in the destination:" )
, MessageIfNonEmpty ShowWhichTypeWithLabelSym optsInAllDups
( Text "The following duplicate optional types cause a problem:" )
, MessageIfNonEmpty ShowWhichTypeWithLabelSym argsInAllDups
( Text "The following duplicate provided types cause a problem:" )
, MessageIfNonEmpty ShowTypeWithLabelSym ( allNotInOpt `Intersect` allNotInArgs )
( Text "The following types are non-optional but have not been provided:" )
]
type ValidRelativePositionMessages :: InjectOrProject -> RelPos ty -> [ ErrorMessage ]
type family ValidRelativePositionMessages injProj relPos where
ValidRelativePositionMessages InjectCase ( 'RelPos smallNotInBig smallInBigDups _ ) =
CatMaybes
'[ MessageIfNonEmpty ShowWhichTypeWithLabelSym smallInBigDups
( Text "The following duplicate types cause a problem:" )
, MessageIfNonEmpty ShowTypeWithLabelSym smallNotInBig
( Text "The following types can't be injected, as they are missing from the target:" )
]
ValidRelativePositionMessages ProjectCase ( 'RelPos smallNotInBig smallInBigDups _ ) =
CatMaybes
'[ MessageIfNonEmpty ShowWhichTypeWithLabelSym smallInBigDups
( Text "The following duplicate types cause a problem:" )
, MessageIfNonEmpty ShowTypeWithLabelSym smallNotInBig
( Text "The following types can't be projected out, as they are missing from the source:" )
]
data Which
= InSmall
| InBig
| InBoth
data RelPos k =
RelPos
{ RelPos k -> [k]
smallNotInBig :: [ k ]
, RelPos k -> [(k, Which)]
smallInBigDups :: [ ( k, Which ) ]
, RelPos k -> [k]
bigNotInSmall :: [ k ]
}
type RelativePosition :: [k] -> [k] -> RelPos k
type family RelativePosition small big where
RelativePosition '[] bs = 'RelPos '[] '[] bs
RelativePosition ( a ': as ) bs =
RelativePositionWithRemoves a ( Remove a as ) ( Remove a bs )
type RelativePositionWithRemoves :: k -> ( [k], Mult ) -> ( [k], Mult ) -> RelPos k
type family RelativePositionWithRemoves a rem_a_as rem_a_bs where
RelativePositionWithRemoves a '( rem_a_as, mult_a_as ) '( rem_a_bs, mult_a_bs ) =
RelativePositionHelper a mult_a_as mult_a_bs ( RelativePosition rem_a_as rem_a_bs )
type RelativePositionHelper :: k -> Mult -> Mult -> RelPos k -> RelPos k
type family RelativePositionHelper a a_in_as a_in_bs rest where
RelativePositionHelper a _ None ( 'RelPos smallNotInBig smallInBigDups bigNotInSmall ) =
'RelPos ( a ': smallNotInBig ) smallInBigDups bigNotInSmall
RelativePositionHelper a None One ( 'RelPos smallNotInBig smallInBigDups bigNotInSmall ) =
'RelPos smallNotInBig smallInBigDups bigNotInSmall
RelativePositionHelper a _ One ( 'RelPos smallNotInBig smallInBigDups bigNotInSmall ) =
'RelPos smallNotInBig ( '( a, InSmall ) ': smallInBigDups ) bigNotInSmall
RelativePositionHelper a None Many ( 'RelPos smallNotInBig smallInBigDups bigNotInSmall ) =
'RelPos smallNotInBig ( '( a, InBig ) ': smallInBigDups ) bigNotInSmall
RelativePositionHelper a _ Many ( 'RelPos smallNotInBig smallInBigDups bigNotInSmall ) =
'RelPos smallNotInBig ( '( a, InBoth ) ': smallInBigDups ) bigNotInSmall
type ShowTypeWithLabel :: ty -> ErrorMessage
type family ShowTypeWithLabel ty where
ShowTypeWithLabel @( Symbol, Type ) '( lbl, ty ) = Text "#" :<>: Text lbl :<>: Text " := " :<>: ShowType ty
ShowTypeWithLabel @k ty = ShowType ty
type ShowTypeWithLabelSym :: TyFun ty ErrorMessage
data ShowTypeWithLabelSym fun mess
type instance Eval ShowTypeWithLabelSym ty = ShowTypeWithLabel ty
type ShowWhichTypeWithLabel :: ( ty, Which ) -> ErrorMessage
type family ShowWhichTypeWithLabel tyWhich where
ShowWhichTypeWithLabel '( ty, _ ) = ShowTypeWithLabel ty
type ShowWhichTypeWithLabelSym :: TyFun ( ty, Which ) ErrorMessage
data ShowWhichTypeWithLabelSym fun mess
type instance Eval ShowWhichTypeWithLabelSym tyWhich = ShowWhichTypeWithLabel tyWhich
type ShowWhich :: Which -> ErrorMessage
type family ShowWhich which where
ShowWhich InSmall = Text "(general)"
ShowWhich InBig = Text "(special)"
ShowWhich InBoth = Text " "
type MergeLeaves :: Leaves -> Leaves ->Leaves
type family MergeLeaves as bs where
MergeLeaves ( 'Leaves l1 u1 ) ( 'Leaves l2 u2 ) = 'Leaves ( l1 :++: l2 ) ( u1 :++: u2 )
type IntersectLeaves :: Leaves -> Leaves ->Leaves
type family IntersectLeaves as bs where
IntersectLeaves ( 'Leaves l1 u1 ) ( 'Leaves l2 u2 ) = 'Leaves ( l1 `Intersect` l2 ) ( u1 `Intersect` u2 )
type Dummy :: Type
data Dummy
deriving stock (forall x. Dummy -> Rep Dummy x)
-> (forall x. Rep Dummy x -> Dummy) -> Generic Dummy
forall x. Rep Dummy x -> Dummy
forall x. Dummy -> Rep Dummy x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Dummy x -> Dummy
$cfrom :: forall x. Dummy -> Rep Dummy x
Generic
instance {-# OVERLAPPING #-} UncheckedAdapt a a Dummy where
uncheckedAdapt :: a -> a -> Dummy
uncheckedAdapt = a -> a -> Dummy
forall a. HasCallStack => a
undefined
instance {-# OVERLAPPING #-} UncheckedAdapt a Dummy Dummy where
uncheckedAdapt :: a -> Dummy -> Dummy
uncheckedAdapt = a -> Dummy -> Dummy
forall a. HasCallStack => a
undefined
instance {-# OVERLAPPING #-} UncheckedAdapt a Dummy a where
uncheckedAdapt :: a -> Dummy -> a
uncheckedAdapt = a -> Dummy -> a
forall a. HasCallStack => a
undefined
instance {-# OVERLAPPING #-} UncheckedAdapt Dummy a a where
uncheckedAdapt :: Dummy -> a -> a
uncheckedAdapt = Dummy -> a -> a
forall a. HasCallStack => a
undefined
instance {-# OVERLAPPING #-} UncheckedAdapt Dummy Dummy a where
uncheckedAdapt :: Dummy -> Dummy -> a
uncheckedAdapt = Dummy -> Dummy -> a
forall a. HasCallStack => a
undefined
instance {-# OVERLAPPING #-} UncheckedInject a Dummy where
uncheckedInject :: a -> Dummy -> Dummy
uncheckedInject = a -> Dummy -> Dummy
forall a. HasCallStack => a
undefined
instance {-# OVERLAPPING #-} UncheckedInject Dummy a where
uncheckedInject :: Dummy -> a -> a
uncheckedInject = Dummy -> a -> a
forall a. HasCallStack => a
undefined
instance {-# OVERLAPPING #-} UncheckedProject a Dummy where
uncheckedProject :: a -> Dummy
uncheckedProject = a -> Dummy
forall a. HasCallStack => a
undefined
instance {-# OVERLAPPING #-} UncheckedProject Dummy a where
uncheckedProject :: Dummy -> a
uncheckedProject = Dummy -> a
forall a. HasCallStack => a
undefined
instance {-# OVERLAPPING #-} Adapt a a Dummy where
adapt :: a -> a -> Dummy
adapt = a -> a -> Dummy
forall a. HasCallStack => a
undefined
instance {-# OVERLAPPING #-} Adapt a Dummy Dummy where
adapt :: a -> Dummy -> Dummy
adapt = a -> Dummy -> Dummy
forall a. HasCallStack => a
undefined
instance {-# OVERLAPPING #-} Adapt a Dummy a where
adapt :: a -> Dummy -> a
adapt = a -> Dummy -> a
forall a. HasCallStack => a
undefined
instance {-# OVERLAPPING #-} Adapt Dummy a a where
adapt :: Dummy -> a -> a
adapt = Dummy -> a -> a
forall a. HasCallStack => a
undefined
instance {-# OVERLAPPING #-} Adapt Dummy Dummy a where
adapt :: Dummy -> Dummy -> a
adapt = Dummy -> Dummy -> a
forall a. HasCallStack => a
undefined
instance {-# OVERLAPPING #-} Inject a Dummy where
inject :: a -> Dummy -> Dummy
inject = a -> Dummy -> Dummy
forall a. HasCallStack => a
undefined
instance {-# OVERLAPPING #-} Inject Dummy a where
inject :: Dummy -> a -> a
inject = Dummy -> a -> a
forall a. HasCallStack => a
undefined
instance {-# OVERLAPPING #-} Project a Dummy where
project :: a -> Dummy
project = a -> Dummy
forall a. HasCallStack => a
undefined
instance {-# OVERLAPPING #-} Project Dummy a where
project :: Dummy -> a
project = Dummy -> a
forall a. HasCallStack => a
undefined