    {-# LANGUAGE DeriveGeneric #-}
    module GHC.Tc.Errors.Types.PromotionErr ( PromotionErr(..)
                                            , pprPECategory
                                            , peCategory
                                            , TermLevelUseErr(..)
                                            , teCategory
                                            ) where

    import GHC.Prelude
    import GHC.Core.Type (ThetaType)
    import GHC.Utils.Outputable
    import GHC.Utils.Misc
    import GHC.Generics (Generic)

    data PromotionErr
      = TyConPE          -- TyCon used in a kind before we are ready
                         --     data T :: T -> * where ...
      | ClassPE          -- Ditto Class

      | FamDataConPE     -- Data constructor for a data family
                         -- See Note [AFamDataCon: not promoting data family constructors]
                         -- in GHC.Tc.Utils.Env.
      | ConstrainedDataConPE ThetaType -- Data constructor with a context
                                       -- See Note [No constraints in kinds] in GHC.Tc.Validity
      | PatSynPE         -- Pattern synonyms
                         -- See Note [Don't promote pattern synonyms] in GHC.Tc.Utils.Env

      | RecDataConPE     -- Data constructor in a recursive loop
                         -- See Note [Recursion and promoting data constructors] in GHC.Tc.TyCl
      | TermVariablePE   -- See Note [Demotion of unqualified variables] in GHC.Rename.Env
      | TypeVariablePE   -- See Note [Type variable scoping errors during typechecking]
      deriving ((forall x. PromotionErr -> Rep PromotionErr x)
    -> (forall x. Rep PromotionErr x -> PromotionErr)
    -> Generic PromotionErr
    forall x. Rep PromotionErr x -> PromotionErr
    forall x. PromotionErr -> Rep PromotionErr x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. PromotionErr -> Rep PromotionErr x
    from :: forall x. PromotionErr -> Rep PromotionErr x
    $cto :: forall x. Rep PromotionErr x -> PromotionErr
    to :: forall x. Rep PromotionErr x -> PromotionErr
    Generic)

    instance Outputable PromotionErr where
      ppr :: PromotionErr -> SDoc
    ppr PromotionErr
    ClassPE              = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "ClassPE"
      ppr PromotionErr
    TyConPE              = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "TyConPE"
      ppr PromotionErr
    PatSynPE             = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "PatSynPE"
      ppr PromotionErr
    FamDataConPE         = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "FamDataConPE"
      ppr (ConstrainedDataConPE ThetaType
    theta) = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "ConstrainedDataConPE" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc
    parens (ThetaType -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr ThetaType
    theta)
      ppr PromotionErr
    RecDataConPE         = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "RecDataConPE"
      ppr PromotionErr
    TermVariablePE       = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "TermVariablePE"
      ppr PromotionErr
    TypeVariablePE       = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "TypeVariablePE"

    pprPECategory :: PromotionErr -> SDoc
    pprPECategory :: PromotionErr -> SDoc
    pprPECategory = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text (String -> SDoc)
    -> (PromotionErr -> String) -> PromotionErr -> SDoc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> String
    capitalise (String -> String)
    -> (PromotionErr -> String) -> PromotionErr -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PromotionErr -> String
    peCategory

    peCategory :: PromotionErr -> String
    peCategory :: PromotionErr -> String
    peCategory PromotionErr
    ClassPE              = String
    "class"
    peCategory PromotionErr
    TyConPE              = String
    "type constructor"
    peCategory PromotionErr
    PatSynPE             = String
    "pattern synonym"
    peCategory PromotionErr
    FamDataConPE         = String
    "data constructor"
    peCategory ConstrainedDataConPE{} = String
    "data constructor"
    peCategory PromotionErr
    RecDataConPE         = String
    "data constructor"
    peCategory PromotionErr
    TermVariablePE       = String
    "term variable"
    peCategory PromotionErr
    TypeVariablePE       = String
    "type variable"

    -- The opposite of a promotion error (a demotion error, in a sense).
    data TermLevelUseErr
      = TyConTE   -- Type constructor used at the term level, e.g. x = Int
      | ClassTE   -- Class used at the term level,            e.g. x = Functor
      | TyVarTE   -- Type variable used at the term level,    e.g. f (Proxy :: Proxy a) = a
      deriving ((forall x. TermLevelUseErr -> Rep TermLevelUseErr x)
    -> (forall x. Rep TermLevelUseErr x -> TermLevelUseErr)
    -> Generic TermLevelUseErr
    forall x. Rep TermLevelUseErr x -> TermLevelUseErr
    forall x. TermLevelUseErr -> Rep TermLevelUseErr x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. TermLevelUseErr -> Rep TermLevelUseErr x
    from :: forall x. TermLevelUseErr -> Rep TermLevelUseErr x
    $cto :: forall x. Rep TermLevelUseErr x -> TermLevelUseErr
    to :: forall x. Rep TermLevelUseErr x -> TermLevelUseErr
    Generic)

    teCategory :: TermLevelUseErr -> String
    teCategory :: TermLevelUseErr -> String
    teCategory TermLevelUseErr
    ClassTE = String
    "class"
    teCategory TermLevelUseErr
    TyConTE = String
    "type constructor"
    teCategory TermLevelUseErr
    TyVarTE = String
    "type variable"

    {- Note [Type variable scoping errors during typechecking]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Consider the scoping of the type variable `a` in the following
    term-level example:

      -- f :: [forall b . Either b ()]
      f = [Right @a @() () :: forall a. Either a ()]

    Here `@a` in the type application and `a` in the type signature refer to
    the same type variable. Indeed, this term elaborates to the following Core:

      f = [(\@a -> Right @a @() ()) :: forall a . Either a ()]

    But how does this work with types? Suppose we have:

      type F = '[Right @a @() () :: forall a. Either a ()]

    To be consistent with the term-level language, we would have to elaborate
    this using a big lambda:

      type F = '[(/\ a . Right @a @() ()) :: forall a. Either a ()]

    Core has no such construct, so this is not a valid type.

    Conclusion: Even with -XExtendedForAllScope, the forall'd variables of a
    kind signature on a type cannot scope over the type.

    In implementation terms, to get a helpful error message we do this:

    * The renamer treats the type variable as bound by the forall
      (so it doesn't just say "out of scope"); see the `HsKindSig` case of GHC.Rename.HsType.rnHsTyKi.

    * The typechecker adds the forall-bound type variables to the type environent,
      but bound to `APromotionErr TypeVariablePE`; see the call to `tcAddKindSigPlaceholders`
      in the `HsKindSig` case of `GHC.Tc.Gen.HsType.tc_infer_hs_type`.

    * The occurrence site of a type variable then complains when it finds `APromotionErr`;
      see `GHC.Tc.Gen.HsType.tcTyVar`.
    -}