module HaScalaM.Types.Tilde where

import HaScalaM.Classes.Base
import HaScalaM.Classes.Enums
import HaScalaM.Classes.Stat
import HaScalaM.Classes.Ref
import HaScalaM.Classes.Term
import HaScalaM.Classes.Type
import HaScalaM.Classes
import HaScalaM.Types.Base
import HaScalaM.Types.Enums
import HaScalaM.Types.Pat
import HaScalaM.Types.Ref
import HaScalaM.Types.Stat
import HaScalaM.Types.Term
import HaScalaM.Types.Type


-- C ---------------------------------------------------------------------------

data SmCaseCT p t where
    SmCaseC :: ( p ~ SmPat
               , t ~ SmTerm
               , Pat p
               , Term t
               ) => { forall p t. SmCaseCT p t -> p
patCCT :: p
                    , forall p t. SmCaseCT p t -> Maybe t
condCCT :: Maybe t
                    , forall p t. SmCaseCT p t -> t
bodyCCT :: t } -> SmCaseCT p t

data SmType'CaseCT t' where
    SmType'CaseT'C :: ( t' ~ SmType'
                      , Type' t'
                      ) => { forall t'. SmType'CaseCT t' -> t'
patT'CCT :: t'
                           , forall t'. SmType'CaseCT t' -> t'
bodyT'CCT :: t' } -> SmType'CaseCT t'


data SmCtorPrimary m n p t' t pc where
    SmCtorPrimary :: ( m ~ SmMod
                     , n ~ SmName
                     , p ~ SmParamT m n t' t
                     , pc ~ SmParamClauseT m n p t' t
                     , ParamClauseT m n p t' t pc
                     ) => { forall m n p t' t pc. SmCtorPrimary m n p t' t pc -> [m]
modsCP :: [m]
                          , forall m n p t' t pc. SmCtorPrimary m n p t' t pc -> n
nameCP :: n
                          , forall m n p t' t pc. SmCtorPrimary m n p t' t pc -> [pc]
paramClausesCP :: [pc] } -> SmCtorPrimary m n p t' t pc

-- E ---------------------------------------------------------------------------

data SmEnumerator where
    ECaseGenerator :: ( p ~ SmPat
                      , b ~ SmTerm
                      , Pat p
                      , Term b
                      ) => SmCaseGeneratorE p b -> SmEnumerator
    EGenerator :: ( p ~ SmPat
                  , b ~ SmTerm
                  , Pat p
                  , Term b
                  ) => SmGeneratorE p b -> SmEnumerator
    EGuard :: ( b ~ SmTerm
              , Term b
              ) => SmGuardE b -> SmEnumerator
    EVal :: ( p ~ SmPat
            , b ~ SmTerm
            , Pat p
            , Term b
            ) => SmValE p b -> SmEnumerator

-- I ---------------------------------------------------------------------------

