module Morley.Michelson.Typed.Haskell.ValidateDescription
( FieldDescriptions
, FieldDescriptionsV
, FieldDescriptionsValid
) where
import Data.Singletons (Demote)
import Data.Type.Bool (type (||))
import GHC.Generics qualified as G
import GHC.TypeLits (ErrorMessage(..), Symbol, TypeError)
import Morley.Util.Type (FailUnless, FailUnlessElse)
type FieldDescriptions = [(Symbol, (Maybe Symbol, [(Symbol, Symbol)]))]
type FieldDescriptionsV = Demote FieldDescriptions
type family FieldDescriptionsValid (descr :: FieldDescriptions) (typ :: Type) :: Constraint where
FieldDescriptionsValid '[] _ = ()
FieldDescriptionsValid descr typ =
Assert
(TypeError
('Text "No Generic instance for " ':<>: 'ShowType typ ':<>: 'Text "." ':$$:
'Text "Generic is needed to validate TypeDocFieldDescriptions.")
)
(G.Rep typ)
(FieldDescriptionsValidImpl descr typ)
type family FieldDescriptionsValidImpl (descr :: FieldDescriptions) (typ :: Type) :: Constraint where
FieldDescriptionsValidImpl '[] _ = ()
FieldDescriptionsValidImpl ( '(conName, '(_, fields)) ': rest ) typ =
( HasAllFields conName fields typ
, FieldDescriptionsValidImpl rest typ
)
type family HasConstructor (conName :: Symbol) (g :: Type -> Type) :: Bool where
HasConstructor conName (G.D1 _ cs) = HasConstructor conName cs
HasConstructor conName (G.C1 ('G.MetaCons conName _ _) _) = 'True
HasConstructor conName (l G.:+: r) = HasConstructor conName l || HasConstructor conName r
HasConstructor _ _ = 'False
type family HasAllFields (conName :: Symbol) (fields :: [(Symbol, Symbol)]) (typ :: Type) :: Constraint where
HasAllFields conName fields typ =
FailUnlessElse
(HasConstructor conName (G.Rep typ))
('Text "No constructor " ':<>: 'ShowType conName ':<>:
'Text " in type " ':<>: 'ShowType typ ':<>: 'Text "."
)
(HasAllFieldsImpl conName fields typ)
type family HasAllFieldsImpl (conName :: Symbol) (fields :: [(Symbol, Symbol)]) (typ :: Type) :: Constraint where
HasAllFieldsImpl _ '[] _ = ()
HasAllFieldsImpl conName ( '(fieldName, _) ': rest ) typ =
( FailUnless
(HasField conName fieldName (G.Rep typ))
('Text "No field " ':<>: 'ShowType fieldName ':<>: 'Text " in constructor " ':<>:
'ShowType conName ':<>: 'Text " of type " ':<>: 'ShowType typ ':<>: 'Text "."
)
, HasAllFieldsImpl conName rest typ
)
type family HasField (conName :: Symbol) (fieldName :: Symbol) (g :: Type -> Type) :: Bool where
HasField conName fieldName (G.D1 _ cs) = HasField conName fieldName cs
HasField conName fieldName (G.C1 ('G.MetaCons conName _ _) c) = ConHasField fieldName c
HasField conName fieldName (l G.:+: r) = HasField conName fieldName l || HasField conName fieldName r
HasField _ _ _ = 'False
type family ConHasField (fieldName :: Symbol) (g :: Type -> Type) :: Bool where
ConHasField fieldName (G.S1 ('G.MetaSel ('Just fieldName) _ _ _) _) = 'True
ConHasField fieldName (l G.:*: r) = ConHasField fieldName l || ConHasField fieldName r
ConHasField _ _ = 'False
data T1 a
type Assert :: Constraint -> (Type -> Type) -> k -> k
type family Assert err break v where
Assert _ T1 _ = Any
Assert _ _ k = k