{-# 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`.
-}