data SmImportee where
    SmGivenI :: ( t' ~ SmType'
                , Type' t'
                ) => { ()
tpeGI :: t' } -> SmImportee
    SmGivenAllI :: SmImportee
    SmNameI :: ( n ~ SmName
               , Name n
               )  => { ()
nameNI :: n } -> SmImportee
    SmRenameI :: ( n ~ SmName
                 , Name n
                 ) => { ()
nameRI :: n
                      , ()
renameRI :: n } -> SmImportee
    SmUnimportI ::( n ~ SmName
                  , Name n
                  ) => { ()
nameUI :: n } -> SmImportee
    SmWildcardI :: SmImportee


data SmImporter r i where
    SmImporter :: ( r ~ SmRef
                  , i ~ SmImportee
                  , RefT r
                  , Importee i
                  ) => { forall r i. SmImporter r i -> r
refII :: r
                       , forall r i. SmImporter r i -> [i]
importeesII :: [i] } -> SmImporter r i


data SmInit m n t' t ac where
    SmInit :: ( m ~ SmMod
              , n ~ SmName
              , t' ~ SmType'
              , t ~ SmTerm
              , ac ~ SmArgClauseT m t
              , Name n
              , Type' t'
              , ArgClauseT m t ac
              ) => { forall m n t' t ac. SmInit m n t' t ac -> t'
tpeI :: t'
                   , forall m n t' t ac. SmInit m n t' t ac -> n
nameI :: n
                   , forall m n t' t ac. SmInit m n t' t ac -> [ac]
argClausesI :: [ac] } -> SmInit m n t' t ac

-- M ---------------------------------------------------------------------------

data SmMod where
    MAnnot :: ( m ~ SmMod
              , n ~ SmName
              , t' ~ SmType'
              , t ~ SmTerm
              , ac ~ SmArgClauseT m t
              , i ~ SmInit m n t' t ac
              , Init m n t' t ac i
              ) => SmAnnotM m n t' t ac i -> SmMod
    MMod :: SmModM -> SmMod
    MAccess :: ( r ~ SmRef_
               , Ref r
               ) => SmAccessM r -> SmMod

-- N ---------------------------------------------------------------------------

data SmName where
    NAnonymous :: SmAnonymousRT -> SmName
    NName :: SmNameN -> SmName
    NTName :: SmNameT -> SmName
    NT'Name :: SmNameT' -> SmName


data SmNameT where
    SmNameT :: { SmNameT -> String
valueNT :: String } -> SmNameT


data SmNameT' where
    SmNameT' :: { SmNameT' -> String
valueNT' :: String } -> SmNameT'

-- P ---------------------------------------------------------------------------

data SmParamClauseGroup m n p p' t' b' t pc pc' where
    SmParamClauseGroup :: ( m ~ SmMod
                          , n ~ SmName
                          , p ~ SmParamT m n t' t
                          , p' ~ SmParamT' m n t' b'
                          , t' ~ SmType'
                          , b' ~ SmBounds' t'
                          , t ~ SmTerm
                          , pc ~ SmParamClauseT m n p t' t
                          , pc' ~ SmParamClauseT' m n p' t' b'
                          , ParamClauseT' m n p' t' b' pc'
                          , ParamClauseT m n p t' t pc
                          ) => { forall m n p t' t p' b' pc pc'.
SmParamClauseGroup m n p p' t' b' t pc pc' -> pc'
t'paramClausePCG :: pc'
                               , forall m n p t' t p' b' pc pc'.
SmParamClauseGroup m n p p' t' b' t pc pc' -> [pc]
paramClausesPCG :: [pc] } -> SmParamClauseGroup m n p p' t' b' t pc pc'

data SmPatP where
    SmAlternativeP :: ( p ~ SmPat
                      , Pat p
                      ) => { ()
lhsAP :: p
                           , ()
rhsAP :: p } -> SmPatP
    SmBindP :: ( p ~ SmPat
               , Pat p
               ) => { ()
lhsBP :: p
                    , ()
rhsBP :: p } -> SmPatP
    SmGivenP :: ( t' ~ SmType'
                , Type' t'
                ) => { ()
tpeGP :: t' } -> SmPatP
    SmInterpolateP :: ( tn ~ SmNameT
                      , l ~ SmLit
                      , p ~ SmPat
                      , NameT tn
                      , Lit l
                      , Pat p
                      ) => { ()
prefixIP :: tn
                           , ()
partsIP :: [l]
                           , ()
argsIP :: [p] } -> SmPatP
    SmNameP :: ( tn ~ SmNameT
               , NameT tn
               ) => { ()
nameP :: tn } -> SmPatP
    SmRepeatedP :: ( tn ~ SmNameT
                   , NameT tn
                   ) => { ()
nameRP :: tn } -> SmPatP
    SmSelectP :: ( tn ~ SmNameT
                 , t ~ SmTerm
                 , NameT tn
                 , Term t
                 ) => { ()
seleP :: SmSelectRT tn t } -> SmPatP
    SmSeqWildcardP :: SmPatP
    SmTypedP :: ( p ~ SmPat
                , t' ~ SmType'
                , Type' t'
                , Pat p
                , Type' t'
                ) => { ()
lhsTP :: p
                     , ()
rhsTP :: t' } -> SmPatP
    SmWildcardP :: SmPatP
    SmXmlP :: ( l ~ SmLit
              , p ~ SmPat
              , Lit l
              , Pat p
              ) => { ()
partsXP :: [l]
                   , ()
argsXP :: [p] } -> SmPatP

data SmPat where
    PExtract :: ( t ~ SmTerm
                , p ~ SmPat
                , ac ~ SmArgClauseP p
                , Term t
                , Pat p
                , ArgClauseP p ac
                ) => SmExtractP t p ac -> SmPat
    PExtractInfix :: ( tn ~ SmNameT
                     , p ~ SmPat
                     , ac ~ SmArgClauseP p
                     , NameT tn
                     , Pat p
                     , ArgClauseP p ac
                     ) => SmExtractInfixP tn p ac -> SmPat
    PLit :: SmLit -> SmPat
    PMacro :: ( t ~ SmTerm
              , Term t
              ) => SmMacroP t -> SmPat
    PPat :: SmPatP -> SmPat
    PTuple :: ( p ~ SmPat
              , Pat p
              ) => SmTupleP p -> SmPat
    PVar :: ( tn ~ SmNameT
            , NameT tn
            ) => SmVarP tn -> SmPat

data SmArgClauseP p where
    SmArgClauseP :: ( p ~ SmPat
                    , Pat p
                    ) => { forall p. SmArgClauseP p -> [p]
valuesACP :: [p] } -> SmArgClauseP p

-- R ---------------------------------------------------------------------------

data SmRef_ where
    RImportee :: SmImportee -> SmRef_
    RInit :: ( m ~ SmMod
             , n ~ SmName
             , t' ~ SmType'
             , t ~ SmTerm
             , ac ~ SmArgClauseT m t
             , Name n
             , Type' t'
             , ArgClauseT m t ac
             ) => SmInit m n t' t ac -> SmRef_
    RName :: SmName -> SmRef_
    R_TRef :: SmRef -> SmRef_
    R_T'Ref:: SmRef' -> SmRef_


data SmRef where
    RTAnonymous :: SmAnonymousRT -> SmRef
    RTName :: SmNameT -> SmRef
    RTRef :: ( n ~ SmNameT
             , t ~ SmTerm
             ) => SmRefT n t -> SmRef
    RTSelect :: ( tn ~ SmNameT
                , t ~ SmTerm
                , Name tn
                , Term t
                ) => SmSelectRT tn t -> SmRef


data SmRef' where
    RT'Name :: SmNameT' -> SmRef'
    RT'Ref :: ( t'n ~ SmNameT'
              , t' ~ SmType'
              , r ~ SmRef
              ) => SmRefT' t'n t' r -> SmRef'

-- S ---------------------------------------------------------------------------

data SmSelf n t' where
    SmSelf :: ( n ~ SmName
              , t' ~ SmType'
              , Name n
              , Type' t'
              ) => { forall n t'. SmSelf n t' -> n
nameS :: n
                   , forall n t'. SmSelf n t' -> Maybe t'
decltpeOptS :: Maybe t' } -> SmSelf n t'


data SmStat where
    S'' :: String -> SmStat
    SCtorSecondary :: ( m ~ SmMod
                      , n ~ SmName
                      , p ~ SmParamT m n t' t
                      , t' ~ SmType'
                      , t ~ SmTerm
                      , pc ~ SmParamClauseT m n p t' t
                      , ac ~ SmArgClauseT m t
                      , i ~ SmInit m n t' t ac
                      , s ~ SmStat
                      , ParamClauseT m n p t' t pc
                      , Init m n t' t ac i
                      , Stat s
                      ) => SmCtorSecondaryS m n p t' t pc ac i s -> SmStat
    SDef' :: ( m ~ SmMod
             , n ~ SmName
             , tn ~ SmNameT
             , p ~ SmParamT m n t' t
             , p' ~ SmParamT' m n t' b'
             , t' ~ SmType'
             , b' ~ SmBounds' t'
             , t ~ SmTerm
             , pc ~ SmParamClauseT m n p t' t
             , pc' ~ SmParamClauseT' m n p' t' b'
             , g ~ SmParamClauseGroup m n p p' t' b' t pc pc'
             , NameT tn
             , ParamClauseGroup m n p p' t' b' t pc pc' g
             ) => SmDef'S m n tn p p' t' b' t pc pc' g -> SmStat
    SGiven' :: ( m ~ SmMod
               , n ~ SmName
               , tn ~ SmNameT
               , p ~ SmParamT m n t' t
               , p' ~ SmParamT' m n t' b'
               , t' ~ SmType'
               , b' ~ SmBounds' t'
               , t ~ SmTerm
               , pc ~ SmParamClauseT m n p t' t
               , pc' ~ SmParamClauseT' m n p' t' b'
               , g ~ SmParamClauseGroup m n p p' t' b' t pc pc'
               , NameT tn
               , ParamClauseGroup m n p p' t' b' t pc pc' g
               ) => SmGiven'S m n tn p p' t' b' t pc pc' g -> SmStat
    SType' :: ( m ~ SmMod
              , n ~ SmName
              , t'n ~ SmNameT'
              , p' ~ SmParamT' m n t' b'
              , t' ~ SmType'
              , b' ~ SmBounds' t'
              , pc' ~ SmParamClauseT' m n p' t' b'
              , NameT' t'n
              , ParamClauseT' m n p' t' b' pc'
              ) => SmType'S m n t'n p' t' b' pc' -> SmStat
    SVal' :: ( m ~ SmMod
             , p ~ SmPat
             , t' ~ SmType'
             , Mod m
             , Pat p
             , Type' t'
             ) => SmVal'S m p t' -> SmStat
    SVar' :: ( m ~ SmMod
             , p ~ SmPat
             , t' ~ SmType'
             , Mod m
             , Pat p
             , Type' t'
             ) => SmVar'S m p t' -> SmStat
    SClass :: ( m ~ SmMod
              , n ~ SmName
              , t'n ~ SmNameT'
              , p ~ SmParamT m n t' t
              , p' ~ SmParamT' m n t' b'
              , t' ~ SmType'
              , b' ~ SmBounds' t'
              , t ~ SmTerm
              , pc ~ SmParamClauseT m n p t' t
              , pc' ~ SmParamClauseT' m n p' t' b'
              , c ~ SmCtorPrimary m n p t' t pc
              , ac ~ SmArgClauseT m t
              , i ~ SmInit m n t' t ac
              , f ~ SmSelf n t'
              , s ~ SmStat
              , e ~ SmTemplate m n t' t ac i f s
              , NameT' t'n
              , ParamClauseT' m n p' t' b' pc'
              , Primary m n p t' t pc c
              , Template m n t' t ac i f s e
              ) => SmClassS m n t'n p p' t' b' t pc pc' c ac i f s e -> SmStat
    SDef :: ( m ~ SmMod
            , n ~ SmName
            , tn ~ SmNameT
            , p ~ SmParamT m n t' t
            , p' ~ SmParamT' m n t' b'
            , t' ~ SmType'
            , b' ~ SmBounds' t'
            , t ~ SmTerm
            , pc ~ SmParamClauseT m n p t' t
            , pc' ~ SmParamClauseT' m n p' t' b'
            , g ~ SmParamClauseGroup m n p p' t' b' t pc pc'
            , NameT tn
            , ParamClauseGroup m n p p' t' b' t pc pc' g
            ) => SmDefS m n tn p p' t' b' t pc pc' g -> SmStat
    SEnum :: ( m ~ SmMod
             , n ~ SmName
             , t'n ~ SmNameT'
             , p ~ SmParamT m n t' t
             , p' ~ SmParamT' m n t' b'
             , t' ~ SmType'
             , b' ~ SmBounds' t'
             , t ~ SmTerm
             , pc ~ SmParamClauseT m n p t' t
             , pc' ~ SmParamClauseT' m n p' t' b'
             , c ~ SmCtorPrimary m n p t' t pc
             , ac ~ SmArgClauseT m t
             , i ~ SmInit m n t' t ac
             , f ~ SmSelf n t'
             , s ~ SmStat
             , e ~ SmTemplate m n t' t ac i f s
             , NameT' t'n
             , ParamClauseT' m n p' t' b' pc'
             , Primary m n p t' t pc c
             , Template m n t' t ac i f s e
             ) => SmEnumS m n t'n p p' t' b' t pc pc' c ac i f s e -> SmStat
    SEnumCase :: ( m ~ SmMod
                 , n ~ SmName
                 , tn ~ SmNameT
                 , p ~ SmParamT m n t' t
                 , p' ~ SmParamT' m n t' b'
                 , t' ~ SmType'
                 , b' ~ SmBounds' t'
                 , t ~ SmTerm
                 , pc ~ SmParamClauseT m n p t' t
                 , pc' ~ SmParamClauseT' m n p' t' b'
                 , c ~ SmCtorPrimary m n p t' t pc
                 , ac ~ SmArgClauseT m t
                 , i ~ SmInit m n t' t ac
                 , NameT tn
                 , ParamClauseT' m n p' t' b' pc'
                 , Primary m n p t' t pc c
                 , Init m n t' t ac i
                 ) => SmEnumCaseS m n tn p p' t' b' t pc pc' c ac i -> SmStat
    SExtensionGroup :: ( m ~ SmMod
                       , n ~ SmName
                       , p ~ SmParamT m n t' t
                       , p' ~ SmParamT' m n t' b'
                       , t' ~ SmType'
                       , b' ~ SmBounds' t'
                       , t ~ SmTerm
                       , pc ~ SmParamClauseT m n p t' t
                       , pc' ~ SmParamClauseT' m n p' t' b'
                       , s ~ SmStat
                       , g ~ SmParamClauseGroup m n p p' t' b' t pc pc'
                       , ParamClauseGroup m n p p' t' b' t pc pc' g
                       , Stat s
                       ) => SmExtensionGroupS m n p p' t' b' t pc pc' s g -> SmStat
    SGiven :: ( m ~ SmMod
              , n ~ SmName
              , tn ~ SmNameT
              , p ~ SmParamT m n t' t
              , p' ~ SmParamT' m n t' b'
              , t' ~ SmType'
              , b' ~ SmBounds' t'
              , t ~ SmTerm
              , pc ~ SmParamClauseT m n p t' t
              , pc' ~ SmParamClauseT' m n p' t' b'
              , g ~ SmParamClauseGroup m n p p' t' b' t pc pc'
              , ac ~ SmArgClauseT m t
              , i ~ SmInit m n t' t ac
              , f ~ SmSelf n t'
              , s ~ SmStat
              , e ~ SmTemplate m n t' t ac i f s
              , ParamClauseGroup m n p p' t' b' t pc pc' g
              , Template m n t' t ac i f s e
              ) => SmGivenS m n p p' t' b' t pc pc' ac i f s e g -> SmStat
    SImpExp :: ( r ~ SmRef
               , i ~ SmImportee
               , t ~ SmImporter r i
               , Importer r i t
               ) => SmImportExportStatS r i t -> SmStat
    SGivenAlias :: ( m ~ SmMod
                   , n ~ SmName
                   , p ~ SmParamT m n t' t
                   , p' ~ SmParamT' m n t' b'
                   , t' ~ SmType'
                   , b' ~ SmBounds' t'
                   , t ~ SmTerm
                   , pc ~ SmParamClauseT m n p t' t
                   , pc' ~ SmParamClauseT' m n p' t' b'
                   , g ~ SmParamClauseGroup m n p p' t' b' t pc pc'
                   , ParamClauseGroup m n p p' t' b' t pc pc' g
                   ) => SmGivenAliasS m n p p' t' b' t pc pc' g -> SmStat
    SMacro :: ( m ~ SmMod
              , n ~ SmName
              , tn ~ SmNameT
              , p ~ SmParamT m n t' t
              , p' ~ SmParamT' m n t' b'
              , t' ~ SmType'
              , b' ~ SmBounds' t'
              , t ~ SmTerm
              , pc ~ SmParamClauseT m n p t' t
              , pc' ~ SmParamClauseT' m n p' t' b'
              , g ~ SmParamClauseGroup m n p p' t' b' t pc pc'
              , NameT tn
              , ParamClauseGroup m n p p' t' b' t pc pc' g
              ) => SmMacroS m n tn p p' t' b' t pc pc' g -> SmStat
    SObject :: ( m ~ SmMod
               , n ~ SmName
               , tn ~ SmNameT
               , p ~ SmParamT m n t' t
               , t' ~ SmType'
               , t ~ SmTerm
               , ac ~ SmArgClauseT m t
               , i ~ SmInit m n t' t ac
               , f ~ SmSelf n t'
               , s ~ SmStat
               , e ~ SmTemplate m n t' t ac i f s
               , NameT tn
               , Template m n t' t ac i f s e
               ) => SmObjectS m n tn t' t ac i f s e -> SmStat
    SPkg :: ( r ~ SmRef
            , s ~ SmStat
            , RefT r
            , Stat s
            ) => SmPkgS r s-> SmStat
    SPkgObject :: ( m ~ SmMod
                  , n ~ SmName
                  , tn ~ SmNameT
                  , p ~ SmParamT m n t' t
                  , t' ~ SmType'
                  , t ~ SmTerm
                  , ac ~ SmArgClauseT m t
                  , i ~ SmInit m n t' t ac
                  , f ~ SmSelf n t'
                  , s ~ SmStat
                  , e ~ SmTemplate m n t' t ac i f s
                  , NameT tn
                  , Template m n t' t ac i f s e
                  ) => SmPkgObjectS m n tn t' t ac i f s e -> SmStat
    SRepeatedEnumCase :: ( m ~ SmMod
                         , tn ~ SmNameT
                         , Mod m
                         , NameT tn
                         ) => SmRepeatedEnumCase m tn -> SmStat
    STerm :: SmTerm -> SmStat
    STrait :: ( m ~ SmMod
              , n ~ SmName
              , t'n ~ SmNameT'
              , p ~ SmParamT m n t' t
              , p' ~ SmParamT' m n t' b'
              , t' ~ SmType'
              , b' ~ SmBounds' t'
              , t ~ SmTerm
              , pc ~ SmParamClauseT m n p t' t
              , pc' ~ SmParamClauseT' m n p' t' b'
              , c ~ SmCtorPrimary m n p t' t pc
              , ac ~ SmArgClauseT m t
              , i ~ SmInit m n t' t ac
              , f ~ SmSelf n t'
              , s ~ SmStat
              , e ~ SmTemplate m n t' t ac i f s
              , NameT' t'n
              , ParamClauseT' m n p' t' b' pc'
              , Primary m n p t' t pc c
              , Template m n t' t ac i f s e
              ) => SmTraitS m n t'n p p' t' b' t pc pc' c ac i f s e -> SmStat
    SType :: ( m ~ SmMod
             , n ~ SmName
             , t'n ~ SmNameT'
             , p' ~ SmParamT' m n t' b'
             , t' ~ SmType'
             , b' ~ SmBounds' t'
             , pc' ~ SmParamClauseT' m n p' t' b'
             , NameT' t'n
             , ParamClauseT' m n p' t' b' pc'
             ) => SmTypeS m n t'n p' t' b' pc' -> SmStat
    SVal :: ( m ~ SmMod
            , p ~ SmPat
            , t' ~ SmType'
            , t ~ SmTerm
            , Mod m
            , Pat p
            , Type' t'
            , Term t
            ) => SmValS m p t' t -> SmStat
    SVar :: ( m ~ SmMod
            , p ~ SmPat
            , t' ~ SmType'
            , t ~ SmTerm
            , Mod m
            , Pat p
            , Type' t'
            , Term t
            ) => SmVarS m p t' t -> SmStat

data SmSource s where
  SmSource :: ( s ~ SmStat
              , Stat s
              ) => { forall s. SmSource s -> [s]
statsS :: [s] } -> SmSource s

-- T ---------------------------------------------------------------------------

data SmTemplate m n t' t ac i p s where
    SmTemplate :: ( m ~ SmMod
                  , n ~ SmName
                  , t' ~ SmType'
                  , t ~ SmTerm
                  , ac ~ SmArgClauseT m t
                  , i ~ SmInit m n t' t ac
                  , s ~ SmStat
                  , p ~ SmSelf n t'
                  , Init m n t' t ac i
                  , Stat s
                  , Self n t' p
                  ) => { forall m n t' t ac i s p. SmTemplate m n t' t ac i p s -> [s]
earlyT :: [s]
                       , forall m n t' t ac i s p. SmTemplate m n t' t ac i p s -> [i]
initsT :: [i]
                       , forall m n t' t ac i s p. SmTemplate m n t' t ac i p s -> p
selfT :: p
                       , forall m n t' t ac i s p. SmTemplate m n t' t ac i p s -> [s]
statsT :: [s]
                       , forall m n t' t ac i s p. SmTemplate m n t' t ac i p s -> [t']
derivesT :: [t'] } -> SmTemplate m n t' t ac i p s

-- Te --------------------------------------------------------------------------

data SmTermT where
    SmAnnotateT :: ( m ~ SmMod
                   , n ~ SmName
                   , t' ~ SmType'
                   , t ~ SmTerm
                   , ac ~ SmArgClauseT m t
                   , i ~ SmInit m n t' t ac
                   , n ~ SmName
                   , a ~ SmAnnotM m n t' t ac i
                   , Annot m n t' t ac i a
                   ) => { ()
exprAnnT :: t
                        , ()
annotsAnnT :: [a] } -> SmTermT
    SmAnonymousFunctionT :: ( t ~ SmTerm
                            , Term t
                            ) => { ()
bodyAFT :: t } -> SmTermT
    SmAscribeT :: ( t ~ SmTerm
                  , t' ~ SmType'
                  , Term t
                  , Type' t'
                  ) => { ()
exprAscrT :: t
                       , ()
tpeAscrT :: t' } -> SmTermT
    SmBlockT :: ( s ~ SmStat
                , Stat s
                ) => { ()
statsBlT :: [s] } -> SmTermT
    SmEndMarkerT :: ( tn ~ SmNameT
                    , NameT tn
                    ) => { ()
nameEMT :: tn } -> SmTermT
    SmEtaT :: ( t ~ SmTerm
              , Term t
              ) => { ()
exprEtaT :: t } -> SmTermT
    SmIfT :: ( m ~ SmMod
             , t ~ SmTerm
             , Mod m
             , Term t
             ) => { ()
condIfT :: t
                  , ()
thenpIfT :: t
                  , ()
elsepIfT :: t
                  , ()
mods :: [m] } -> SmTermT
    SmInterpolateT :: ( tn ~ SmNameT
                      , l ~ SmLit
                      , t ~ SmTerm
                      , NameT tn
                      , Lit l
                      , Term t
                      ) => { ()
prefixIT :: tn
                           , ()
partsIT :: [l]
                           , ()
argsIT :: [t] } -> SmTermT
    SmNewT :: ( m ~ SmMod
              , n ~ SmName
              , t' ~ SmType'
              , t ~ SmTerm
              , ac ~ SmArgClauseT m t
              , i ~ SmInit m n t' t ac
              , Init m n t' t ac i
              ) => { ()
initN :: i } -> SmTermT
    SmPlaceholder :: SmTermT
    SmQuotedMacroExprT :: ( t ~ SmTerm
                          , Term t
                          ) => { ()
bodyQMET :: t } -> SmTermT
    SmQuotedMacroType'T :: ( t' ~ SmType'
                           , Type' t'
                           ) => { ()
tpeQMT'T :: t' } -> SmTermT
    SmRepeatedT :: ( t ~ SmTerm
                   , Term t
                   ) => { ()
exprRepT :: t } -> SmTermT
    SmReturnT :: ( t ~ SmTerm
                 , Term t
                 ) => { ()
exprRetT :: t } -> SmTermT
    SmSplicedMacroExprT :: ( t ~ SmTerm
                           , Term t
                           ) => { ()
bodySMET :: t } -> SmTermT
    SmSplicedMacroPatT :: ( p ~ SmPat
                          , Pat p
                          ) => { ()
patSMPT :: p } -> SmTermT
    SmThrowT :: ( t ~ SmTerm
                , Term t
                ) => { ()
exprThrT :: t } -> SmTermT
    SmTryWithHandlerT :: ( t ~ SmTerm
                         , Term t
                         ) => { ()
exprTWHT :: t
                              , ()
catchpTWHT :: t
                              , ()
finallypTWHT :: t } -> SmTermT
    SmXmlT :: ( l ~ SmLit
              , t ~ SmTerm
              , Lit l
              , Term t
              ) => { ()
partsXT :: [l]
                   , ()
argsXT :: [t] } -> SmTermT

data SmTerm where
    T'' :: String -> SmTerm
    TApply :: ( m ~ SmMod
              , t ~ SmTerm
              , ac ~ SmArgClauseT m t
              , ArgClauseT m t ac
              ) => SmApplyT m t ac -> SmTerm
    TApplyInfix :: ( m ~ SmMod
                   , tn ~ SmNameT
                   , t' ~ SmType'
                   , t ~ SmTerm
                   , ac' ~ SmArgClauseT' t'
                   , ac ~ SmArgClauseT m t
                   , NameT tn
                   , ArgClauseT' t' ac'
                   , ArgClauseT m t ac
                   ) => SmApplyInfixT m tn t t' ac' ac -> SmTerm
    TApplyType' :: ( t ~ SmTerm
                   , t' ~ SmType'
                   , ac' ~ SmArgClauseT' t'
                   , Term t
                   , ArgClauseT' t' ac'
                   ) => SmApplyType'T t t' ac' -> SmTerm
    TAssign :: ( t ~ SmTerm
               , Term t
               ) => SmAssignT t -> SmTerm
    TContextFunction :: ( m ~ SmMod
                        , n ~ SmName
                        , p ~ SmParamT m n t' t
                        , t' ~ SmType'
                        , t ~ SmTerm
                        , pc ~ SmParamClauseT m n p t' t
                        , ParamClauseT m n p t' t pc
                        ) => SmContextFunctionT m n p t' t pc -> SmTerm
    TDo :: ( t ~ SmTerm
           , Term t
           ) => SmDoT t -> SmTerm
    TFor :: ( e ~ SmEnumerator
            , t ~ SmTerm
            , Enumerator e
            , Term t
            ) => SmForT e t -> SmTerm
    TForYield :: ( e ~ SmEnumerator
                 , t ~ SmTerm
                 , Enumerator e
                 , Term t
                 ) => SmForYieldT e t -> SmTerm
    TFunction :: ( m ~ SmMod
                 , n ~ SmName
                 , p ~ SmParamT m n t' t
                 , t' ~ SmType'
                 , t ~ SmTerm
                 , pc ~ SmParamClauseT m n p t' t
                 , ParamClauseT m n p t' t pc
                 ) => SmFunctionT m n p t' t pc -> SmTerm
    TLit :: SmLit -> SmTerm
    TMatch :: ( p ~ SmPat
              , t ~ SmTerm
              , ct ~ SmCaseCT p t
              , Case p t ct
              ) => SmMatchT p t ct -> SmTerm
    TNewAnonymous :: ( m ~ SmMod
                     , n ~ SmName
                     , t' ~ SmType'
                     , t ~ SmTerm
                     , ac ~ SmArgClauseT m t
                     , i ~ SmInit m n t' t ac
                     , p ~ SmSelf n t'
                     , s ~ SmStat
                     , e ~ SmTemplate m n t' t ac i p s
                     , Template m n t' t ac i p s e
                     ) => SmNewAnonymousT m n t' t ac i p s e -> SmTerm
    TPartialFunction :: ( p ~ SmPat
                        , t ~ SmTerm
                        , ct ~ SmCaseCT p t
                        , Case p t ct
                        ) => SmPartialFunctionT p t ct -> SmTerm
    TPolyFunction :: ( m ~ SmMod
                     , n ~ SmName
                     , p' ~ SmParamT' m n t' b'
                     , t' ~ SmType'
                     , b' ~ SmBounds' t'
                     , pc' ~ SmParamClauseT' m n p' t' b'
                     , t ~ SmTerm
                     , ParamClauseT' m n p' t' b' pc'
                     , Term t
                     ) => SmPolyFunctionT m n p' t' b' pc' t -> SmTerm
    TRef :: SmRef -> SmTerm
    TTerm :: SmTermT -> SmTerm
    TTry :: ( p ~ SmPat
            , t ~ SmTerm
            , ct ~ SmCaseCT p t
            , Case p t ct
            ) => SmTryT p t ct -> SmTerm
    TTuple :: ( t ~ SmTerm
              , Term t
              ) => SmTupleT t -> SmTerm
    TWhile :: ( t ~ SmTerm
              , Term t
              ) => SmWhileT t -> SmTerm

data SmArgClauseT m t where
    SmArgClauseT :: ( m ~ SmMod
                    , t ~ SmTerm
                    , ArgsType m
                    , Term t
                    ) => { forall m t. SmArgClauseT m t -> [t]
valuesACT :: [t]
                         , forall m t. SmArgClauseT m t -> Maybe m
modACT :: Maybe m } -> SmArgClauseT m t

data SmParamT m n t' t where
    SmParamT :: ( m ~ SmMod
                , n ~ SmName
                , t' ~ SmType'
                , t ~ SmTerm
                , Mod m
                , Name n
                , Type' t'
                , Term t
                ) => { forall m n t' t. SmParamT m n t' t -> [m]
modsPT :: [m]
                     , forall m n t' t. SmParamT m n t' t -> n
namePT :: n
                     , forall m n t' t. SmParamT m n t' t -> Maybe t'
decltpeOptPT :: Maybe t'
                     , forall m n t' t. SmParamT m n t' t -> Maybe t
defaultOptPT :: Maybe t } -> SmParamT m n t' t

data SmParamClauseT m n p t' t where
    SmParamClauseT :: ( p ~ SmParamT m n t' t
                      , ParamsType m
                      , ParamT m n p t' t
                      ) => { forall p m n t' t. SmParamClauseT m n p t' t -> [p]
valuesPCT :: [p]
                           , forall p m n t' t. SmParamClauseT m n p t' t -> Maybe m
modPCT :: Maybe m } -> SmParamClauseT m n p t' t

-- Ty --------------------------------------------------------------------------

data SmType'T' where
    SmAndT' :: ( t' ~ SmType'
               , Type' t'
               ) => { ()
lhsAndT' :: t'
                    , ()
rhsAndT' :: t' } -> SmType'T'
    SmAnnotateT' :: ( m ~ SmMod
                    , n ~ SmName
                    , t' ~ SmType'
                    , ac ~ SmArgClauseT m t
                    , a ~ SmAnnotM m n t' t ac i
                    , i ~ SmInit m n t' t ac
                    , Annot m n t' t ac i a
                    ) => { ()
tpeAnnT' :: t'
                         , ()
annotsAnnT' :: [a] } -> SmType'T'
    SmAnonymousLambdaT' :: ( t' ~ SmType'
                           , Type' t'
                           ) => { ()
tpeALT' :: t' } -> SmType'T'
    SmAnonymousNameT' :: SmType'T'
    SmAnonymousParamT' :: ( m ~ SmMod
                          , Variant m
                          ) => { ()
variantAPT' :: Maybe m } -> SmType'T'
    SmBlockT' :: ( m ~ SmMod
                 , n ~ SmName
                 , t'n ~ SmNameT'
                 , p' ~ SmParamT' m n t' b'
                 , t' ~ SmType'
                 , b' ~ SmBounds' t'
                 , pc' ~ SmParamClauseT' m n p' t' b'
                 , t'd ~ SmType'Def m n t'n p' t' b' pc'
                 , Type'Def m n t'n p' t' b' pc' t'd
                 ) => { ()
type'DefsBT' :: [t'd],
                        ()
tpeBT' :: t' } -> SmType'T'
    SmByNameT' :: ( t' ~ SmType'
                  , Type' t'
                  ) => { ()
tpeBNT' :: t' } -> SmType'T'
    SmExistentialT' :: ( t' ~ SmType'
                       , s ~ SmStat
                       , Type' t'
                       , Stat s
                       ) => { ()
tpeET' :: t'
                            , ()
statsET' :: [s] } -> SmType'T'
    SmImplicitFunctionT' :: ( t' ~ SmType'
                            , Type' t'
                            ) => { ()
paramsIFT' :: [t']
                                 , ()
resIFT' :: t' } -> SmType'T'
    SmMethodT' :: ( m ~ SmMod
                  , n ~ SmName
                  , p ~ SmParamT m n t' t
                  , t ~ SmTerm
                  , t' ~ SmType'
                  , pc ~ SmParamClauseT m n p t' t
                  , ParamClauseT m n p t' t pc
                  ) => { ()
paramClausesMT' :: [pc]
                       , ()
tpeMthT' :: t' } -> SmType'T'
    SmOrT' :: ( t' ~ SmType'
              , Type' t'
              ) => { ()
lhsOrT' :: t'
                   , ()
rhsOrT' :: t' } -> SmType'T'
    SmRefineT' :: ( t' ~ SmType'
                  , s ~ SmStat
                  , Type' t'
                  , Stat s
                  ) => { ()
tpeRfT' :: Maybe t'
                       , ()
statsRfT' :: [s] } -> SmType'T'
    SmRepeatedT' :: ( t' ~ SmType'
                    , Type' t'
                    ) => { ()
tpeRpT' :: t' } -> SmType'T'
    SmPatWildcardT' :: SmType'T'
    SmWithT' :: ( t' ~ SmType'
                , Type' t'
                ) => { ()
lhsWT' :: t'
                     , ()
rhsWT' :: t' } -> SmType'T'
    SmWildcardT' :: ( t' ~ SmType'
                    , b' ~ SmBounds' t'
                    , Type' t'
                    , Bounds' t' b'
                    ) => { ()
boundsWT' :: b' } -> SmType'T'

data SmType' where
    T'Apply :: ( n ~ SmName
               , t' ~ SmType'
               , ac' ~ SmArgClauseT' t'
               , ArgClauseT' t' ac'
               ) => SmApplyT' t' ac' -> SmType'
    T'ApplyInfix :: ( t'n ~ SmNameT'
                    , t' ~ SmType'
                    , NameT' t'n
                    , Type' t'
                    ) => SmApplyInfixT' t'n t' -> SmType'
    T'ContextFunction :: ( t' ~ SmType'
                         , Type' t'
                         ) => SmContextFunctionT' t' -> SmType'
    T'Function :: ( t' ~ SmType'
                  , Type' t'
                  ) => SmFunctionT' t' -> SmType'
    T'Lambda :: ( m ~ SmMod
                , n ~ SmName
                , p' ~ SmParamT' m n t' b'
                , t' ~ SmType'
                , b' ~ SmBounds' t'
                , pc' ~ SmParamClauseT' m n p' t' b'
                , ParamClauseT' m n p' t' b' pc'
                ) => SmLambdaT' m n p' t' b' pc' -> SmType'
    T'Lit :: SmLit -> SmType'
    T'Macro :: ( t ~ SmTerm
               , Term t
               ) => SmMacroT' t -> SmType'
    T'Match :: ( t' ~ SmType'
               , ct ~ SmType'CaseCT t'
               , Type'Case t' ct
               ) => SmMatchT' t' ct -> SmType'
    T'PolyFunction :: ( m ~ SmMod
                      , n ~ SmName
                      , p' ~ SmParamT' m n t' b'
                      , t' ~ SmType'
                      , b' ~ SmBounds' t'
                      , pc' ~ SmParamClauseT' m n p' t' b'
                      , ParamClauseT' m n p' t' b' pc'
                      ) => SmPolyFunctionT' m n p' t' b' pc' -> SmType'
    T'Ref :: SmRef' -> SmType'
    T'Tuple :: ( t' ~ SmType'
               , Type' t'
               ) => SmTupleT' t' -> SmType'
    T'Type' :: SmType'T' -> SmType'
    T'Var :: ( t'n ~ SmNameT'
             , NameT' t'n
             ) => SmVarT' t'n -> SmType'

data SmArgClauseT' t' where
    SmArgClauseT' :: ( t' ~ SmType'
                     , Type' t'
                     ) => { forall t'. SmArgClauseT' t' -> [t']
valuesACACT' :: [t'] } -> SmArgClauseT' t'


data SmBounds' t' where
    SmBounds' :: ( t' ~ SmType'
                 , Type' t'
                 ) => { forall t'. SmBounds' t' -> Maybe t'
loB' :: Maybe t'
                      , forall t'. SmBounds' t' -> Maybe t'
hiB' :: Maybe t' } -> SmBounds' t'


data SmType'Def m n t'n p' t' b' pc' where
    T'DType' :: SmType'S m n t'n p' t' b' pc' -> SmType'Def m n t'n p' t' b' pc'
    T'DType :: SmTypeS m n t'n p' t' b' pc' -> SmType'Def m n t'n p' t' b' pc'


data SmParamT' m n t' b' where
    SmParamT' :: ( n ~ SmName
                 , p' ~ SmParamT' m n t' b'
                 , pc' ~ SmParamClauseT' m n p' t' b'
                 , Mod m
                 , Name n
                 , Bounds' t' b'
                 ) => { forall n m t' b'. SmParamT' m n t' b' -> [m]
modsPT' :: [m]
                      , forall n m t' b'. SmParamT' m n t' b' -> n
namePT' :: n
                      , ()
t'paramClausePT' :: pc'
                      , forall n m t' b'. SmParamT' m n t' b' -> b'
tboundsPT' :: b'
                      , forall n m t' b'. SmParamT' m n t' b' -> [t']
vboundsPT' :: [t']
                      , forall n m t' b'. SmParamT' m n t' b' -> [t']
cboundsPT' :: [t'] } -> SmParamT' m n t' b'


data SmParamClauseT' m n p' t' b' where
    SmParamClauseT' :: ( p' ~ SmParamT' m n t' b'
                       , Mod m
                       , Name n
                       , Bounds' t' b'
                       ) => { forall p' m n t' b'. SmParamClauseT' m n p' t' b' -> [p']
valuesPCT' :: [p'] } -> SmParamClauseT' m n p' t' b'