{- Data/Singletons/TH/Promote.hs

(c) Richard Eisenberg 2013
rae@cs.brynmawr.edu

This file contains functions to promote term-level constructs to the
type level. It is an internal module to the singletons-th package.
-}

module Data.Singletons.TH.Promote where

import Language.Haskell.TH hiding ( Q, cxt )
import Language.Haskell.TH.Syntax ( NameSpace(..), Quasi(..), Uniq )
import Language.Haskell.TH.Desugar
import qualified Language.Haskell.TH.Desugar.OMap.Strict as OMap
import Language.Haskell.TH.Desugar.OMap.Strict (OMap)
import qualified Language.Haskell.TH.Desugar.OSet as OSet
import Language.Haskell.TH.Desugar.OSet (OSet)
import qualified Language.Haskell.TH.Desugar.Subst.Capturing as SC
import Data.Singletons.TH.Deriving.Bounded
import Data.Singletons.TH.Deriving.Enum
import Data.Singletons.TH.Deriving.Eq
import Data.Singletons.TH.Deriving.Ord
import Data.Singletons.TH.Deriving.Show
import Data.Singletons.TH.Deriving.Util
import Data.Singletons.TH.Names
import Data.Singletons.TH.Options
import Data.Singletons.TH.Partition
import Data.Singletons.TH.Promote.Defun
import Data.Singletons.TH.Promote.Monad
import Data.Singletons.TH.Promote.Type
import Data.Singletons.TH.Syntax
import Data.Singletons.TH.Util
import Prelude hiding (exp)
import Control.Applicative (Alternative(..))
import Control.Arrow (second)
import Control.Monad
import Control.Monad.Trans.Maybe
import Control.Monad.Writer
import Data.Function (on)
import Data.List (deleteFirstsBy, nub)
import qualified Data.Map.Strict as Map
import Data.Map.Strict ( Map )
import Data.Maybe
import qualified GHC.LanguageExtensions.Type as LangExt

{-
Note [Disable genQuotedDecs in genPromotions and genSingletons]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Somewhat curiously, the genPromotions and genSingletons functions set the
genQuotedDecs option to False, despite neither function accepting quoted
declarations as arguments in the first place. There is a good reason for doing
this, however. Imagine this code:

  class C a where
    infixl 9 <%%>
    (<%%>) :: a -> a -> a
  $(genPromotions [''C])

If genQuotedDecs is set to True, then the (<%%>) type family will not receive
a fixity declaration (see
Note [singletons-th and fixity declarations] in D.S.TH.Single.Fixity, wrinkle 1 for
more details on this point). Therefore, we set genQuotedDecs to False to avoid
this problem.
-}

-- | Generate promoted definitions for each of the provided type-level
-- declaration 'Name's. This is generally only useful with classes.
genPromotions :: OptionsMonad q => [Name] -> q [Dec]
genPromotions :: forall (q :: * -> *). OptionsMonad q => [Name] -> q [Dec]
genPromotions [Name]
names = do
  opts <- q Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  -- See Note [Disable genQuotedDecs in genPromotions and genSingletons]
  withOptions opts{genQuotedDecs = False} $ do
    checkForRep names
    infos <- mapM reifyWithLocals names
    dinfos <- mapM dsInfo infos
    ddecs <- promoteM_ [] $ mapM_ promoteInfo dinfos
    return $ decsToTH ddecs

-- | Promote every declaration given to the type level, retaining the originals.
-- See the
-- @<https://github.com/goldfirere/singletons/blob/master/README.md README>@
-- for further explanation.
promote :: OptionsMonad q => q [Dec] -> q [Dec]
promote :: forall (q :: * -> *). OptionsMonad q => q [Dec] -> q [Dec]
promote q [Dec]
qdecs = do
  opts <- q Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  withOptions opts{genQuotedDecs = True} $ promote' $ lift qdecs

-- | Promote each declaration, discarding the originals. Note that a promoted
-- datatype uses the same definition as an original datatype, so this will
-- not work with datatypes. Classes, instances, and functions are all fine.
promoteOnly :: OptionsMonad q => q [Dec] -> q [Dec]
promoteOnly :: forall (q :: * -> *). OptionsMonad q => q [Dec] -> q [Dec]
promoteOnly q [Dec]
qdecs = do
  opts <- q Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  withOptions opts{genQuotedDecs = False} $ promote' $ lift qdecs

-- The workhorse for 'promote' and 'promoteOnly'. The difference between the
-- two functions is whether 'genQuotedDecs' is set to 'True' or 'False'.
promote' :: OptionsMonad q => q [Dec] -> q [Dec]
promote' :: forall (q :: * -> *). OptionsMonad q => q [Dec] -> q [Dec]
promote' q [Dec]
qdecs = do
  opts     <- q Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  decs     <- qdecs
  ddecs    <- withLocalDeclarations decs $ dsDecs decs
  promDecs <- promoteM_ decs $ promoteDecs ddecs
  let origDecs | Options -> Bool
genQuotedDecs Options
opts = [Dec]
decs
               | Bool
otherwise          = []
  return $ origDecs ++ decsToTH promDecs

-- | Generate defunctionalization symbols for each of the provided type-level
-- declaration 'Name's. See the "Promotion and partial application" section of
-- the @singletons@
-- @<https://github.com/goldfirere/singletons/blob/master/README.md README>@
-- for further explanation.
genDefunSymbols :: OptionsMonad q => [Name] -> q [Dec]
genDefunSymbols :: forall (q :: * -> *). OptionsMonad q => [Name] -> q [Dec]
genDefunSymbols [Name]
names = do
  [Name] -> q ()
forall (q :: * -> *). Quasi q => [Name] -> q ()
checkForRep [Name]
names
  infos <- (Name -> q DInfo) -> [Name] -> q [DInfo]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Info -> q DInfo
forall (q :: * -> *). DsMonad q => Info -> q DInfo
dsInfo (Info -> q DInfo) -> (Name -> q Info) -> Name -> q DInfo
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Name -> q Info
forall (q :: * -> *). DsMonad q => Name -> q Info
reifyWithLocals) [Name]
names
  decs <- promoteMDecs [] $ concatMapM defunInfo infos
  return $ decsToTH decs

-- | Produce instances for @PEq@ from the given types
promoteEqInstances :: OptionsMonad q => [Name] -> q [Dec]
promoteEqInstances :: forall (q :: * -> *). OptionsMonad q => [Name] -> q [Dec]
promoteEqInstances = (Name -> q [Dec]) -> [Name] -> q [Dec]
forall (monad :: * -> *) monoid (t :: * -> *) a.
(Monad monad, Monoid monoid, Traversable t) =>
(a -> monad monoid) -> t a -> monad monoid
concatMapM Name -> q [Dec]
forall (q :: * -> *). OptionsMonad q => Name -> q [Dec]
promoteEqInstance

-- | Produce an instance for @PEq@ from the given type
promoteEqInstance :: OptionsMonad q => Name -> q [Dec]
promoteEqInstance :: forall (q :: * -> *). OptionsMonad q => Name -> q [Dec]
promoteEqInstance = DerivDesc q -> String -> Name -> q [Dec]
forall (q :: * -> *).
OptionsMonad q =>
DerivDesc q -> String -> Name -> q [Dec]
promoteInstance DerivDesc q
forall (q :: * -> *). DsMonad q => DerivDesc q
mkEqInstance String
"Eq"

-- | Produce instances for 'POrd' from the given types
promoteOrdInstances :: OptionsMonad q => [Name] -> q [Dec]
promoteOrdInstances :: forall (q :: * -> *). OptionsMonad q => [Name] -> q [Dec]
promoteOrdInstances = (Name -> q [Dec]) -> [Name] -> q [Dec]
forall (monad :: * -> *) monoid (t :: * -> *) a.
(Monad monad, Monoid monoid, Traversable t) =>
(a -> monad monoid) -> t a -> monad monoid
concatMapM Name -> q [Dec]
forall (q :: * -> *). OptionsMonad q => Name -> q [Dec]
promoteOrdInstance

-- | Produce an instance for 'POrd' from the given type
promoteOrdInstance :: OptionsMonad q => Name -> q [Dec]
promoteOrdInstance :: forall (q :: * -> *). OptionsMonad q => Name -> q [Dec]
promoteOrdInstance = DerivDesc q -> String -> Name -> q [Dec]
forall (q :: * -> *).
OptionsMonad q =>
DerivDesc q -> String -> Name -> q [Dec]
promoteInstance DerivDesc q
forall (q :: * -> *). DsMonad q => DerivDesc q
mkOrdInstance String
"Ord"

-- | Produce instances for 'PBounded' from the given types
promoteBoundedInstances :: OptionsMonad q => [Name] -> q [Dec]
promoteBoundedInstances :: forall (q :: * -> *). OptionsMonad q => [Name] -> q [Dec]
promoteBoundedInstances = (Name -> q [Dec]) -> [Name] -> q [Dec]
forall (monad :: * -> *) monoid (t :: * -> *) a.
(Monad monad, Monoid monoid, Traversable t) =>
(a -> monad monoid) -> t a -> monad monoid
concatMapM Name -> q [Dec]
forall (q :: * -> *). OptionsMonad q => Name -> q [Dec]
promoteBoundedInstance

-- | Produce an instance for 'PBounded' from the given type
promoteBoundedInstance :: OptionsMonad q => Name -> q [Dec]
promoteBoundedInstance :: forall (q :: * -> *). OptionsMonad q => Name -> q [Dec]
promoteBoundedInstance = DerivDesc q -> String -> Name -> q [Dec]
forall (q :: * -> *).
OptionsMonad q =>
DerivDesc q -> String -> Name -> q [Dec]
promoteInstance DerivDesc q
forall (q :: * -> *). DsMonad q => DerivDesc q
mkBoundedInstance String
"Bounded"

-- | Produce instances for 'PEnum' from the given types
promoteEnumInstances :: OptionsMonad q => [Name] -> q [Dec]
promoteEnumInstances :: forall (q :: * -> *). OptionsMonad q => [Name] -> q [Dec]
promoteEnumInstances = (Name -> q [Dec]) -> [Name] -> q [Dec]
forall (monad :: * -> *) monoid (t :: * -> *) a.
(Monad monad, Monoid monoid, Traversable t) =>
(a -> monad monoid) -> t a -> monad monoid
concatMapM Name -> q [Dec]
forall (q :: * -> *). OptionsMonad q => Name -> q [Dec]
promoteEnumInstance

-- | Produce an instance for 'PEnum' from the given type
promoteEnumInstance :: OptionsMonad q => Name -> q [Dec]
promoteEnumInstance :: forall (q :: * -> *). OptionsMonad q => Name -> q [Dec]
promoteEnumInstance = DerivDesc q -> String -> Name -> q [Dec]
forall (q :: * -> *).
OptionsMonad q =>
DerivDesc q -> String -> Name -> q [Dec]
promoteInstance DerivDesc q
forall (q :: * -> *). DsMonad q => DerivDesc q
mkEnumInstance String
"Enum"

-- | Produce instances for 'PShow' from the given types
promoteShowInstances :: OptionsMonad q => [Name] -> q [Dec]
promoteShowInstances :: forall (q :: * -> *). OptionsMonad q => [Name] -> q [Dec]
promoteShowInstances = (Name -> q [Dec]) -> [Name] -> q [Dec]
forall (monad :: * -> *) monoid (t :: * -> *) a.
(Monad monad, Monoid monoid, Traversable t) =>
(a -> monad monoid) -> t a -> monad monoid
concatMapM Name -> q [Dec]
forall (q :: * -> *). OptionsMonad q => Name -> q [Dec]
promoteShowInstance

-- | Produce an instance for 'PShow' from the given type
promoteShowInstance :: OptionsMonad q => Name -> q [Dec]
promoteShowInstance :: forall (q :: * -> *). OptionsMonad q => Name -> q [Dec]
promoteShowInstance = DerivDesc q -> String -> Name -> q [Dec]
forall (q :: * -> *).
OptionsMonad q =>
DerivDesc q -> String -> Name -> q [Dec]
promoteInstance DerivDesc q
forall (q :: * -> *). OptionsMonad q => DerivDesc q
mkShowInstance String
"Show"

promoteInstance :: OptionsMonad q => DerivDesc q -> String -> Name -> q [Dec]
promoteInstance :: forall (q :: * -> *).
OptionsMonad q =>
DerivDesc q -> String -> Name -> q [Dec]
promoteInstance DerivDesc q
mk_inst String
class_name Name
name = do
  (df, tvbs, cons) <- String -> Name -> q (DataFlavor, [TyVarBndrVis], [Con])
forall (q :: * -> *).
DsMonad q =>
String -> Name -> q (DataFlavor, [TyVarBndrVis], [Con])
getDataD (String
"I cannot make an instance of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
class_name
                                String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" for it.") Name
name
  dtvbs <- mapM dsTvbVis tvbs
  let data_ty   = DType -> [DTyVarBndrVis] -> DType
foldTypeTvbs (Name -> DType
DConT Name
name) [DTyVarBndrVis]
dtvbs
      dtvbSpecs = Specificity -> [DTyVarBndrVis] -> [DTyVarBndr Specificity]
forall newFlag oldFlag.
newFlag -> [DTyVarBndr oldFlag] -> [DTyVarBndr newFlag]
changeDTVFlags Specificity
SpecifiedSpec [DTyVarBndrVis]
dtvbs
  cons' <- concatMapM (dsCon dtvbSpecs data_ty) cons
  let data_decl = DataFlavor -> Name -> [DTyVarBndrVis] -> [DCon] -> DataDecl
DataDecl DataFlavor
df Name
name [DTyVarBndrVis]
dtvbs [DCon]
cons'
  raw_inst <- mk_inst Nothing data_ty data_decl
  decs <- promoteM_ [] $ void $
          promoteInstanceDec OMap.empty Map.empty raw_inst
  return $ decsToTH decs

promoteInfo :: DInfo -> PrM ()
promoteInfo :: DInfo -> PrM ()
promoteInfo (DTyConI DDec
dec Maybe [DDec]
_instances) = [DDec] -> PrM ()
promoteDecs [DDec
dec]
promoteInfo (DPrimTyConI Name
_name Int
_numArgs Bool
_unlifted) =
  String -> PrM ()
forall a. String -> PrM a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Promotion of primitive type constructors not supported"
promoteInfo (DVarI Name
_name DType
_ty Maybe Name
_mdec) =
  String -> PrM ()
forall a. String -> PrM a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Promotion of individual values not supported"
promoteInfo (DTyVarI Name
_name DType
_ty) =
  String -> PrM ()
forall a. String -> PrM a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Promotion of individual type variables not supported"
promoteInfo (DPatSynI {}) =
  String -> PrM ()
forall a. String -> PrM a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Promotion of pattern synonyms not supported"

-- Promote a list of top-level declarations.
promoteDecs :: [DDec] -> PrM ()
promoteDecs :: [DDec] -> PrM ()
promoteDecs [DDec]
raw_decls = do
  decls <- [DDec] -> PrM [DDec]
forall (q :: * -> *) a. (DsMonad q, Data a) => a -> q a
expand [DDec]
raw_decls     -- expand type synonyms
  checkForRepInDecls decls
  PDecs { pd_let_decs                = let_decs
        , pd_class_decs              = classes
        , pd_instance_decs           = insts
        , pd_data_decs               = datas
        , pd_ty_syn_decs             = ty_syns
        , pd_open_type_family_decs   = o_tyfams
        , pd_closed_type_family_decs = c_tyfams } <- partitionDecs decls

  defunTopLevelTypeDecls ty_syns c_tyfams o_tyfams
  rec_sel_let_decs <- promoteDataDecs datas
    -- promoteLetDecs returns LetBinds, which we don't need at top level
  _ <- promoteLetDecs Nothing $ rec_sel_let_decs ++ let_decs
  mapM_ promoteClassDec classes
  let orig_meth_sigs = (UClassDecl -> OMap Name DType) -> [UClassDecl] -> OMap Name DType
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (LetDecEnv Unannotated -> OMap Name DType
forall (ann :: AnnotationFlag). LetDecEnv ann -> OMap Name DType
lde_types (LetDecEnv Unannotated -> OMap Name DType)
-> (UClassDecl -> LetDecEnv Unannotated)
-> UClassDecl
-> OMap Name DType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UClassDecl -> LetDecEnv Unannotated
forall (ann :: AnnotationFlag). ClassDecl ann -> LetDecEnv ann
cd_lde) [UClassDecl]
classes
      cls_tvbs_map   = [(Name, [DTyVarBndrVis])] -> Map Name [DTyVarBndrVis]
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Name, [DTyVarBndrVis])] -> Map Name [DTyVarBndrVis])
-> [(Name, [DTyVarBndrVis])] -> Map Name [DTyVarBndrVis]
forall a b. (a -> b) -> a -> b
$ (UClassDecl -> (Name, [DTyVarBndrVis]))
-> [UClassDecl] -> [(Name, [DTyVarBndrVis])]
forall a b. (a -> b) -> [a] -> [b]
map (\UClassDecl
cd -> (UClassDecl -> Name
forall (ann :: AnnotationFlag). ClassDecl ann -> Name
cd_name UClassDecl
cd, UClassDecl -> [DTyVarBndrVis]
forall (ann :: AnnotationFlag). ClassDecl ann -> [DTyVarBndrVis]
cd_tvbs UClassDecl
cd)) [UClassDecl]
classes
  mapM_ (promoteInstanceDec orig_meth_sigs cls_tvbs_map) insts

-- curious about ALetDecEnv? See the LetDecEnv module for an explanation.
promoteLetDecs :: Maybe Uniq -- let-binding unique (if locally bound)
               -> [DLetDec] -> PrM ([LetBind], ALetDecEnv)
promoteLetDecs :: Maybe Uniq -> [DLetDec] -> PrM ([LetBind], ALetDecEnv)
promoteLetDecs Maybe Uniq
mb_let_uniq [DLetDec]
decls = do
  opts <- PrM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  let_dec_env <- buildLetDecEnv decls
  all_locals <- allLocals
  let let_dec_proms :: [(Name, LetDecProm)]
      let_dec_proms =
        [ (Name
name, (Name
pro_name, [LocalVar]
all_locals))
        | (Name
name, LetDecRHS Unannotated
_) <- OMap Name (LetDecRHS Unannotated)
-> [(Name, LetDecRHS Unannotated)]
forall k v. OMap k v -> [(k, v)]
OMap.assocs (OMap Name (LetDecRHS Unannotated)
 -> [(Name, LetDecRHS Unannotated)])
-> OMap Name (LetDecRHS Unannotated)
-> [(Name, LetDecRHS Unannotated)]
forall a b. (a -> b) -> a -> b
$ LetDecEnv Unannotated -> OMap Name (LetDecRHS Unannotated)
forall (ann :: AnnotationFlag).
LetDecEnv ann -> OMap Name (LetDecRHS ann)
lde_defns LetDecEnv Unannotated
let_dec_env
        , let pro_name :: Name
pro_name = Options -> Name -> Maybe Uniq -> Name
promotedValueName Options
opts Name
name Maybe Uniq
mb_let_uniq ]

      binds :: [LetBind]
      binds =
        [ (Name
name, DType -> [LocalVar] -> DType
foldTypeLocalVars (Name -> DType
DConT Name
sym) [LocalVar]
locals)
        | (Name
name, (Name
pro_name, [LocalVar]
locals)) <- [(Name, LetDecProm)]
let_dec_proms
        , let sym :: Name
sym = Options -> Name -> Name
defunctionalizedName0 Options
opts Name
pro_name ]
  (decs, let_dec_env') <- letBind binds $ promoteLetDecEnv mb_let_uniq let_dec_env
  emitDecs decs
  return (binds, let_dec_env' { lde_proms = OMap.fromList let_dec_proms })

promoteDataDecs :: [DataDecl] -> PrM [DLetDec]
promoteDataDecs :: [DataDecl] -> PrM [DLetDec]
promoteDataDecs = (DataDecl -> PrM [DLetDec]) -> [DataDecl] -> PrM [DLetDec]
forall (monad :: * -> *) monoid (t :: * -> *) a.
(Monad monad, Monoid monoid, Traversable t) =>
(a -> monad monoid) -> t a -> monad monoid
concatMapM DataDecl -> PrM [DLetDec]
promoteDataDec

-- "Promotes" a data type, much like D.S.TH.Single.Data.singDataD singles a data
-- type. Promoting a data type is much easier than singling it, however, since
-- DataKinds automatically promotes data types and kinds and data constructors
-- to types. That means that promoteDataDec only has to do three things:
--
-- 1. Emit defunctionalization symbols for each data constructor,
--
-- 2. Emit promoted fixity declarations for each data constructor and promoted
--    record selector (assuming the originals have fixity declarations), and
--
-- 3. Assemble a top-level function that mimics the behavior of its record
--    selectors. Note that promoteDataDec does not actually promote this record
--    selector function—it merely returns its DLetDecs. Later, the promoteDecs
--    function takes these DLetDecs and promotes them (using promoteLetDecs).
--    This greatly simplifies the plumbing, since this allows all DLetDecs to
--    be promoted in a single location.
--    See Note [singletons-th and record selectors] in D.S.TH.Single.Data.
--
-- Note that if @NoFieldSelectors@ is active, then neither steps (2) nor (3)
-- will promote any records to top-level field selectors.
promoteDataDec :: DataDecl -> PrM [DLetDec]
promoteDataDec :: DataDecl -> PrM [DLetDec]
promoteDataDec (DataDecl DataFlavor
_ Name
_ [DTyVarBndrVis]
_ [DCon]
ctors) = do
  let rec_sel_names :: [Name]
rec_sel_names = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ (DCon -> [Name]) -> [DCon] -> [Name]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap DCon -> [Name]
extractRecSelNames [DCon]
ctors
                      -- Note the use of nub: the same record selector name can
                      -- be used in multiple constructors!
  fld_sels         <- Extension -> PrM Bool
forall (m :: * -> *). Quasi m => Extension -> m Bool
qIsExtEnabled Extension
LangExt.FieldSelectors
  rec_sel_let_decs <- if fld_sels then getRecordSelectors ctors else pure []
  ctorSyms         <- buildDefunSymsDataD ctors
  -- NB: If NoFieldSelectors is active, then promoteReifiedInfixDecls will not
  -- promote any of `rec_sel_names` to field selectors, so there is no need to
  -- check for it here.
  infix_decs       <- promoteReifiedInfixDecls rec_sel_names
  emitDecs $ ctorSyms ++ infix_decs
  pure rec_sel_let_decs

promoteClassDec :: UClassDecl -> PrM AClassDecl
promoteClassDec :: UClassDecl -> PrM AClassDecl
promoteClassDec decl :: UClassDecl
decl@(ClassDecl { cd_name :: forall (ann :: AnnotationFlag). ClassDecl ann -> Name
cd_name = Name
cls_name
                                , cd_tvbs :: forall (ann :: AnnotationFlag). ClassDecl ann -> [DTyVarBndrVis]
cd_tvbs = [DTyVarBndrVis]
orig_cls_tvbs
                                , cd_fds :: forall (ann :: AnnotationFlag). ClassDecl ann -> [FunDep]
cd_fds  = [FunDep]
fundeps
                                , cd_atfs :: forall (ann :: AnnotationFlag).
ClassDecl ann -> [OpenTypeFamilyDecl]
cd_atfs = [OpenTypeFamilyDecl]
atfs
                                , cd_lde :: forall (ann :: AnnotationFlag). ClassDecl ann -> LetDecEnv ann
cd_lde  = lde :: LetDecEnv Unannotated
lde@LetDecEnv
                                    { lde_defns :: forall (ann :: AnnotationFlag).
LetDecEnv ann -> OMap Name (LetDecRHS ann)
lde_defns = OMap Name (LetDecRHS Unannotated)
defaults
                                    , lde_types :: forall (ann :: AnnotationFlag). LetDecEnv ann -> OMap Name DType
lde_types = OMap Name DType
meth_sigs
                                    , lde_infix :: forall (ann :: AnnotationFlag).
LetDecEnv ann -> OMap Name (Fixity, NamespaceSpecifier)
lde_infix = OMap Name (Fixity, NamespaceSpecifier)
infix_decls } }) = do
  opts <- PrM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  let pClsName       = Options -> Name -> Name
promotedClassName Options
opts Name
cls_name
      meth_sigs_list = OMap Name DType -> [LetBind]
forall k v. OMap k v -> [(k, v)]
OMap.assocs OMap Name DType
meth_sigs
      meth_names     = (LetBind -> Name) -> [LetBind] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map LetBind -> Name
forall a b. (a, b) -> a
fst [LetBind]
meth_sigs_list
      defaults_list  = OMap Name (LetDecRHS Unannotated)
-> [(Name, LetDecRHS Unannotated)]
forall k v. OMap k v -> [(k, v)]
OMap.assocs OMap Name (LetDecRHS Unannotated)
defaults
      defaults_names = ((Name, LetDecRHS Unannotated) -> Name)
-> [(Name, LetDecRHS Unannotated)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, LetDecRHS Unannotated) -> Name
forall a b. (a, b) -> a
fst [(Name, LetDecRHS Unannotated)]
defaults_list
  mb_cls_sak <- dsReifyType cls_name

  -- If the class has a standalone kind signature, we take the original,
  -- user-written class binders (`orig_cls_tvbs`) and fill them out using
  -- `dMatchUpSAKWithDecl` to produce the "full" binders, as described in
  -- Note [Propagating kind information from class standalone kind signatures].
  mb_full_cls_tvbs <-
    traverse (\DType
cls_sak -> DType -> [DTyVarBndrVis] -> PrM [DTyVarBndr ForAllTyFlag]
forall (q :: * -> *).
MonadFail q =>
DType -> [DTyVarBndrVis] -> q [DTyVarBndr ForAllTyFlag]
dMatchUpSAKWithDecl DType
cls_sak [DTyVarBndrVis]
orig_cls_tvbs) mb_cls_sak
  let mb_full_cls_tvbs_spec = [DTyVarBndr ForAllTyFlag] -> [DTyVarBndr Specificity]
dtvbForAllTyFlagsToSpecs ([DTyVarBndr ForAllTyFlag] -> [DTyVarBndr Specificity])
-> Maybe [DTyVarBndr ForAllTyFlag]
-> Maybe [DTyVarBndr Specificity]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe [DTyVarBndr ForAllTyFlag]
mb_full_cls_tvbs
      -- The class binders, converted to `DTyVarBndrSpec`s. If the parent class
      -- has a standalone kind signature, we compute these `DTyVarBndrSpec`s
      -- from the full class binders, which likely have richer kind information.
      -- Otherwise, we compute these from the original, user-written class
      -- binders.
      cls_tvbs_spec = [DTyVarBndr Specificity]
-> Maybe [DTyVarBndr Specificity] -> [DTyVarBndr Specificity]
forall a. a -> Maybe a -> a
fromMaybe
                        (Specificity -> [DTyVarBndrVis] -> [DTyVarBndr Specificity]
forall newFlag oldFlag.
newFlag -> [DTyVarBndr oldFlag] -> [DTyVarBndr newFlag]
changeDTVFlags Specificity
SpecifiedSpec [DTyVarBndrVis]
orig_cls_tvbs)
                        Maybe [DTyVarBndr Specificity]
mb_full_cls_tvbs_spec

  sig_decs <- mapM (uncurry (promote_sig mb_full_cls_tvbs_spec)) meth_sigs_list
  (default_decs, ann_rhss, prom_rhss)
    <- mapAndUnzip3M (promoteMethod DefaultMethods meth_sigs cls_tvbs_spec) defaults_list
  defunAssociatedTypeFamilies orig_cls_tvbs atfs

  infix_decls' <- mapMaybeM (\(Name
n, (Fixity
f, NamespaceSpecifier
ns)) -> Maybe Uniq
-> Name -> Fixity -> NamespaceSpecifier -> PrM (Maybe DDec)
forall (q :: * -> *).
OptionsMonad q =>
Maybe Uniq
-> Name -> Fixity -> NamespaceSpecifier -> q (Maybe DDec)
promoteInfixDecl Maybe Uniq
forall a. Maybe a
Nothing Name
n Fixity
f NamespaceSpecifier
ns) $
                  OMap.assocs infix_decls
  cls_infix_decls <- promoteReifiedInfixDecls $ cls_name:meth_names

  -- no need to do anything to the fundeps. They work as is!
  let pro_cls_dec = DCxt -> Name -> [DTyVarBndrVis] -> [FunDep] -> [DDec] -> DDec
DClassD [] Name
pClsName [DTyVarBndrVis]
orig_cls_tvbs [FunDep]
fundeps
                            ([DDec]
sig_decs [DDec] -> [DDec] -> [DDec]
forall a. [a] -> [a] -> [a]
++ [DDec]
default_decs [DDec] -> [DDec] -> [DDec]
forall a. [a] -> [a] -> [a]
++ [DDec]
infix_decls')
      mb_pro_cls_sak = (DType -> DDec) -> Maybe DType -> Maybe DDec
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name -> DType -> DDec
DKiSigD Name
pClsName) Maybe DType
mb_cls_sak
  emitDecs $ maybeToList mb_pro_cls_sak ++ pro_cls_dec:cls_infix_decls
  let defaults_list' = [Name] -> [ALetDecRHS] -> [(Name, ALetDecRHS)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
defaults_names [ALetDecRHS]
ann_rhss
      proms          = [Name] -> [LetDecProm] -> [(Name, LetDecProm)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
defaults_names [LetDecProm]
prom_rhss
  return (decl { cd_lde = lde { lde_defns = OMap.fromList defaults_list'
                              , lde_proms = OMap.fromList proms } })
  where
    -- Promote a class method's type signature to an associated type family.
    promote_sig ::
         Maybe [DTyVarBndrSpec]
         -- ^ If the parent class has a standalone kind signature, then this
         -- will be @'Just' full_bndrs@, where @full_bndrs@ are the full type
         -- variable binders described in @Note [Propagating kind information
         -- from class standalone kind signatures]@. Otherwise, this will be
         -- 'Nothing'.
      -> Name
         -- ^ The class method's name.
      -> DType
         -- ^ The class method's type.
      -> PrM DDec
         -- ^ The associated type family for the promoted class method.
    promote_sig :: Maybe [DTyVarBndr Specificity] -> Name -> DType -> PrM DDec
promote_sig Maybe [DTyVarBndr Specificity]
mb_full_cls_tvbs_spec Name
name DType
meth_ty = do
      opts <- PrM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
      let proName = Options -> Name -> Name
promotedTopLevelValueName Options
opts Name
name
      (_, meth_arg_kis, meth_res_ki) <- promoteUnraveled meth_ty
      args <- mapM (const $ qNewName "arg") meth_arg_kis
      let pro_meth_args = (Name -> DType -> DTyVarBndrVis)
-> [Name] -> DCxt -> [DTyVarBndrVis]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Name -> BndrVis -> DType -> DTyVarBndrVis
forall flag. Name -> flag -> DType -> DTyVarBndr flag
`DKindedTV` BndrVis
BndrReq) [Name]
args DCxt
meth_arg_kis
          -- Binders for all of the type variables mentioned in the argument and
          -- result kinds of the promoted class method. This includes both class
          -- variables and variables that only scope over the method itself.
          --
          -- This quantifies the variables in a simple left-to-right order,
          -- which may not be the same order in which the original method's type
          -- quantifies them. This is a known limitation: see
          -- Note [Promoted class methods and kind variable ordering].
          meth_tvbs = Specificity -> [DTyVarBndr ()] -> [DTyVarBndr Specificity]
forall newFlag oldFlag.
newFlag -> [DTyVarBndr oldFlag] -> [DTyVarBndr newFlag]
changeDTVFlags Specificity
SpecifiedSpec ([DTyVarBndr ()] -> [DTyVarBndr Specificity])
-> [DTyVarBndr ()] -> [DTyVarBndr Specificity]
forall a b. (a -> b) -> a -> b
$
                      DCxt -> [DTyVarBndr ()]
toposortTyVarsOf (DCxt -> [DTyVarBndr ()]) -> DCxt -> [DTyVarBndr ()]
forall a b. (a -> b) -> a -> b
$ DCxt
meth_arg_kis DCxt -> DCxt -> DCxt
forall a. [a] -> [a] -> [a]
++ [DType
meth_res_ki]
          -- The type variable binders to use in the standalone kind signatures
          -- for the promoted class method's defunctionalization symbols.
          meth_sak_tvbs =
            case Maybe [DTyVarBndr Specificity]
mb_full_cls_tvbs_spec of
              -- If the parent class has a standalone kind signature, then
              -- propagate as much of the kind information as possible by
              -- incorporating the full class binders. See Note [Propagating
              -- kind information from class standalone kind signatures].
              Just [DTyVarBndr Specificity]
full_cls_tvbs_spec ->
                -- `meth_tvbs` can include class binder names, so make sure to
                -- delete type variables from `meth_tvbs` whose names are also
                -- bound by the full class binders.
                let meth_tvbs_without_cls_tvbs :: [DTyVarBndr Specificity]
meth_tvbs_without_cls_tvbs =
                      (DTyVarBndr Specificity -> DTyVarBndr Specificity -> Bool)
-> [DTyVarBndr Specificity]
-> [DTyVarBndr Specificity]
-> [DTyVarBndr Specificity]
forall a. (a -> a -> Bool) -> [a] -> [a] -> [a]
deleteFirstsBy
                        (Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Name -> Name -> Bool)
-> (DTyVarBndr Specificity -> Name)
-> DTyVarBndr Specificity
-> DTyVarBndr Specificity
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` DTyVarBndr Specificity -> Name
forall flag. DTyVarBndr flag -> Name
extractTvbName)
                        [DTyVarBndr Specificity]
meth_tvbs
                        [DTyVarBndr Specificity]
full_cls_tvbs_spec in
                [DTyVarBndr Specificity]
full_cls_tvbs_spec [DTyVarBndr Specificity]
-> [DTyVarBndr Specificity] -> [DTyVarBndr Specificity]
forall a. [a] -> [a] -> [a]
++ [DTyVarBndr Specificity]
meth_tvbs_without_cls_tvbs
              -- If the parent class lacks a standalone kind signature, then we
              -- simply return `meth_tvbs`.
              Maybe [DTyVarBndr Specificity]
Nothing ->
                [DTyVarBndr Specificity]
meth_tvbs
          meth_sak = [DTyVarBndr Specificity] -> DCxt -> DCxt -> DType -> DType
ravelVanillaDType [DTyVarBndr Specificity]
meth_sak_tvbs [] DCxt
meth_arg_kis DType
meth_res_ki
      m_fixity <- reifyFixityWithLocals name
      emitDecsM $ defunctionalize proName m_fixity $ DefunSAK meth_sak

      return $ DOpenTypeFamilyD (DTypeFamilyHead proName
                                                 pro_meth_args
                                                 (DKindSig meth_res_ki)
                                                 Nothing)

{-
Note [Promoted class methods and kind variable ordering]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In general, we make an effort to preserve the order of type variables when
promoting type signatures, but there is an annoying corner case where this is
difficult: class methods. When promoting class methods, the order of kind
variables in their kinds will often "just work" by happy coincidence, but
there are some situations where this does not happen. Consider the following
class:

  class C (b :: Type) where
    m :: forall a. a -> b -> a

The full type of `m` is `forall b. C b => forall a. a -> b -> a`, which binds
`b` before `a`. This order is preserved when singling `m`, but *not* when
promoting `m`. This is because the `C` class is promoted as follows:

  class PC (b :: Type) where
    type M (x :: a) (y :: b) :: a

Due to the way GHC kind-checks associated type families, the kind of `M` is
`forall a b. a -> b -> a`, which binds `b` *after* `a`. Moreover, the
`StandaloneKindSignatures` extension does not provide a way to explicitly
declare the full kind of an associated type family, so this limitation is
not easy to work around.

The defunctionalization symbols for `M` will also follow a similar
order of type variables:

  type MSym0 :: forall a b. a ~> b ~> a
  type MSym1 :: forall a b. a -> b ~> a

In the past, we have considered different ways to rectify this, but none of
the approaches that we have tried are quite satisfactory:

* We could hackily specify the order of kind variables using a type synonym
  like `FlipConst`:

    type FlipConst x y = y
    class PC (b :: Type) where
      type M (x :: FlipConst '(b, a) a) (y :: b) :: a

  Using `FlipConst` would cause `b` to be mentioned before `a`, which would give
  `M` the kind `forall b a. FlipConst '(b, a) a -> b -> a`. While the order of
  type variables would be preserved, the downside is that the ugly `FlipConst`
  type synonym leaks into the kind. I'm not particularly fond of this, so I have
  decided not to use this hack unless someone specifically requests it.

* We could specify the order of kind variables using the TypeAbstractions
  language extension:

    class PC (b :: Type) where
      type M @(b :: Type) @a (x :: a) (y :: b) :: a

  This is much nicer to look at than the `FlipConst` hack above. However, this
  approach has its own drawbacks. For one thing, GHC only permits using
  TypeAbstractions in an associated type family declaration if its parent class
  also has a standalone kind signature. As such, this trick would only work some
  of the time.

  Even if we /did/ give the parent class a standalone kind signature, however,
  it is still not guaranteed that the promoted method would kind-check. Consider
  what would happen if you promoted this class:

    type Traversable :: (Type -> Type) -> Constraint
    class (Functor t, Foldable t) => Traversable t where
      traverse :: Applicative f => (a -> f b) -> t a -> t (f b)

  This would be promoted to:

    type PTraversable :: (Type -> Type) -> Constraint
    class PTraversable t where
      type PTraverse @(t :: Type -> Type) @f @a @b
                     (x :: a ~> f b) (y :: t a) :: t (f b)

  There is a subtle problem with this definition: because the `@f` binder lacks
  an explicit kind signature, GHC defaults its kind to `Type`. This is very bad,
  however, because `f`'s kind must be `Type -> Type`, not `Type`! Nor would it
  be straightforward to generate `@(f :: Type -> Type)`, as nothing in the
  original definition of `traverse` explicitly indicates that `f` has the kind
  `Type -> Type`.

  In theory, we could implement kind inference inside of Template Haskell to
  infer that `f :: Type -> Type`, but this is a tall order. Best to keep things
  simple and not do this.

Note [Propagating kind information from class standalone kind signatures]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider what happens when you promote this example:

  type Alternative :: (Type -> Type) -> Constraint
  class Applicative f => Alternative f where
    empty :: f a
    ...

We want the promoted `Empty` type family, as well as the `EmptySym0`
defunctionalization symbol, to have the kind
`forall (f :: Type -> Type) a. f a`. Giving `Empty` the appropriate kind is
easy enough, as we can simply copy over `Alternative`'s standalone kind
signature to `PAltenative`, its promoted counterpart:

  type PAlternative :: (Type -> Type) -> Constraint
  class PAlternative f where
    type Empty :: f a
    ...

Giving `EmptySym0` the appropriate kind is trickier, however. A naïve approach
would be to generate this:

  type EmptySym0 :: f a
  type family EmptySym0 where
    EmptySym0 = Empty

This would give EmptySym0 a more general kind than what we want, however, as
GHC will generalize this to:

  EmptySym0 :: forall {k} (f :: k -> Type) (a :: k). f a

This is undesirable, as now `EmptySym0` can be called on kinds that cannot have
`PAlternative` instances. What's more, if GHC proposal #425 were fully
implemented (see
https://github.com/ghc-proposals/ghc-proposals/blob/8443acc903437cef1a7fbb56de79b6dce77b1a09/proposals/0425-decl-invis-binders.rst#proposed-change-specification-instances),
then this code would simply not kind-check, as the left-hand side of the
`EmptySym0 = Empty` would be too general for its right-hand side.

Instead, we strive to generate this code for `EmptySym0` instead:

  type EmptySym0 :: forall (f :: Type -> Type) a. f a
  type family EmptySym0 where
    EmptySym0 = Empty

This is very doable because the user gave `Alternative` a standalone kind
signature, so it should be possible to match up the `Type -> Type` part of the
standalone kind signature with `f`. And that is exactly what we do:

* In `promoteClassDec`, we use the `dMatchUpSAKWithDecl` function to take the
  original class type variable binders and the class standalone kind signature
  as input and produce a new set of class binders as output, where the new
  binders have been annotated with kinds taken from the standalone kind
  signature. We will call these new class type variable binders the /full/
  binders.

* When generating a defunctionalization symbol for a promoted class method, we
  always quantify the defunctionalization symbol's kind using an explicit
  `forall`, where the `forall` looks like:

    forall <full class type variable binders> <method type variable binders>. ...

  This ensures that the kind information from the full class binders is
  propagated through to the defunctionalization symbol. (Note that we do not
  make any guarantees about the /order/ of these type variables, however. See
  Note [Promoted class methods and kind variable ordering].)

If the parent class lacks a standalone kind signature, then we skip all of this
and simply quantify the the defunctionalization symbols' kind variables in a
left-to-right order. Again, the order of these kind variables in unspecified, so
we are free to choose a simpler implementation that makes our lives easier.
-}

-- returns (unpromoted method name, ALetDecRHS) pairs
promoteInstanceDec :: OMap Name DType
                      -- Class method type signatures
                   -> Map Name [DTyVarBndrVis]
                      -- Class header type variable (e.g., if `class C a b` is
                      -- quoted, then this will have an entry for {C |-> [a, b]})
                   -> UInstDecl -> PrM AInstDecl
promoteInstanceDec :: OMap Name DType
-> Map Name [DTyVarBndrVis] -> UInstDecl -> PrM AInstDecl
promoteInstanceDec OMap Name DType
orig_meth_sigs Map Name [DTyVarBndrVis]
cls_tvbs_map
                   decl :: UInstDecl
decl@(InstDecl { id_name :: forall (ann :: AnnotationFlag). InstDecl ann -> Name
id_name     = Name
cls_name
                                  , id_arg_tys :: forall (ann :: AnnotationFlag). InstDecl ann -> DCxt
id_arg_tys  = DCxt
inst_tys
                                  , id_sigs :: forall (ann :: AnnotationFlag). InstDecl ann -> OMap Name DType
id_sigs     = OMap Name DType
inst_sigs
                                  , id_meths :: forall (ann :: AnnotationFlag).
InstDecl ann -> [(Name, LetDecRHS ann)]
id_meths    = [(Name, LetDecRHS Unannotated)]
meths }) = do
  opts <- PrM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  cls_tvbs <- lookup_cls_tvbs
  inst_kis <- mapM promoteType inst_tys
  let pClsName      = Options -> Name -> Name
promotedClassName Options
opts Name
cls_name
      cls_tvb_names = (DTyVarBndrVis -> Name) -> [DTyVarBndrVis] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndrVis -> Name
forall flag. DTyVarBndr flag -> Name
extractTvbName [DTyVarBndrVis]
cls_tvbs
      subst         = [LetBind] -> Map Name DType
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([LetBind] -> Map Name DType) -> [LetBind] -> Map Name DType
forall a b. (a -> b) -> a -> b
$ [Name] -> DCxt -> [LetBind]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
cls_tvb_names DCxt
inst_kis
      meth_impl     = OMap Name DType -> Map Name DType -> MethodSort
InstanceMethods OMap Name DType
inst_sigs Map Name DType
subst
      inst_ki_kvbs  = Specificity -> [DTyVarBndr ()] -> [DTyVarBndr Specificity]
forall newFlag oldFlag.
newFlag -> [DTyVarBndr oldFlag] -> [DTyVarBndr newFlag]
changeDTVFlags Specificity
SpecifiedSpec ([DTyVarBndr ()] -> [DTyVarBndr Specificity])
-> [DTyVarBndr ()] -> [DTyVarBndr Specificity]
forall a b. (a -> b) -> a -> b
$ DCxt -> [DTyVarBndr ()]
toposortTyVarsOf DCxt
inst_kis
  (meths', ann_rhss, _)
    <- mapAndUnzip3M (promoteMethod meth_impl orig_meth_sigs inst_ki_kvbs) meths
  emitDecs [DInstanceD Nothing Nothing [] (foldType (DConT pClsName)
                                            inst_kis) meths']
  return (decl { id_meths = zip (map fst meths) ann_rhss })
  where
    lookup_cls_tvbs :: PrM [DTyVarBndrVis]
    lookup_cls_tvbs :: PrM [DTyVarBndrVis]
lookup_cls_tvbs =
      -- First, try consulting the map of class names to their type variables.
      -- It is important to do this first to ensure that we consider locally
      -- declared classes before imported ones. See #410 for what happens if
      -- you don't.
      case Name -> Map Name [DTyVarBndrVis] -> Maybe [DTyVarBndrVis]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
cls_name Map Name [DTyVarBndrVis]
cls_tvbs_map of
        Just [DTyVarBndrVis]
tvbs -> [DTyVarBndrVis] -> PrM [DTyVarBndrVis]
forall a. a -> PrM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [DTyVarBndrVis]
tvbs
        Maybe [DTyVarBndrVis]
Nothing   -> PrM [DTyVarBndrVis]
reify_cls_tvbs
          -- If the class isn't present in this map, we try reifying the class
          -- as a last resort.

    reify_cls_tvbs :: PrM [DTyVarBndrVis]
    reify_cls_tvbs :: PrM [DTyVarBndrVis]
reify_cls_tvbs = do
      opts <- PrM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
      let pClsName = Options -> Name -> Name
promotedClassName Options
opts Name
cls_name
          mk_tvbs  = PrM (Maybe DInfo) -> MaybeT PrM [DTyVarBndrVis]
extract_tvbs (Name -> PrM (Maybe DInfo)
forall (q :: * -> *). DsMonad q => Name -> q (Maybe DInfo)
dsReifyTypeNameInfo Name
pClsName)
                 MaybeT PrM [DTyVarBndrVis]
-> MaybeT PrM [DTyVarBndrVis] -> MaybeT PrM [DTyVarBndrVis]
forall a. MaybeT PrM a -> MaybeT PrM a -> MaybeT PrM a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> PrM (Maybe DInfo) -> MaybeT PrM [DTyVarBndrVis]
extract_tvbs (Name -> PrM (Maybe DInfo)
forall (q :: * -> *). DsMonad q => Name -> q (Maybe DInfo)
dsReifyTypeNameInfo Name
cls_name)
                      -- See Note [Using dsReifyTypeNameInfo when promoting instances]
      mb_tvbs <- runMaybeT mk_tvbs
      case mb_tvbs of
        Just [DTyVarBndrVis]
tvbs -> [DTyVarBndrVis] -> PrM [DTyVarBndrVis]
forall a. a -> PrM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [DTyVarBndrVis]
tvbs
        Maybe [DTyVarBndrVis]
Nothing -> String -> PrM [DTyVarBndrVis]
forall a. String -> PrM a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> PrM [DTyVarBndrVis]) -> String -> PrM [DTyVarBndrVis]
forall a b. (a -> b) -> a -> b
$ String
"Cannot find class declaration annotation for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
cls_name

    extract_tvbs :: PrM (Maybe DInfo) -> MaybeT PrM [DTyVarBndrVis]
    extract_tvbs :: PrM (Maybe DInfo) -> MaybeT PrM [DTyVarBndrVis]
extract_tvbs PrM (Maybe DInfo)
reify_info = do
      mb_info <- PrM (Maybe DInfo) -> MaybeT PrM (Maybe DInfo)
forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift PrM (Maybe DInfo)
reify_info
      case mb_info of
        Just (DTyConI (DClassD DCxt
_ Name
_ [DTyVarBndrVis]
tvbs [FunDep]
_ [DDec]
_) Maybe [DDec]
_) -> [DTyVarBndrVis] -> MaybeT PrM [DTyVarBndrVis]
forall a. a -> MaybeT PrM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [DTyVarBndrVis]
tvbs
        Maybe DInfo
_                                       -> MaybeT PrM [DTyVarBndrVis]
forall a. MaybeT PrM a
forall (f :: * -> *) a. Alternative f => f a
empty

{-
Note [Using dsReifyTypeNameInfo when promoting instances]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
During the promotion of a class instance, it becomes necessary to reify the
original promoted class's info to learn various things. It's tempting to think
that just calling dsReify on the class name will be sufficient, but it's not.
Consider this class and its promotion:

  class Eq a where
    (==) :: a -> a -> Bool

  class PEq a where
    type (==) (x :: a) (y :: a) :: Bool

Notice how both of these classes have an identifier named (==), one at the
value level, and one at the type level. Now imagine what happens when you
attempt to promote this Template Haskell declaration:

   [d| f :: Bool
       f = () == () |]

When promoting ==, singletons-th will come up with its promoted equivalent (which also
happens to be ==). However, this promoted name is a raw Name, since it is created
with mkName. This becomes an issue when we call dsReify the raw "==" Name, as
Template Haskell has to arbitrarily choose between reifying the info for the
value-level (==) and the type-level (==), and in this case, it happens to pick the
value-level (==) info. We want the type-level (==) info, however, because we care
about the promoted version of (==).

Fortunately, there's a serviceable workaround. Instead of dsReify, we can use
dsReifyTypeNameInfo, which first calls lookupTypeName (to ensure we can find a Name
that's in the type namespace) and _then_ reifies it.
-}

-- Which sort of class methods are being promoted?
data MethodSort
    -- The method defaults in class declarations.
  = DefaultMethods
    -- The methods in instance declarations.
  | InstanceMethods (OMap Name DType) -- ^ InstanceSigs
                    (Map Name DKind)  -- ^ Instantiations for class tyvars
                                      --   See Note [Promoted class method kinds]
  deriving Int -> MethodSort -> String -> String
[MethodSort] -> String -> String
MethodSort -> String
(Int -> MethodSort -> String -> String)
-> (MethodSort -> String)
-> ([MethodSort] -> String -> String)
-> Show MethodSort
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> MethodSort -> String -> String
showsPrec :: Int -> MethodSort -> String -> String
$cshow :: MethodSort -> String
show :: MethodSort -> String
$cshowList :: [MethodSort] -> String -> String
showList :: [MethodSort] -> String -> String
Show

promoteMethod :: MethodSort
              -> OMap Name DType    -- method types
              -> [DTyVarBndrSpec]   -- The type variables bound by the class
                                    -- header (e.g., the @a b@ in
                                    -- @class C a b where ...@).
              -> (Name, ULetDecRHS)
              -> PrM (DDec, ALetDecRHS, LetDecProm)
                 -- returns (type instance, ALetDecRHS, promoted RHS)
promoteMethod :: MethodSort
-> OMap Name DType
-> [DTyVarBndr Specificity]
-> (Name, LetDecRHS Unannotated)
-> PrM (DDec, ALetDecRHS, LetDecProm)
promoteMethod MethodSort
meth_sort OMap Name DType
orig_sigs_map [DTyVarBndr Specificity]
cls_tvbs (Name
meth_name, LetDecRHS Unannotated
meth_rhs) = do
  opts <- PrM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  (meth_scoped_tvs, meth_tvbs, meth_arg_kis, meth_res_ki) <- promote_meth_ty
  -- If ScopedTypeVariables is enabled, bring type variables into scope over the
  -- RHS. These type variables can come from the class/instance header, the
  -- method type signature/instance signature, or both, depending on how the
  -- class or instance declaration is written. See
  -- Note [Scoped type variables and class methods] in D.S.TH.Promote.Monad.
  -- See also (Wrinkle: Partial scoping) from that Note for a scenario in which
  -- we bring class/instance header type variables into scope but /not/
  -- type variables from the class method/instance signature.
  scoped_tvs_ext <- qIsExtEnabled LangExt.ScopedTypeVariables
  let all_meth_scoped_tvs
        | Bool
scoped_tvs_ext
        = [LocalVar] -> OSet LocalVar
forall a. Ord a => [a] -> OSet a
OSet.fromList ((DTyVarBndr Specificity -> LocalVar)
-> [DTyVarBndr Specificity] -> [LocalVar]
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndr Specificity -> LocalVar
forall flag. DTyVarBndr flag -> LocalVar
tvbToLocalVar [DTyVarBndr Specificity]
cls_tvbs) OSet LocalVar -> OSet LocalVar -> OSet LocalVar
forall a. Ord a => OSet a -> OSet a -> OSet a
`OSet.union` OSet LocalVar
meth_scoped_tvs
        | Bool
otherwise
        = OSet LocalVar
forall a. OSet a
OSet.empty
  meth_arg_tvs <- replicateM (length meth_arg_kis) (qNewName "a")
  let proName = Options -> Name -> Name
promotedTopLevelValueName Options
opts Name
meth_name
      -- The name of the "helper" type family which defines the promoted version
      -- of a class method default or instance method. If the method's name is
      -- alphanumeric, we reuse the method's name for the helper type family's
      -- name. Otherwise, we use the name "TFHelper". (Note that
      -- promoteLetDecRHS expects a value-level name, so we pass it "tFHelper",
      -- which later gets promoted to TFHelper.)
      helperNameBase = case Name -> String
nameBase Name
proName of
                         Char
first:String
_ | Bool -> Bool
not (Char -> Bool
isHsLetter Char
first) -> String
"tFHelper"
                         String
alpha                            -> String
alpha

      -- family_args are the type variables in a promoted class's
      -- associated type family instance (or default implementation), e.g.,
      --
      --   class C k where
      --     type T (a :: k) (b :: Bool)
      --     type T a b = THelper1 a b        -- family_args = [a, b]
      --
      --   instance C Bool where
      --     type T a b = THelper2 a b        -- family_args = [a, b]
      --
      -- We could annotate these variables with explicit kinds, but it's not
      -- strictly necessary, as kind inference can figure them out just as well.
      family_args = (Name -> DType) -> [Name] -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map Name -> DType
DVarT [Name]
meth_arg_tvs
  helperName <- newUniqueName helperNameBase
  let proHelperName = Options -> Name -> Maybe Uniq -> Name
promotedValueName Options
opts Name
helperName Maybe Uniq
forall a. Maybe a
Nothing
      -- If a promoted method's kind lacks an outermost `forall`, then we need
      -- to compute the list of kind variable binders manually. The order of
      -- these binders doesn't matter, as the user will never invoke a helper
      -- type family directly, so we simply quantify the binders in
      -- left-to-right order.
      full_meth_tvbs
        | [DTyVarBndr Specificity] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [DTyVarBndr Specificity]
meth_tvbs
        = Specificity -> [DTyVarBndr ()] -> [DTyVarBndr Specificity]
forall newFlag oldFlag.
newFlag -> [DTyVarBndr oldFlag] -> [DTyVarBndr newFlag]
changeDTVFlags Specificity
SpecifiedSpec ([DTyVarBndr ()] -> [DTyVarBndr Specificity])
-> [DTyVarBndr ()] -> [DTyVarBndr Specificity]
forall a b. (a -> b) -> a -> b
$
          DCxt -> [DTyVarBndr ()]
toposortTyVarsOf (DCxt
meth_arg_kis DCxt -> DCxt -> DCxt
forall a. [a] -> [a] -> [a]
++ [DType
meth_res_ki])
        | Bool
otherwise
        = [DTyVarBndr Specificity]
meth_tvbs
      -- Make sure not to re-quantify any kind variable binders that are already
      -- bound by the class or instance head.
      full_meth_tvbs_without_cls_tvbs =
        (DTyVarBndr Specificity -> DTyVarBndr Specificity -> Bool)
-> [DTyVarBndr Specificity]
-> [DTyVarBndr Specificity]
-> [DTyVarBndr Specificity]
forall a. (a -> a -> Bool) -> [a] -> [a] -> [a]
deleteFirstsBy (Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Name -> Name -> Bool)
-> (DTyVarBndr Specificity -> Name)
-> DTyVarBndr Specificity
-> DTyVarBndr Specificity
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` DTyVarBndr Specificity -> Name
forall flag. DTyVarBndr flag -> Name
extractTvbName) [DTyVarBndr Specificity]
full_meth_tvbs [DTyVarBndr Specificity]
cls_tvbs
      -- All of the kind variable binders, including both (1) those bound by the
      -- class or instance head, and (2) those bound by the promoted method's
      -- kind. This will be used in an outermost `forall` in the helper type
      -- family's standalone kind signature to specify the kinds of kind
      -- variables (when possible).
      all_meth_tvbs = [DTyVarBndr Specificity]
cls_tvbs [DTyVarBndr Specificity]
-> [DTyVarBndr Specificity] -> [DTyVarBndr Specificity]
forall a. [a] -> [a] -> [a]
++ [DTyVarBndr Specificity]
full_meth_tvbs_without_cls_tvbs

  -- Promote the right-hand side of the helper. Note that we never partially
  -- apply the helper type family, and users will never invoke the helper
  -- directly. As such, there is no need to emit defunctionalization symbols for
  -- the helper type family.
  (pro_decs, _defun_decs, ann_rhs)
    <- promoteLetDecRHS (ClassMethodRHS all_meth_scoped_tvs all_meth_tvbs meth_arg_kis meth_res_ki)
                        OMap.empty OMap.empty
                        Nothing helperName meth_rhs
  emitDecs pro_decs
  return ( DTySynInstD
             (DTySynEqn Nothing
                        (foldType (DConT proName) family_args)
                        (foldType (DConT proHelperName) family_args))
         , ann_rhs
         , (proHelperName, []) )
  where
    -- Promote the type of a class method. For a default method, "the type" is
    -- simply the type of the original method. For an instance method,
    -- "the type" is like the type of the original method, but substituted for
    -- the types in the instance head. (e.g., if you have `class C a` and
    -- `instance C T`, then the substitution [a |-> T] must be applied to the
    -- original method's type.)
    --
    -- This returns four things in a tuple:
    --
    -- 1. The set of scoped type variables from the class method signature or
    --    instance signature. If an instance method lacks an instance signature,
    --    this will be an empty set. These type variables will be brought into
    --    scope over the RHS of the method: see Note [Scoped type variables and
    --    class methods] in D.S.TH.Promote.Monad.
    --
    -- 2. The list of kind variable binders that are explicitly quantified by an
    --    outermost `forall` in the promoted type. If there is no such outermost
    --    `forall`, then this will be the empty list.
    --
    -- 3. The promoted argument kinds.
    --
    -- 4. The promoted result kind.
    --
    -- Note that:
    --
    -- * Ultimately, this information is used to compute a standalone kind
    --   signature for a "helper" type family which defines the promoted version
    --   of a class method default or instance method. Because users never
    --   invoke helper type families directly, it is not important to get the
    --   order of kind variables exactly right. As such, the list of kind
    --   variable binders can be in an unspecified order.
    --
    -- * The kind variable binders only include kind variables that are
    --   quantified by the /method/, not by the class or instance head. The
    --   variables bound by the class or instance head are added separately
    --   (see `all_meth_tvbs` above).
    --
    -- * The set of scoped type variable names will always be a subset of the
    --   names in the list of kind variable binders. We are using the kind
    --   variable binders primarily as a way to annotate the kinds of each
    --   variable, so it is possible for the helper type family to bind a kind
    --   variable in a `forall` without it scoping over the body.
    promote_meth_ty :: PrM (OSet LocalVar, [DTyVarBndrSpec], [DKind], DKind)
    promote_meth_ty :: PrM (OSet LocalVar, [DTyVarBndr Specificity], DCxt, DType)
promote_meth_ty =
      case MethodSort
meth_sort of
        MethodSort
DefaultMethods ->
          -- No substitution for class variables is required for default
          -- method type signatures, as they share type variables with the
          -- class they inhabit.
          PrM (OSet LocalVar, [DTyVarBndr Specificity], DCxt, DType)
lookup_meth_ty
        InstanceMethods OMap Name DType
inst_sigs_map Map Name DType
cls_subst ->
          case Name -> OMap Name DType -> Maybe DType
forall k v. Ord k => k -> OMap k v -> Maybe v
OMap.lookup Name
meth_name OMap Name DType
inst_sigs_map of
            Just DType
ty -> do
              -- We have an InstanceSig. These are easy: we can just use the
              -- instance signature's type directly, and no substitution for
              -- class variables is required.
              (kvbs, arg_kis, res_ki) <- DType -> PrM ([DTyVarBndr Specificity], DCxt, DType)
forall (m :: * -> *).
OptionsMonad m =>
DType -> m ([DTyVarBndr Specificity], DCxt, DType)
promoteUnraveled DType
ty
              pure (OSet.fromList (map tvbToLocalVar kvbs), kvbs, arg_kis, res_ki)
            Maybe DType
Nothing -> do
              -- We don't have an InstanceSig, so we must compute the kind to use
              -- ourselves.
              (_, kvbs, arg_kis, res_ki) <- PrM (OSet LocalVar, [DTyVarBndr Specificity], DCxt, DType)
lookup_meth_ty
              -- Substitute for the class variables in the method's type.
              -- See Note [Promoted class method kinds]
              let kvbs'    = (DType -> DType)
-> DTyVarBndr Specificity -> DTyVarBndr Specificity
forall flag. (DType -> DType) -> DTyVarBndr flag -> DTyVarBndr flag
mapDTVKind (Map Name DType -> DType -> DType
SC.substTy Map Name DType
cls_subst) (DTyVarBndr Specificity -> DTyVarBndr Specificity)
-> [DTyVarBndr Specificity] -> [DTyVarBndr Specificity]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DTyVarBndr Specificity]
kvbs
                  arg_kis' = (DType -> DType) -> DCxt -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map (Map Name DType -> DType -> DType
SC.substTy Map Name DType
cls_subst) DCxt
arg_kis
                  res_ki'  = Map Name DType -> DType -> DType
SC.substTy Map Name DType
cls_subst DType
res_ki
              -- If there is no instance signature, then there are no additional
              -- type variables to bring into scope, so return an empty set of
              -- scoped type variables. We will reuse the list of kind variable
              -- binders in case they have useful kind information.
              pure (OSet.empty, kvbs', arg_kis', res_ki')

    -- Attempt to look up a class method's original type.
    lookup_meth_ty :: PrM (OSet LocalVar, [DTyVarBndrSpec], [DKind], DKind)
    lookup_meth_ty :: PrM (OSet LocalVar, [DTyVarBndr Specificity], DCxt, DType)
lookup_meth_ty = do
      opts <- PrM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
      let proName = Options -> Name -> Name
promotedTopLevelValueName Options
opts Name
meth_name
      case OMap.lookup meth_name orig_sigs_map of
        Just DType
ty -> do
          -- The type of the method is in scope, so promote that.
          (kvbs, arg_kis, res_ki) <- DType -> PrM ([DTyVarBndr Specificity], DCxt, DType)
forall (m :: * -> *).
OptionsMonad m =>
DType -> m ([DTyVarBndr Specificity], DCxt, DType)
promoteUnraveled DType
ty
          pure (OSet.fromList (map tvbToLocalVar kvbs), kvbs, arg_kis, res_ki)
        Maybe DType
Nothing -> do
          -- If the type of the method is not in scope, the only other option
          -- is to try reifying the promoted method name.
          mb_info <- Name -> PrM (Maybe DInfo)
forall (q :: * -> *). DsMonad q => Name -> q (Maybe DInfo)
dsReifyTypeNameInfo Name
proName
                     -- See Note [Using dsReifyTypeNameInfo when promoting instances]
          case mb_info of
            Just (DTyConI (DOpenTypeFamilyD (DTypeFamilyHead Name
_ [DTyVarBndrVis]
tvbs DFamilyResultSig
mb_res_ki Maybe InjectivityAnn
_)) Maybe [DDec]
_)
              -> let arg_kis :: DCxt
arg_kis = (DTyVarBndrVis -> DType) -> [DTyVarBndrVis] -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map (Maybe DType -> DType
defaultMaybeToTypeKind (Maybe DType -> DType)
-> (DTyVarBndrVis -> Maybe DType) -> DTyVarBndrVis -> DType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DTyVarBndrVis -> Maybe DType
forall flag. DTyVarBndr flag -> Maybe DType
extractTvbKind) [DTyVarBndrVis]
tvbs
                     res_ki :: DType
res_ki  = Maybe DType -> DType
defaultMaybeToTypeKind (DFamilyResultSig -> Maybe DType
resultSigToMaybeKind DFamilyResultSig
mb_res_ki)
                  -- If there is no instance signature, then there are no
                  -- additional type variables to bring into scope, so return an
                  -- empty set of scoped type variables. Moreover, we do not
                  -- have a list of kind variable binders readily available, so
                  -- we return an empty list. This is OK, as we will compute
                  -- the kind variable binders for the helper type family
                  -- elsewhere (see `full_meth_tvbs` above).
                  in (OSet LocalVar, [DTyVarBndr Specificity], DCxt, DType)
-> PrM (OSet LocalVar, [DTyVarBndr Specificity], DCxt, DType)
forall a. a -> PrM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (OSet LocalVar
forall a. OSet a
OSet.empty, [], DCxt
arg_kis, DType
res_ki)
            Maybe DInfo
_ -> String
-> PrM (OSet LocalVar, [DTyVarBndr Specificity], DCxt, DType)
forall a. String -> PrM a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
 -> PrM (OSet LocalVar, [DTyVarBndr Specificity], DCxt, DType))
-> String
-> PrM (OSet LocalVar, [DTyVarBndr Specificity], DCxt, DType)
forall a b. (a -> b) -> a -> b
$ String
"Cannot find type annotation for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
proName

{-
Note [Promoted class method kinds]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this example of a type class (and instance):

  class C a where
    m :: a -> Bool -> Bool
    m _ x = x

  instance C [a] where
    m l _ = null l

The promoted version of these declarations would be:

  class PC a where
    type M (x :: a) (y :: Bool) :: Bool
    type M x y = MHelper1 x y

  instance PC [a] where
    type M x y = MHelper2 x y

  type MHelper1 :: a -> Bool -> Bool
  type family MHelper1 x y where ...

  type MHelper2 :: [a] -> Bool -> Bool
  type family MHelper2 x y where ...

Getting the kind signature for MHelper1 (the promoted default implementation of
M) is quite simple, as it corresponds exactly to the kind of M. We might even
choose to make that the kind of MHelper2, but then it would be overly general
(and more difficult to find in -ddump-splices output). For this reason, we
substitute in the kinds of the instance itself to determine the kinds of
promoted method implementations like MHelper2.
-}

promoteLetDecEnv :: Maybe Uniq -> ULetDecEnv -> PrM ([DDec], ALetDecEnv)
promoteLetDecEnv :: Maybe Uniq -> LetDecEnv Unannotated -> PrM ([DDec], ALetDecEnv)
promoteLetDecEnv Maybe Uniq
mb_let_uniq (LetDecEnv { lde_defns :: forall (ann :: AnnotationFlag).
LetDecEnv ann -> OMap Name (LetDecRHS ann)
lde_defns = OMap Name (LetDecRHS Unannotated)
value_env
                                        , lde_types :: forall (ann :: AnnotationFlag). LetDecEnv ann -> OMap Name DType
lde_types = OMap Name DType
type_env
                                        , lde_infix :: forall (ann :: AnnotationFlag).
LetDecEnv ann -> OMap Name (Fixity, NamespaceSpecifier)
lde_infix = OMap Name (Fixity, NamespaceSpecifier)
fix_env }) = do
  infix_decls <- ((Name, (Fixity, NamespaceSpecifier)) -> PrM (Maybe DDec))
-> [(Name, (Fixity, NamespaceSpecifier))] -> PrM [DDec]
forall (m :: * -> *) a b.
Monad m =>
(a -> m (Maybe b)) -> [a] -> m [b]
mapMaybeM (\(Name
n, (Fixity
f, NamespaceSpecifier
ns)) -> Maybe Uniq
-> Name -> Fixity -> NamespaceSpecifier -> PrM (Maybe DDec)
forall (q :: * -> *).
OptionsMonad q =>
Maybe Uniq
-> Name -> Fixity -> NamespaceSpecifier -> q (Maybe DDec)
promoteInfixDecl Maybe Uniq
mb_let_uniq Name
n Fixity
f NamespaceSpecifier
ns) ([(Name, (Fixity, NamespaceSpecifier))] -> PrM [DDec])
-> [(Name, (Fixity, NamespaceSpecifier))] -> PrM [DDec]
forall a b. (a -> b) -> a -> b
$
                 OMap Name (Fixity, NamespaceSpecifier)
-> [(Name, (Fixity, NamespaceSpecifier))]
forall k v. OMap k v -> [(k, v)]
OMap.assocs OMap Name (Fixity, NamespaceSpecifier)
fix_env

    -- promote all the declarations, producing annotated declarations
  let (names, rhss) = unzip $ OMap.assocs value_env
  (pro_decs, defun_decss, ann_rhss)
    <- fmap unzip3 $
       zipWithM (promoteLetDecRHS LetBindingRHS type_env (fmap fst fix_env) mb_let_uniq)
                names rhss

  emitDecs $ concat defun_decss
  let decs = [[DDec]] -> [DDec]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[DDec]]
pro_decs [DDec] -> [DDec] -> [DDec]
forall a. [a] -> [a] -> [a]
++ [DDec]
infix_decls

    -- build the ALetDecEnv
  let let_dec_env' = LetDecEnv { lde_defns :: OMap Name ALetDecRHS
lde_defns     = [(Name, ALetDecRHS)] -> OMap Name ALetDecRHS
forall k v. Ord k => [(k, v)] -> OMap k v
OMap.fromList ([(Name, ALetDecRHS)] -> OMap Name ALetDecRHS)
-> [(Name, ALetDecRHS)] -> OMap Name ALetDecRHS
forall a b. (a -> b) -> a -> b
$ [Name] -> [ALetDecRHS] -> [(Name, ALetDecRHS)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
names [ALetDecRHS]
ann_rhss
                               , lde_types :: OMap Name DType
lde_types     = OMap Name DType
type_env
                               , lde_infix :: OMap Name (Fixity, NamespaceSpecifier)
lde_infix     = OMap Name (Fixity, NamespaceSpecifier)
fix_env
                               , lde_proms :: IfAnn Annotated (OMap Name LetDecProm) ()
lde_proms     = OMap Name LetDecProm
IfAnn Annotated (OMap Name LetDecProm) ()
forall k v. OMap k v
OMap.empty  -- filled in promoteLetDecs
                               }

  return (decs, let_dec_env')

-- Promote a fixity declaration.
promoteInfixDecl :: forall q. OptionsMonad q
                 => Maybe Uniq -> Name -> Fixity
                 -> NamespaceSpecifier
                    -- The namespace specifier for the fixity declaration. We
                    -- only pass this for the sake of checking if we need to
                    -- avoid promoting a fixity declaration (see `promote_val`
                    -- below). The actual namespace used in the promoted fixity
                    -- declaration will always be `type`.
                 -> q (Maybe DDec)
promoteInfixDecl :: forall (q :: * -> *).
OptionsMonad q =>
Maybe Uniq
-> Name -> Fixity -> NamespaceSpecifier -> q (Maybe DDec)
promoteInfixDecl Maybe Uniq
mb_let_uniq Name
name Fixity
fixity NamespaceSpecifier
ns = do
  opts <- q Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  fld_sels <- qIsExtEnabled LangExt.FieldSelectors
  mb_ns <- reifyNameSpace name
  case mb_ns of
    -- If we can't find the Name for some odd reason, fall back to promote_val
    Maybe NameSpace
Nothing          -> q (Maybe DDec)
promote_val
    Just NameSpace
VarName     -> q (Maybe DDec)
promote_val
    Just (FldName String
_)
      | Bool
fld_sels     -> q (Maybe DDec)
promote_val
      | Bool
otherwise    -> q (Maybe DDec)
never_mind
    Just NameSpace
DataName    -> q (Maybe DDec)
never_mind
    Just NameSpace
TcClsName   -> do
      mb_info <- Name -> q (Maybe DInfo)
forall (q :: * -> *). DsMonad q => Name -> q (Maybe DInfo)
dsReify Name
name
      case mb_info of
        Just (DTyConI DClassD{} Maybe [DDec]
_)
          -> Name -> q (Maybe DDec)
finish (Name -> q (Maybe DDec)) -> Name -> q (Maybe DDec)
forall a b. (a -> b) -> a -> b
$ Options -> Name -> Name
promotedClassName Options
opts Name
name
        Maybe DInfo
_ -> q (Maybe DDec)
never_mind
  where
    -- Produce the fixity declaration. Promoted names always inhabit the `type`
    -- namespace (i.e., `TypeNamespaceSpecifier`).
    finish :: Name -> q (Maybe DDec)
    finish :: Name -> q (Maybe DDec)
finish = Maybe DDec -> q (Maybe DDec)
forall a. a -> q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe DDec -> q (Maybe DDec))
-> (Name -> Maybe DDec) -> Name -> q (Maybe DDec)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DDec -> Maybe DDec
forall a. a -> Maybe a
Just (DDec -> Maybe DDec) -> (Name -> DDec) -> Name -> Maybe DDec
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DLetDec -> DDec
DLetDec (DLetDec -> DDec) -> (Name -> DLetDec) -> Name -> DDec
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fixity -> NamespaceSpecifier -> Name -> DLetDec
DInfixD Fixity
fixity NamespaceSpecifier
TypeNamespaceSpecifier

    -- Don't produce a fixity declaration at all. This can happen in the
    -- following circumstances:
    --
    -- - When promoting a fixity declaration for a name whose promoted
    --   counterpart is the same as the original name.
    --   See Note [singletons-th and fixity declarations] in
    --   D.S.TH.Single.Fixity, wrinkle 1.
    --
    -- - A fixity declaration contains the name of a record selector when
    --   NoFieldSelectors is active.
    never_mind :: q (Maybe DDec)
    never_mind :: q (Maybe DDec)
never_mind = Maybe DDec -> q (Maybe DDec)
forall a. a -> q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe DDec
forall a. Maybe a
Nothing

    -- Certain value names do not change when promoted (e.g., infix names).
    -- Therefore, don't bother promoting their fixity declarations if the
    -- following hold:
    --
    -- - 'genQuotedDecs' is set to 'True'.
    --
    -- - The name lacks an explicit namespace specifier.
    --
    -- Doing so will run the risk of generating duplicate fixity declarations.
    -- See Note [singletons-th and fixity declarations] in D.S.TH.Single.Fixity, wrinkle 1.
    promote_val :: q (Maybe DDec)
    promote_val :: q (Maybe DDec)
promote_val = do
      opts <- q Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
      let promoted_name :: Name
          promoted_name = Options -> Name -> Maybe Uniq -> Name
promotedValueName Options
opts Name
name Maybe Uniq
mb_let_uniq
      if nameBase name == nameBase promoted_name
         && genQuotedDecs opts
         && ns == NoNamespaceSpecifier
         then never_mind
         else finish promoted_name

-- Try producing promoted fixity declarations for Names by reifying them
-- /without/ consulting quoted declarations. If reification fails, recover and
-- return the empty list.
-- See [singletons-th and fixity declarations] in D.S.TH.Single.Fixity, wrinkle 2.
promoteReifiedInfixDecls :: forall q. OptionsMonad q => [Name] -> q [DDec]
promoteReifiedInfixDecls :: forall (q :: * -> *). OptionsMonad q => [Name] -> q [DDec]
promoteReifiedInfixDecls = (Name -> q (Maybe DDec)) -> [Name] -> q [DDec]
forall (m :: * -> *) a b.
Monad m =>
(a -> m (Maybe b)) -> [a] -> m [b]
mapMaybeM Name -> q (Maybe DDec)
tryPromoteFixityDeclaration
  where
    tryPromoteFixityDeclaration :: Name -> q (Maybe DDec)
    tryPromoteFixityDeclaration :: Name -> q (Maybe DDec)
tryPromoteFixityDeclaration Name
name =
      q (Maybe DDec) -> q (Maybe DDec) -> q (Maybe DDec)
forall a. q a -> q a -> q a
forall (m :: * -> *) a. Quasi m => m a -> m a -> m a
qRecover (Maybe DDec -> q (Maybe DDec)
forall a. a -> q a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe DDec
forall a. Maybe a
Nothing) (q (Maybe DDec) -> q (Maybe DDec))
-> q (Maybe DDec) -> q (Maybe DDec)
forall a b. (a -> b) -> a -> b
$ do
        mFixity <- Name -> q (Maybe Fixity)
forall (m :: * -> *). Quasi m => Name -> m (Maybe Fixity)
qReifyFixity Name
name
        case mFixity of
          Maybe Fixity
Nothing     -> Maybe DDec -> q (Maybe DDec)
forall a. a -> q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe DDec
forall a. Maybe a
Nothing
          -- NB: We don't have a NamespaceSpecifier in hand here. We could try
          -- to look one up, but it doesn't actually matter which namespace we
          -- pass here. If we reach this point in the code, we know we have a
          -- non-quoted Name (as reification would failed earlier if the Name
          -- were quoted). As such, the special case described in
          -- [singletons-th and fixity declarations] in D.S.TH.Single.Fixity,
          -- wrinkle 1 won't apply, and we only pass a namespace specifier for
          -- the sake of checking this special case.
          Just Fixity
fixity -> Maybe Uniq
-> Name -> Fixity -> NamespaceSpecifier -> q (Maybe DDec)
forall (q :: * -> *).
OptionsMonad q =>
Maybe Uniq
-> Name -> Fixity -> NamespaceSpecifier -> q (Maybe DDec)
promoteInfixDecl Maybe Uniq
forall a. Maybe a
Nothing Name
name Fixity
fixity NamespaceSpecifier
NoNamespaceSpecifier

-- Which sort of let-bound declaration's right-hand side is being promoted?
data LetDecRHSSort
    -- An ordinary (i.e., non-class-related) let-bound declaration.
  = LetBindingRHS
    -- The right-hand side of a class method (either a default method or a
    -- method in an instance declaration).
  | ClassMethodRHS
      (OSet LocalVar)
                  -- The scoped type variables to bring into scope over
                  -- the RHS of the class method. See
                  -- Note [Scoped type variables and class methods]
                  -- in D.S.TH.Promote.Monad.
      [DTyVarBndrSpec]
                  -- The RHS's kind variable binders. Note that we do not
                  -- guarantee a particular order for these binders (see
                  -- Note [Promoted class methods and kind variable ordering]),
                  -- as we are mainly using kind variable binders for the sake
                  -- of annotating variables with their kinds.
      [DKind]     -- The RHS's promoted argument kinds. Needed to fix #136.
      DKind       -- The RHS's promoted result kind. Needed to fix #136.
  deriving Int -> LetDecRHSSort -> String -> String
[LetDecRHSSort] -> String -> String
LetDecRHSSort -> String
(Int -> LetDecRHSSort -> String -> String)
-> (LetDecRHSSort -> String)
-> ([LetDecRHSSort] -> String -> String)
-> Show LetDecRHSSort
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> LetDecRHSSort -> String -> String
showsPrec :: Int -> LetDecRHSSort -> String -> String
$cshow :: LetDecRHSSort -> String
show :: LetDecRHSSort -> String
$cshowList :: [LetDecRHSSort] -> String -> String
showList :: [LetDecRHSSort] -> String -> String
Show

-- This function is used both to promote class method defaults and normal
-- let bindings. Thus, it can't quite do all the work locally and returns
-- an intermediate structure. Perhaps a better design is available.
promoteLetDecRHS :: LetDecRHSSort
                 -> OMap Name DType      -- local type env't
                 -> OMap Name Fixity     -- local fixity env't
                 -> Maybe Uniq           -- let-binding unique (if locally bound)
                 -> Name                 -- name of the thing being promoted
                 -> ULetDecRHS           -- body of the thing
                 -> PrM ( [DDec]        -- promoted type family dec, plus the
                                        -- SAK dec (if one exists)
                        , [DDec]        -- defunctionalization
                        , ALetDecRHS )  -- annotated RHS
promoteLetDecRHS :: LetDecRHSSort
-> OMap Name DType
-> OMap Name Fixity
-> Maybe Uniq
-> Name
-> LetDecRHS Unannotated
-> PrM ([DDec], [DDec], ALetDecRHS)
promoteLetDecRHS LetDecRHSSort
rhs_sort OMap Name DType
type_env OMap Name Fixity
fix_env Maybe Uniq
mb_let_uniq Name
name LetDecRHS Unannotated
let_dec_rhs = do
  all_locals <- PrM [LocalVar]
forall (m :: * -> *). MonadReader PrEnv m => m [LocalVar]
allLocals
  case let_dec_rhs of
    UValue DExp
exp -> do
      (m_ldrki, ty_num_args) <- [LocalVar] -> Int -> PrM (Maybe LetDecRHSKindInfo, Int)
promote_let_dec_ty [LocalVar]
all_locals Int
0
      if ty_num_args == 0
      then do
        prom_fun_lhs <- promoteLetDecName mb_let_uniq name m_ldrki all_locals
        promote_let_dec_rhs all_locals m_ldrki 0 (promoteExp exp)
                            (\DType
exp' -> [Maybe [DTyVarBndr ()] -> DType -> DType -> DTySynEqn
DTySynEqn Maybe [DTyVarBndr ()]
forall a. Maybe a
Nothing DType
prom_fun_lhs DType
exp'])
                            AValue
      else
        -- If we have a UValue with a function type, process it as though it
        -- were a UFunction. promote_function_rhs will take care of
        -- eta-expanding arguments as necessary.
        promote_function_rhs all_locals [DClause [] exp]
    UFunction [DClause]
clauses -> [LocalVar] -> [DClause] -> PrM ([DDec], [DDec], ALetDecRHS)
promote_function_rhs [LocalVar]
all_locals [DClause]
clauses
  where
    -- Promote the RHS of a UFunction (or a UValue with a function type).
    promote_function_rhs :: [LocalVar]
                         -> [DClause] -> PrM ([DDec], [DDec], ALetDecRHS)
    promote_function_rhs :: [LocalVar] -> [DClause] -> PrM ([DDec], [DDec], ALetDecRHS)
promote_function_rhs [LocalVar]
all_locals [DClause]
clauses = do
      numArgs <- [DClause] -> PrM Int
count_args [DClause]
clauses
      (m_ldrki, ty_num_args) <- promote_let_dec_ty all_locals numArgs
      expClauses <- mapM (etaContractOrExpand ty_num_args numArgs) clauses
      let promote_clause = Maybe Uniq
-> Name
-> Maybe LetDecRHSKindInfo
-> [LocalVar]
-> DClause
-> PrM (DTySynEqn, ADClause)
promoteClause Maybe Uniq
mb_let_uniq Name
name Maybe LetDecRHSKindInfo
m_ldrki [LocalVar]
all_locals
      promote_let_dec_rhs all_locals m_ldrki ty_num_args
                          (mapAndUnzipM promote_clause expClauses)
                          id (AFunction ty_num_args)

    -- Promote a UValue or a UFunction.
    -- Notes about type variables:
    --
    -- * For UValues, `prom_a` is DType and `a` is Exp.
    --
    -- * For UFunctions, `prom_a` is [DTySynEqn] and `a` is [DClause].
    promote_let_dec_rhs
      :: [LocalVar]               -- Local variables bound in this scope
      -> Maybe LetDecRHSKindInfo  -- Information about the promoted kind (if present)
      -> Int                      -- The number of promoted function arguments
      -> PrM (prom_a, a)          -- Promote the RHS
      -> (prom_a -> [DTySynEqn])  -- Turn the promoted RHS into type family equations
      -> (a -> ALetDecRHS)        -- Build an ALetDecRHS
      -> PrM ([DDec], [DDec], ALetDecRHS)
    promote_let_dec_rhs :: forall prom_a a.
[LocalVar]
-> Maybe LetDecRHSKindInfo
-> Int
-> PrM (prom_a, a)
-> (prom_a -> [DTySynEqn])
-> (a -> ALetDecRHS)
-> PrM ([DDec], [DDec], ALetDecRHS)
promote_let_dec_rhs [LocalVar]
all_locals Maybe LetDecRHSKindInfo
m_ldrki Int
ty_num_args
                        PrM (prom_a, a)
promote_thing prom_a -> [DTySynEqn]
mk_prom_eqns a -> ALetDecRHS
mk_alet_dec_rhs = do
      opts <- PrM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
      tyvarNames <- replicateM ty_num_args (qNewName "a")
      let proName    = Options -> Name -> Maybe Uniq -> Name
promotedValueName Options
opts Name
name Maybe Uniq
mb_let_uniq
          m_fixity   = Name -> OMap Name Fixity -> Maybe Fixity
forall k v. Ord k => k -> OMap k v -> Maybe v
OMap.lookup Name
name OMap Name Fixity
fix_env

          mk_tf_head :: [DTyVarBndrVis] -> DFamilyResultSig -> DTypeFamilyHead
          mk_tf_head [DTyVarBndrVis]
arg_tvbs DFamilyResultSig
res_sig =
            Name
-> [LocalVar]
-> [DTyVarBndrVis]
-> DFamilyResultSig
-> DTypeFamilyHead
dTypeFamilyHead_with_locals Name
proName [LocalVar]
all_locals [DTyVarBndrVis]
arg_tvbs DFamilyResultSig
res_sig

          (lde_kvs_to_bind, m_sak_dec, defun_ki, tf_head) =
              -- There are three possible cases:
            case m_ldrki of
              -- 1. We have no kind information whatsoever.
              Maybe LetDecRHSKindInfo
Nothing ->
                let arg_tvbs :: [DTyVarBndrVis]
arg_tvbs = (Name -> DTyVarBndrVis) -> [Name] -> [DTyVarBndrVis]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> BndrVis -> DTyVarBndrVis
forall flag. Name -> flag -> DTyVarBndr flag
`DPlainTV` BndrVis
BndrReq) [Name]
tyvarNames in
                ( OSet LocalVar
forall a. OSet a
OSet.empty
                , Maybe DDec
forall a. Maybe a
Nothing
                , [LocalVar] -> [DTyVarBndrVis] -> Maybe DType -> DefunKindInfo
DefunNoSAK [LocalVar]
all_locals [DTyVarBndrVis]
arg_tvbs Maybe DType
forall a. Maybe a
Nothing
                , [DTyVarBndrVis] -> DFamilyResultSig -> DTypeFamilyHead
mk_tf_head [DTyVarBndrVis]
arg_tvbs DFamilyResultSig
DNoSig
                )
              -- 2. We have some kind information in the form of a LetDecRHSKindInfo.
              Just (LDRKI Maybe DType
m_sak OSet LocalVar
lde_kvs_to_bind' [DTyVarBndr Specificity]
tvbs DCxt
argKs DType
resK) ->
                let arg_tvbs :: [DTyVarBndrVis]
arg_tvbs = (Name -> DType -> DTyVarBndrVis)
-> [Name] -> DCxt -> [DTyVarBndrVis]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Name -> BndrVis -> DType -> DTyVarBndrVis
forall flag. Name -> flag -> DType -> DTyVarBndr flag
`DKindedTV` BndrVis
BndrReq) [Name]
tyvarNames DCxt
argKs in
                case Maybe DType
m_sak of
                  -- 2(a). We do not have a standalone kind signature.
                  Maybe DType
Nothing ->
                    ( OSet LocalVar
lde_kvs_to_bind'
                    , Maybe DDec
forall a. Maybe a
Nothing
                    , [LocalVar] -> [DTyVarBndrVis] -> Maybe DType -> DefunKindInfo
DefunNoSAK [LocalVar]
all_locals [DTyVarBndrVis]
arg_tvbs (DType -> Maybe DType
forall a. a -> Maybe a
Just DType
resK)
                    , [DTyVarBndrVis] -> DFamilyResultSig -> DTypeFamilyHead
mk_tf_head [DTyVarBndrVis]
arg_tvbs (DType -> DFamilyResultSig
DKindSig DType
resK)
                    )
                  -- 2(b). We have a standalone kind signature.
                  Just DType
sak ->
                    -- Compute the type variable binders needed to give the type
                    -- family the correct arity.
                    -- See Note [Generating type families with the correct arity].
                    let tvbs' :: [DTyVarBndr Specificity]
tvbs' | [DTyVarBndr Specificity] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [DTyVarBndr Specificity]
tvbs
                              = Specificity -> [DTyVarBndr ()] -> [DTyVarBndr Specificity]
forall newFlag oldFlag.
newFlag -> [DTyVarBndr oldFlag] -> [DTyVarBndr newFlag]
changeDTVFlags Specificity
SpecifiedSpec ([DTyVarBndr ()] -> [DTyVarBndr Specificity])
-> [DTyVarBndr ()] -> [DTyVarBndr Specificity]
forall a b. (a -> b) -> a -> b
$
                                DCxt -> [DTyVarBndr ()]
toposortTyVarsOf (DCxt
argKs DCxt -> DCxt -> DCxt
forall a. [a] -> [a] -> [a]
++ [DType
resK])
                              | Bool
otherwise
                              = [DTyVarBndr Specificity]
tvbs
                        arg_tvbs' :: [DTyVarBndrVis]
arg_tvbs' = [DTyVarBndr Specificity] -> [DTyVarBndrVis]
dtvbSpecsToBndrVis [DTyVarBndr Specificity]
tvbs' [DTyVarBndrVis] -> [DTyVarBndrVis] -> [DTyVarBndrVis]
forall a. [a] -> [a] -> [a]
++ [DTyVarBndrVis]
arg_tvbs in
                    ( OSet LocalVar
lde_kvs_to_bind'
                    , DDec -> Maybe DDec
forall a. a -> Maybe a
Just (DDec -> Maybe DDec) -> DDec -> Maybe DDec
forall a b. (a -> b) -> a -> b
$ Name -> DType -> DDec
DKiSigD Name
proName DType
sak
                    , DType -> DefunKindInfo
DefunSAK DType
sak
                      -- We opt to annotate the argument and result kinds in
                      -- the body of the type family declaration even if it is
                      -- given a standalone kind signature.
                      -- See Note [Keep redundant kind information for Haddocks].
                    , [DTyVarBndrVis] -> DFamilyResultSig -> DTypeFamilyHead
mk_tf_head [DTyVarBndrVis]
arg_tvbs' (DType -> DFamilyResultSig
DKindSig DType
resK)
                    )

      defun_decs <- defunctionalize proName m_fixity defun_ki
      (prom_thing, thing) <- scopedBind lde_kvs_to_bind promote_thing
      return ( catMaybes [ m_sak_dec
                         , Just $ DClosedTypeFamilyD tf_head (mk_prom_eqns prom_thing)
                         ]
             , defun_decs
             , mk_alet_dec_rhs thing )

    promote_let_dec_ty :: [LocalVar]
                                 -- The local variables that the let-dec closes
                                 -- over. If this is non-empty, we cannot
                                 -- produce a standalone kind signature.
                                 -- See Note [No SAKs for let-decs with local variables]
                       -> Int    -- The number of arguments to default to if the
                                 -- type cannot be inferred. This is 0 for UValues
                                 -- and the number of arguments in a single clause
                                 -- for UFunctions.
                       -> PrM (Maybe LetDecRHSKindInfo, Int)
                                 -- Returns two things in a pair:
                                 --
                                 -- 1. Information about the promoted kind,
                                 --    if available.
                                 --
                                 -- 2. The number of arguments the let-dec has.
                                 --    If no kind information is available from
                                 --    which to infer this number, then this
                                 --    will default to the earlier Int argument.
    promote_let_dec_ty :: [LocalVar] -> Int -> PrM (Maybe LetDecRHSKindInfo, Int)
promote_let_dec_ty [LocalVar]
all_locals Int
default_num_args =
      case LetDecRHSSort
rhs_sort of
        ClassMethodRHS OSet LocalVar
scoped_tvs [DTyVarBndr Specificity]
tvbs DCxt
arg_kis DType
res_ki
          -> let sak :: DType
sak = [DTyVarBndr Specificity] -> DCxt -> DCxt -> DType -> DType
ravelVanillaDType [DTyVarBndr Specificity]
tvbs [] DCxt
arg_kis DType
res_ki in
             (Maybe LetDecRHSKindInfo, Int)
-> PrM (Maybe LetDecRHSKindInfo, Int)
forall a. a -> PrM a
forall (m :: * -> *) a. Monad m => a -> m a
return (LetDecRHSKindInfo -> Maybe LetDecRHSKindInfo
forall a. a -> Maybe a
Just (Maybe DType
-> OSet LocalVar
-> [DTyVarBndr Specificity]
-> DCxt
-> DType
-> LetDecRHSKindInfo
LDRKI (DType -> Maybe DType
forall a. a -> Maybe a
Just DType
sak) OSet LocalVar
scoped_tvs [DTyVarBndr Specificity]
tvbs DCxt
arg_kis DType
res_ki), DCxt -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length DCxt
arg_kis)
        LetDecRHSSort
LetBindingRHS
          |  Just DType
ty <- Name -> OMap Name DType -> Maybe DType
forall k v. Ord k => k -> OMap k v -> Maybe v
OMap.lookup Name
name OMap Name DType
type_env
          -> do
          -- promoteType turns rank-1 uses of (->) into (~>). So, we unravel
          -- first to avoid this behavior, and then ravel back.
          (tvbs, argKs, resultK) <- DType -> PrM ([DTyVarBndr Specificity], DCxt, DType)
forall (m :: * -> *).
OptionsMonad m =>
DType -> m ([DTyVarBndr Specificity], DCxt, DType)
promoteUnraveled DType
ty
          let m_sak | [LocalVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [LocalVar]
all_locals = DType -> Maybe DType
forall a. a -> Maybe a
Just (DType -> Maybe DType) -> DType -> Maybe DType
forall a b. (a -> b) -> a -> b
$ [DTyVarBndr Specificity] -> DCxt -> DCxt -> DType -> DType
ravelVanillaDType [DTyVarBndr Specificity]
tvbs [] DCxt
argKs DType
resultK
                      -- If this let-dec closes over local variables, then
                      -- don't give it a SAK.
                      -- See Note [No SAKs for let-decs with local variables]
                    | Bool
otherwise       = Maybe DType
forall a. Maybe a
Nothing
          -- If ScopedTypeVariables is enabled, bring all of the type variables
          -- from the outermost forall into scope over the RHS.
          scoped_tvs_ext <- qIsExtEnabled LangExt.ScopedTypeVariables
          let scoped_tvs | Bool
scoped_tvs_ext
                         = [LocalVar] -> OSet LocalVar
forall a. Ord a => [a] -> OSet a
OSet.fromList ((DTyVarBndr Specificity -> LocalVar)
-> [DTyVarBndr Specificity] -> [LocalVar]
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndr Specificity -> LocalVar
forall flag. DTyVarBndr flag -> LocalVar
tvbToLocalVar [DTyVarBndr Specificity]
tvbs)
                         | Bool
otherwise
                         = OSet LocalVar
forall a. OSet a
OSet.empty
          -- invariant: count_args ty == length argKs
          return (Just (LDRKI m_sak scoped_tvs tvbs argKs resultK), length argKs)

          |  Bool
otherwise
          -> (Maybe LetDecRHSKindInfo, Int)
-> PrM (Maybe LetDecRHSKindInfo, Int)
forall a. a -> PrM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe LetDecRHSKindInfo
forall a. Maybe a
Nothing, Int
default_num_args)

    etaContractOrExpand :: Int -> Int -> DClause -> PrM DClause
    etaContractOrExpand :: Int -> Int -> DClause -> PrM DClause
etaContractOrExpand Int
ty_num_args Int
clause_num_args (DClause [DPat]
pats DExp
exp)
      | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 = do -- Eta-expand
          names <- Int -> PrM Name -> PrM [Name]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
n (String -> PrM Name
forall (m :: * -> *). Quasi m => String -> m Name
newUniqueName String
"a")
          let newPats = (Name -> DPat) -> [Name] -> [DPat]
forall a b. (a -> b) -> [a] -> [b]
map Name -> DPat
DVarP [Name]
names
              newArgs = (Name -> DExp) -> [Name] -> [DExp]
forall a b. (a -> b) -> [a] -> [b]
map Name -> DExp
DVarE [Name]
names
          return $ DClause (pats ++ newPats) (foldExp exp newArgs)
      | Bool
otherwise = do -- Eta-contract
          let ([DPat]
clausePats, [DPat]
lamPats) = Int -> [DPat] -> ([DPat], [DPat])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
ty_num_args [DPat]
pats
              lamExp :: DExp
lamExp = [DPat] -> DExp -> DExp
dLamE [DPat]
lamPats DExp
exp
          DClause -> PrM DClause
forall a. a -> PrM a
forall (m :: * -> *) a. Monad m => a -> m a
return (DClause -> PrM DClause) -> DClause -> PrM DClause
forall a b. (a -> b) -> a -> b
$ [DPat] -> DExp -> DClause
DClause [DPat]
clausePats DExp
lamExp
      where
        n :: Int
n = Int
ty_num_args Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
clause_num_args

    count_args :: [DClause] -> PrM Int
    count_args :: [DClause] -> PrM Int
count_args (DClause [DPat]
pats DExp
_ : [DClause]
_) = Int -> PrM Int
forall a. a -> PrM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> PrM Int) -> Int -> PrM Int
forall a b. (a -> b) -> a -> b
$ [DPat] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [DPat]
pats
    count_args [DClause]
_ = String -> PrM Int
forall a. String -> PrM a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> PrM Int) -> String -> PrM Int
forall a b. (a -> b) -> a -> b
$ String
"Impossible! A function without clauses."

-- An auxiliary data type used in promoteLetDecRHS that describes information
-- related to the promoted kind of a class method default or normal
-- let binding.
data LetDecRHSKindInfo =
  LDRKI (Maybe DKind)    -- The standalone kind signature, if applicable.
                         -- This will be Nothing if the let-dec RHS has local
                         -- variables that it closes over.
                         -- See Note [No SAKs for let-decs with local variables]
        (OSet LocalVar)  -- The scoped type variables to bring into scope over
                         -- the RHS of the let-dec. This will be a subset of the
                         -- type variables of the kind (see the field below),
                         -- but not necessarily the same. See
                         -- Note [Scoped type variables and class methods]
                         -- (Wrinkle: Partial scoping) in D.S.TH.Promote.Monad
                         -- for an example where this can be a proper subset.
        [DTyVarBndrSpec] -- The type variable binders of the kind.
        [DKind]          -- The argument kinds.
        DKind            -- The result kind.

{-
Note [No SAKs for let-decs with local variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider promoting this:

  f :: Bool
  f = let x = True
          g :: () -> Bool
          g _ = x
      in g ()

Clearly, the promoted `F` type family will have the following SAK:

  type F :: ()

What about `G`? At a passing glance, it appears that you could get away with
this:

  type G :: Bool -> ()

But this isn't quite right, since `g` closes over `x = True`. The body of `G`,
therefore, has to lift `x` to be an explicit argument:

  type family G x (u :: ()) :: Bool where
    G x _ = x

At present, we don't keep track of the types of local variables like `x`, which
makes it difficult to create a SAK for things like `G`. Here are some possible
ideas, each followed by explanations for why they are infeasible:

* Use wildcards:

    type G :: _ -> () -> Bool

  Alas, GHC currently does not allow wildcards in SAKs. See GHC#17432.

* Use visible dependent quantification to avoid having to say what the kind
  of `x` is:

    type G :: forall x -> () -> Bool

  A clever trick to be sure, but it doesn't quite do what we want, since
  GHC will generalize that kind to become `forall (x :: k) -> () -> Bool`,
  which is more general than we want.

In any case, it's probably not worth bothering with SAKs for local definitions
like `g` in the first place, so we avoid generating SAKs for anything that
closes over at least one local variable for now. If someone yells about this,
we'll reconsider this design.

Note [Keep redundant kind information for Haddocks]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
`singletons-th` generates explicit argument kinds and result kinds for
type-level declarations whenever possible, even if those kinds are technically
redundant. For example, `singletons-th` would promote this:

  id' :: a -> a

To this:

  type Id' :: a -> a
  type family Id' (x :: a) :: a where ...

Strictly speaking, the argument and result kind of Id' are unnecessary, since
the same information is already present in the standalone kind signature.
However, due to a Haddock limitation
(https://github.com/haskell/haddock/issues/1178), Haddock will not render
standalone kind signatures at all, so if the argument and result kind of Id'
were omitted in the body, Haddock would render it like so:

  type family Id' x where ...

This is unfortunate for Haddock viewers, as this does not convey any kind
information whatsoever. Until the aformentioned Haddock issue is resolved, we
work around this limitation by generating the redundant argument and kind
information anyway. Thankfully, this is simple to accomplish, as we already
compute this information to begin with.

Note [Generating type families with the correct arity]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
As of GHC 9.10, GHC no longer performs arity inference when kind-checking type
family declarations with standalone kind signatures. This is an important
consideration when promoting functions with top-level type signatures. For
example, we would not want to take this definition:

  f :: Either a Bool
  f = Right True

And promote it to this type family:

  type F :: Either a Bool
  type family F where
    F = Right True

GHC would reject this type family because it would expect F to have arity 0,
but its definition requires arity 1. This is because the definition of F is
tantamount to writing:

  F @a = Right @a @Bool True -- This takes 1 argument, hence arity 1

In order to make F kind-check, we need to generate a type family header that
explicitly declares it to have arity 1, not arity 0:

  type F :: Either a Bool
  type family F @a where
    F = Right True

Note the @a binder after F in the type family header.

If the standalone kind signature lacks an outermost forall, then we simply bind
the type variables in left-to-right order, preserving dependencies (using
`toposortTyVarsOf`). If the standalone kind signature does have an outermost
`forall`, then we bind the type variables according to the order in which it
appears in the `forall`, making sure to filter out any inferred type variable
binders. For example, we would want to take this definition (from #585):

  konst :: forall a {b}. a -> b -> a
  konst x _ = x

And promote it to this type family:

  type Konst :: forall a {b}. a -> b -> a
  type family Konst @a x y where
    Konst @a (x :: a) (_ :: b) = x

Note that we do not bind @b here. The `dtvbSpecsToBndrVis` function is
responsible for filtering out inferred type variable binders.
-}

promoteClause :: Maybe Uniq
                 -- ^ Let-binding unique (if locally bound)
              -> Name
                 -- ^ Name of the function being promoted
              -> Maybe LetDecRHSKindInfo
                 -- ^ Information about the promoted kind (if present)
              -> [LocalVar]
                 -- ^ The local variables currently in scope
              -> DClause -> PrM (DTySynEqn, ADClause)
promoteClause :: Maybe Uniq
-> Name
-> Maybe LetDecRHSKindInfo
-> [LocalVar]
-> DClause
-> PrM (DTySynEqn, ADClause)
promoteClause Maybe Uniq
mb_let_uniq Name
name Maybe LetDecRHSKindInfo
m_ldrki [LocalVar]
all_locals (DClause [DPat]
pats DExp
exp) = do
  -- First, check to see if we know the kinds of the patterns in the clause...
  let m_kinds :: Maybe DCxt
m_kinds = (LetDecRHSKindInfo -> DCxt)
-> Maybe LetDecRHSKindInfo -> Maybe DCxt
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(LDRKI Maybe DType
_ OSet LocalVar
_ [DTyVarBndr Specificity]
_ DCxt
kinds DType
_) -> DCxt
kinds) Maybe LetDecRHSKindInfo
m_ldrki
  -- ...if so, use these kinds when promoting the patterns to the type level.
  -- Promoting patterns can create LocalVars, and these LocalVars are brought
  -- into scope when promoting the RHS of the clause. Recording the kinds of
  -- each LocalVar will make the lambda-lifted code more precise. (See
  -- Note [Local variables and kind information] in
  -- D.S.TH.Promote.Syntax.LocalVar.)
  ((types, pats'), prom_pat_infos) <- QWithAux PromDPatInfos PrM (DCxt, [ADPat])
-> PrM ((DCxt, [ADPat]), PromDPatInfos)
forall m (q :: * -> *) a. QWithAux m q a -> q (a, m)
evalForPair (QWithAux PromDPatInfos PrM (DCxt, [ADPat])
 -> PrM ((DCxt, [ADPat]), PromDPatInfos))
-> QWithAux PromDPatInfos PrM (DCxt, [ADPat])
-> PrM ((DCxt, [ADPat]), PromDPatInfos)
forall a b. (a -> b) -> a -> b
$
    case Maybe DCxt
m_kinds of
      Just DCxt
kinds ->
        [(DType, ADPat)] -> (DCxt, [ADPat])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(DType, ADPat)] -> (DCxt, [ADPat]))
-> QWithAux PromDPatInfos PrM [(DType, ADPat)]
-> QWithAux PromDPatInfos PrM (DCxt, [ADPat])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (DType -> DPat -> QWithAux PromDPatInfos PrM (DType, ADPat))
-> DCxt -> [DPat] -> QWithAux PromDPatInfos PrM [(DType, ADPat)]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (\DType
kind -> Maybe DType -> DPat -> QWithAux PromDPatInfos PrM (DType, ADPat)
promotePat (DType -> Maybe DType
forall a. a -> Maybe a
Just DType
kind)) DCxt
kinds [DPat]
pats
      Maybe DCxt
Nothing ->
        (DPat -> QWithAux PromDPatInfos PrM (DType, ADPat))
-> [DPat] -> QWithAux PromDPatInfos PrM (DCxt, [ADPat])
forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM (Maybe DType -> DPat -> QWithAux PromDPatInfos PrM (DType, ADPat)
promotePat Maybe DType
forall a. Maybe a
Nothing) [DPat]
pats
  -- If the function has scoped type variables, then we annotate each argument
  -- in the promoted type family equation with its kind.
  -- See Note [Scoped type variables] in Data.Singletons.TH.Promote.Monad for an
  -- explanation of why we do this.
  let types_w_kinds =
        case Maybe LetDecRHSKindInfo
m_ldrki of
          Just (LDRKI Maybe DType
_ OSet LocalVar
scoped_tvs [DTyVarBndr Specificity]
_ DCxt
kinds DType
_)
            |  Bool -> Bool
not (OSet LocalVar -> Bool
forall a. OSet a -> Bool
OSet.null OSet LocalVar
scoped_tvs)
            -> (DType -> DType -> DType) -> DCxt -> DCxt -> DCxt
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith DType -> DType -> DType
DSigT DCxt
types DCxt
kinds
          Maybe LetDecRHSKindInfo
_ -> DCxt
types
  let PromDPatInfos { prom_dpat_vars    = new_vars
                    , prom_dpat_sig_kvs = sig_kvs } = prom_pat_infos
  (ty, ann_exp) <- scopedBind sig_kvs $
                   lambdaBind new_vars $
                   promoteExp exp
  pro_clause_fun <- promoteLetDecName mb_let_uniq name m_ldrki all_locals
  return ( DTySynEqn Nothing (foldType pro_clause_fun types_w_kinds) ty
         , ADClause new_vars pats' ann_exp )

-- | Promote a term pattern into a type pattern, accumulating bound variable
-- names in 'PromDPatInfos'.
promotePat ::
     Maybe DKind
     -- ^ The kind of the pattern ('Just' if known, 'Nothing' if unknown). When
     -- the kind is known, we can record a 'LocalVar' for variable patterns (see
     -- the 'DVarP' case below) that includes more precise kind information. See
     -- @Note [Local variables and kind information] (Wrinkle: Binding positions
     -- versus argument positions)@ in
     -- "Data.Singletons.TH.Promote.Syntax.LocalVar" for more information.
  -> DPat
  -> QWithAux PromDPatInfos PrM (DType, ADPat)
promotePat :: Maybe DType -> DPat -> QWithAux PromDPatInfos PrM (DType, ADPat)
promotePat Maybe DType
_ (DLitP Lit
lit) = (, Lit -> ADPat
ADLitP Lit
lit) (DType -> (DType, ADPat))
-> QWithAux PromDPatInfos PrM DType
-> QWithAux PromDPatInfos PrM (DType, ADPat)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lit -> QWithAux PromDPatInfos PrM DType
forall (m :: * -> *). MonadFail m => Lit -> m DType
promoteLitPat Lit
lit
promotePat Maybe DType
m_ki (DVarP Name
name) = do
      -- term vars can be symbols... type vars can't!
  tyName <- Name -> QWithAux PromDPatInfos PrM Name
forall (q :: * -> *). Quasi q => Name -> q Name
mkTyName Name
name
  let lv = LocalVar { lvName :: Name
lvName = Name
tyName, lvKind :: Maybe DType
lvKind = Maybe DType
m_ki }
  tell $ PromDPatInfos [(name, lv)] OSet.empty
  return (DVarT tyName, ADVarP name)
promotePat Maybe DType
_ (DConP Name
name DCxt
tys [DPat]
pats) = do
  opts <- QWithAux PromDPatInfos PrM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  kis <- traverse (promoteType_options conOptions) tys
  (types, pats') <- mapAndUnzipM (promotePat Nothing) pats
  let name' = Options -> Name -> Name
promotedDataTypeOrConName Options
opts Name
name
  return (foldType (foldl DAppKindT (DConT name') kis) types, ADConP name kis pats')
  where
    -- Currently, visible type patterns of data constructors are the one place
    -- in `singletons-th` where it makes sense to promote wildcard types, as it
    -- will produce code that GHC will accept.
    conOptions :: PromoteTypeOptions
    conOptions :: PromoteTypeOptions
conOptions = PromoteTypeOptions
defaultPromoteTypeOptions{ptoAllowWildcards = True}
promotePat Maybe DType
m_ki (DTildeP DPat
pat) = do
  String -> QWithAux PromDPatInfos PrM ()
forall (q :: * -> *). Quasi q => String -> q ()
qReportWarning String
"Lazy pattern converted into regular pattern in promotion"
  (ADPat -> ADPat) -> (DType, ADPat) -> (DType, ADPat)
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second ADPat -> ADPat
ADTildeP ((DType, ADPat) -> (DType, ADPat))
-> QWithAux PromDPatInfos PrM (DType, ADPat)
-> QWithAux PromDPatInfos PrM (DType, ADPat)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe DType -> DPat -> QWithAux PromDPatInfos PrM (DType, ADPat)
promotePat Maybe DType
m_ki DPat
pat
promotePat Maybe DType
m_ki (DBangP DPat
pat) = do
  String -> QWithAux PromDPatInfos PrM ()
forall (q :: * -> *). Quasi q => String -> q ()
qReportWarning String
"Strict pattern converted into regular pattern in promotion"
  (ADPat -> ADPat) -> (DType, ADPat) -> (DType, ADPat)
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second ADPat -> ADPat
ADBangP ((DType, ADPat) -> (DType, ADPat))
-> QWithAux PromDPatInfos PrM (DType, ADPat)
-> QWithAux PromDPatInfos PrM (DType, ADPat)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe DType -> DPat -> QWithAux PromDPatInfos PrM (DType, ADPat)
promotePat Maybe DType
m_ki DPat
pat
promotePat Maybe DType
_ (DSigP DPat
pat DType
ty) = do
  -- We must maintain the invariant that any promoted pattern signature must
  -- not have any wildcards in the underlying pattern.
  -- See Note [Singling pattern signatures].
  wildless_pat <- DPat -> QWithAux PromDPatInfos PrM DPat
forall (q :: * -> *). DsMonad q => DPat -> q DPat
removeWilds DPat
pat
  ki <- promoteType ty
  (promoted, pat') <- promotePat (Just ki) wildless_pat
  tell $ PromDPatInfos []
       $ OSet.fromList
       $ map tvbToLocalVar
       $ toposortTyVarsOf [ki]
  return (DSigT promoted ki, ADSigP promoted pat' ki)
promotePat Maybe DType
_ DPat
DWildP = (DType, ADPat) -> QWithAux PromDPatInfos PrM (DType, ADPat)
forall a. a -> QWithAux PromDPatInfos PrM a
forall (m :: * -> *) a. Monad m => a -> m a
return (DType
DWildCardT, ADPat
ADWildP)
promotePat Maybe DType
_ p :: DPat
p@(DTypeP DType
_) = String -> QWithAux PromDPatInfos PrM (DType, ADPat)
forall a. String -> QWithAux PromDPatInfos PrM a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"Embedded type patterns cannot be promoted: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ DPat -> String
forall a. Show a => a -> String
show DPat
p)
promotePat Maybe DType
_ p :: DPat
p@(DInvisP DType
_) = String -> QWithAux PromDPatInfos PrM (DType, ADPat)
forall a. String -> QWithAux PromDPatInfos PrM a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"Invisible type patterns cannot be promoted: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ DPat -> String
forall a. Show a => a -> String
show DPat
p)

promoteExp :: DExp -> PrM (DType, ADExp)
promoteExp :: DExp -> PrM (DType, ADExp)
promoteExp (DVarE Name
name) = (DType -> (DType, ADExp)) -> PrM DType -> PrM (DType, ADExp)
forall a b. (a -> b) -> PrM a -> PrM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (, Name -> ADExp
ADVarE Name
name) (PrM DType -> PrM (DType, ADExp))
-> PrM DType -> PrM (DType, ADExp)
forall a b. (a -> b) -> a -> b
$ Name -> PrM DType
lookupVarE Name
name
promoteExp (DConE Name
name) = do
  opts <- PrM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  return (DConT $ defunctionalizedName0 opts name, ADConE name)
promoteExp (DLitE Lit
lit)  = (DType -> (DType, ADExp)) -> PrM DType -> PrM (DType, ADExp)
forall a b. (a -> b) -> PrM a -> PrM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (, Lit -> ADExp
ADLitE Lit
lit) (PrM DType -> PrM (DType, ADExp))
-> PrM DType -> PrM (DType, ADExp)
forall a b. (a -> b) -> a -> b
$ Lit -> PrM DType
forall (q :: * -> *). OptionsMonad q => Lit -> q DType
promoteLitExp Lit
lit
promoteExp (DAppE DExp
exp1 DExp
exp2) = do
  (exp1', ann_exp1) <- DExp -> PrM (DType, ADExp)
promoteExp DExp
exp1
  (exp2', ann_exp2) <- promoteExp exp2
  return (apply exp1' exp2', ADAppE ann_exp1 ann_exp2)
-- Until we get visible kind applications, this is the best we can do.
promoteExp (DAppTypeE DExp
exp DType
_) = do
  String -> PrM ()
forall (q :: * -> *). Quasi q => String -> q ()
qReportWarning String
"Visible type applications are ignored by `singletons-th`."
  DExp -> PrM (DType, ADExp)
promoteExp DExp
exp
promoteExp (DLamCasesE [DClause]
clauses) = do
  opts <- PrM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  lam_cases_tf_name <- newUniqueName "LamCases"
  all_locals <- allLocals
  (eqns, ann_clauses) <-
    mapAndUnzipM (promoteClause Nothing lam_cases_tf_name Nothing all_locals) clauses
  -- Per the Haddocks for DLamCasesE, an empty list of clauses indicates that
  -- the overall `\cases` expression takes one argument. Otherwise, we look at
  -- the first clause to see how many arguments the expression takes, as each
  -- clause is required to have the same number of patterns.
  let num_args =
        case [DClause]
clauses of
          [] -> Int
1
          DClause [DPat]
pats DExp
_ : [DClause]
_ -> [DPat] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [DPat]
pats
  arg_tvb_names <- replicateM num_args (newUniqueName "a")
  let arg_tvbs = (Name -> DTyVarBndrVis) -> [Name] -> [DTyVarBndrVis]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> BndrVis -> DTyVarBndrVis
forall flag. Name -> flag -> DTyVarBndr flag
`DPlainTV` BndrVis
BndrReq) [Name]
arg_tvb_names
      tfh      = Name
-> [LocalVar]
-> [DTyVarBndrVis]
-> DFamilyResultSig
-> DTypeFamilyHead
dTypeFamilyHead_with_locals Name
lam_cases_tf_name [LocalVar]
all_locals [DTyVarBndrVis]
arg_tvbs DFamilyResultSig
DNoSig
  emitDecs [DClosedTypeFamilyD tfh eqns]
  emitDecsM $ defunctionalize lam_cases_tf_name Nothing $ DefunNoSAK all_locals arg_tvbs Nothing
  let prom_lam_cases =
        DType -> [LocalVar] -> DType
foldTypeLocalVars
          (Name -> DType
DConT (Options -> Name -> Int -> Name
defunctionalizedName Options
opts Name
lam_cases_tf_name Int
0))
          [LocalVar]
all_locals
  pure (prom_lam_cases, ADLamCasesE num_args prom_lam_cases ann_clauses)
promoteExp (DLetE [DLetDec]
decs DExp
exp) = do
  unique <- PrM Uniq
forall (q :: * -> *). DsMonad q => q Uniq
qNewUnique
  (binds, ann_env) <- promoteLetDecs (Just unique) decs
  (exp', ann_exp) <- letBind binds $ promoteExp exp
  return (exp', ADLetE ann_env ann_exp)
promoteExp (DSigE DExp
exp DType
ty) = do
  (exp', ann_exp) <- DExp -> PrM (DType, ADExp)
promoteExp DExp
exp
  ty' <- promoteType ty
  return (DSigT exp' ty', ADSigE exp' ann_exp ty')
promoteExp e :: DExp
e@(DStaticE {}) = String -> PrM (DType, ADExp)
forall a. String -> PrM a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"Static expressions cannot be promoted: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ DExp -> String
forall a. Show a => a -> String
show DExp
e)
promoteExp e :: DExp
e@(DTypedBracketE {}) = String -> PrM (DType, ADExp)
forall a. String -> PrM a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"Typed bracket expressions cannot be promoted: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ DExp -> String
forall a. Show a => a -> String
show DExp
e)
promoteExp e :: DExp
e@(DTypedSpliceE {}) = String -> PrM (DType, ADExp)
forall a. String -> PrM a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"Typed splice expressions cannot be promoted: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ DExp -> String
forall a. Show a => a -> String
show DExp
e)
promoteExp e :: DExp
e@(DTypeE {}) = String -> PrM (DType, ADExp)
forall a. String -> PrM a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"Embedded type expressions cannot be promoted: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ DExp -> String
forall a. Show a => a -> String
show DExp
e)
promoteExp e :: DExp
e@(DForallE {}) = String -> PrM (DType, ADExp)
forall a. String -> PrM a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"Embedded `forall` expressions cannot be promoted: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ DExp -> String
forall a. Show a => a -> String
show DExp
e)
promoteExp e :: DExp
e@(DConstrainedE {}) = String -> PrM (DType, ADExp)
forall a. String -> PrM a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"Embedded constraint expressions cannot be promoted: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ DExp -> String
forall a. Show a => a -> String
show DExp
e)

promoteLitExp :: OptionsMonad q => Lit -> q DType
promoteLitExp :: forall (q :: * -> *). OptionsMonad q => Lit -> q DType
promoteLitExp (IntegerL Uniq
n) = do
  opts <- q Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  let tyFromIntegerName = Options -> Name -> Maybe Uniq -> Name
promotedValueName Options
opts Name
fromIntegerName Maybe Uniq
forall a. Maybe a
Nothing
      tyNegateName      = Options -> Name -> Maybe Uniq -> Name
promotedValueName Options
opts Name
negateName      Maybe Uniq
forall a. Maybe a
Nothing
  if n >= 0
     then return $ (DConT tyFromIntegerName `DAppT` DLitT (NumTyLit n))
     else return $ (DConT tyNegateName `DAppT`
                    (DConT tyFromIntegerName `DAppT` DLitT (NumTyLit (-n))))
promoteLitExp (StringL String
str) = do
  opts <- q Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  let prom_str_lit = TyLit -> DType
DLitT (String -> TyLit
StrTyLit String
str)
  os_enabled <- qIsExtEnabled LangExt.OverloadedStrings
  pure $ if os_enabled
         then DConT (promotedValueName opts fromStringName Nothing) `DAppT` prom_str_lit
         else prom_str_lit
promoteLitExp (CharL Char
c) = DType -> q DType
forall a. a -> q a
forall (m :: * -> *) a. Monad m => a -> m a
return (DType -> q DType) -> DType -> q DType
forall a b. (a -> b) -> a -> b
$ TyLit -> DType
DLitT (Char -> TyLit
CharTyLit Char
c)
promoteLitExp Lit
lit =
  String -> q DType
forall a. String -> q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"Only string, natural number, and character literals can be promoted: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Lit -> String
forall a. Show a => a -> String
show Lit
lit)

promoteLitPat :: MonadFail m => Lit -> m DType
promoteLitPat :: forall (m :: * -> *). MonadFail m => Lit -> m DType
promoteLitPat (IntegerL Uniq
n)
  | Uniq
n Uniq -> Uniq -> Bool
forall a. Ord a => a -> a -> Bool
>= Uniq
0    = DType -> m DType
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (DType -> m DType) -> DType -> m DType
forall a b. (a -> b) -> a -> b
$ (TyLit -> DType
DLitT (Uniq -> TyLit
NumTyLit Uniq
n))
  | Bool
otherwise =
    String -> m DType
forall a. String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> m DType) -> String -> m DType
forall a b. (a -> b) -> a -> b
$ String
"Negative literal patterns are not allowed,\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
           String
"because literal patterns are promoted to natural numbers."
promoteLitPat (StringL String
str) = DType -> m DType
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (DType -> m DType) -> DType -> m DType
forall a b. (a -> b) -> a -> b
$ TyLit -> DType
DLitT (String -> TyLit
StrTyLit String
str)
promoteLitPat (CharL Char
c) = DType -> m DType
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (DType -> m DType) -> DType -> m DType
forall a b. (a -> b) -> a -> b
$ TyLit -> DType
DLitT (Char -> TyLit
CharTyLit Char
c)
promoteLitPat Lit
lit =
  String -> m DType
forall a. String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"Only string, natural number, and character literals can be promoted: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Lit -> String
forall a. Show a => a -> String
show Lit
lit)

-- Promote the name of a 'ULetDecRHS' to the type level. If the promoted
-- 'ULetDecRHS' has a standalone type signature and does not close over any
-- local variables, then this will include the scoped type variables from the
-- type signature as invisible arguments. (See Note [Scoped type variables] in
-- Data.Singletons.TH.Promote.Monad.) Otherwise, it will include any local
-- variables that it closes over as explicit arguments.
promoteLetDecName ::
     Maybe Uniq
     -- ^ Let-binding unique (if locally bound)
  -> Name
     -- ^ Name of the function being promoted
  -> Maybe LetDecRHSKindInfo
     -- ^ Information about the promoted kind (if present)
  -> [LocalVar]
     -- ^ The local variables currently in scope
  -> PrM DType
promoteLetDecName :: Maybe Uniq
-> Name -> Maybe LetDecRHSKindInfo -> [LocalVar] -> PrM DType
promoteLetDecName Maybe Uniq
mb_let_uniq Name
name Maybe LetDecRHSKindInfo
m_ldrki [LocalVar]
all_locals = do
  opts <- PrM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  let proName = Options -> Name -> Maybe Uniq -> Name
promotedValueName Options
opts Name
name Maybe Uniq
mb_let_uniq
      type_args =
        case Maybe LetDecRHSKindInfo
m_ldrki of
          Just (LDRKI Maybe DType
m_sak OSet LocalVar
_ [DTyVarBndr Specificity]
tvbs DCxt
_ DType
_)
            |  Maybe DType -> Bool
forall a. Maybe a -> Bool
isJust Maybe DType
m_sak
               -- Per the comments on LetDecRHSKindInfo, `isJust m_sak` is only True
               -- if there are no local variables. Convert the scoped type variables
               -- `tvbs` to invisible arguments, making sure to use
               -- `dtvbSpecsToBndrVis` to filter out any inferred type variable
               -- binders. For instance, we want to promote this example (from #585):
               --
               --   konst :: forall a {b}. a -> b -> a
               --   konst x _ = x
               --
               -- To this type family:
               --
               --   type Konst :: forall a {b}. a -> b -> a
               --   type family Konst @a x y where
               --     Konst @a (x :: a) (_ :: b) = x
               --
               -- Note that we apply `a` in `Konst @a` but _not_ `b`, as `b` is
               -- bound using an inferred type variable binder.
            -> (DTyVarBndrVis -> DTypeArg) -> [DTyVarBndrVis] -> [DTypeArg]
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndrVis -> DTypeArg
dTyVarBndrVisToDTypeArg ([DTyVarBndrVis] -> [DTypeArg]) -> [DTyVarBndrVis] -> [DTypeArg]
forall a b. (a -> b) -> a -> b
$ [DTyVarBndr Specificity] -> [DTyVarBndrVis]
dtvbSpecsToBndrVis [DTyVarBndr Specificity]
tvbs
          Maybe LetDecRHSKindInfo
_ -> -- ...otherwise, return the local variables as explicit arguments
               -- using DTANormal.
               (LocalVar -> DTypeArg) -> [LocalVar] -> [DTypeArg]
forall a b. (a -> b) -> [a] -> [b]
map LocalVar -> DTypeArg
localVarToTypeArg [LocalVar]
all_locals
  pure $ applyDType (DConT proName) type_args

-- Construct a 'DTypeFamilyHead' that closes over some local variables. We
-- apply `noExactName` to each local variable to avoid GHC#11812.
-- See also Note [Pitfalls of NameU/NameL] in Data.Singletons.TH.Util.
dTypeFamilyHead_with_locals ::
     Name
  -- ^ Name of type family
  -> [LocalVar]
  -- ^ Local variables
  -> [DTyVarBndrVis]
  -- ^ Variables for type family arguments
  -> DFamilyResultSig
  -- ^ Type family result
  -> DTypeFamilyHead
dTypeFamilyHead_with_locals :: Name
-> [LocalVar]
-> [DTyVarBndrVis]
-> DFamilyResultSig
-> DTypeFamilyHead
dTypeFamilyHead_with_locals Name
tf_nm [LocalVar]
local_vars [DTyVarBndrVis]
arg_tvbs DFamilyResultSig
res_sig =
  Name
-> [DTyVarBndrVis]
-> DFamilyResultSig
-> Maybe InjectivityAnn
-> DTypeFamilyHead
DTypeFamilyHead
    Name
tf_nm
    ((LocalVar -> DTyVarBndrVis) -> [LocalVar] -> [DTyVarBndrVis]
forall a b. (a -> b) -> [a] -> [b]
map (BndrVis -> LocalVar -> DTyVarBndrVis
forall flag. flag -> LocalVar -> DTyVarBndr flag
localVarToTvb BndrVis
BndrReq) [LocalVar]
local_vars' [DTyVarBndrVis] -> [DTyVarBndrVis] -> [DTyVarBndrVis]
forall a. [a] -> [a] -> [a]
++ [DTyVarBndrVis]
arg_tvbs')
    DFamilyResultSig
res_sig'
    Maybe InjectivityAnn
forall a. Maybe a
Nothing
  where
    -- We take care to only apply `noExactTyVars` to the local variables and not
    -- to any of the argument/result types. The latter are much more likely to
    -- show up in the Haddocks, and `noExactTyVars` produces incredibly long
    -- Names that are much harder to read in the rendered Haddocks.
    local_vars' :: [LocalVar]
local_vars' = [LocalVar] -> [LocalVar]
forall a. Data a => a -> a
noExactTyVars [LocalVar]
local_vars

    -- Ensure that all references to local_nms are substituted away.
    subst1 :: Map Name DType
subst1 = [LetBind] -> Map Name DType
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([LetBind] -> Map Name DType) -> [LetBind] -> Map Name DType
forall a b. (a -> b) -> a -> b
$
             (LocalVar -> LocalVar -> LetBind)
-> [LocalVar] -> [LocalVar] -> [LetBind]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith
               (\(LocalVar { lvName :: LocalVar -> Name
lvName = Name
local_nm }) (LocalVar { lvName :: LocalVar -> Name
lvName = Name
local_nm' }) ->
                 (Name
local_nm, Name -> DType
DVarT Name
local_nm'))
               [LocalVar]
local_vars
               [LocalVar]
local_vars'
    (Map Name DType
subst2, [DTyVarBndrVis]
arg_tvbs') = Map Name DType
-> [DTyVarBndrVis] -> (Map Name DType, [DTyVarBndrVis])
forall flag.
Map Name DType
-> [DTyVarBndr flag] -> (Map Name DType, [DTyVarBndr flag])
SC.substTyVarBndrs Map Name DType
subst1 [DTyVarBndrVis]
arg_tvbs
    (Map Name DType
_subst3, DFamilyResultSig
res_sig') = Map Name DType
-> DFamilyResultSig -> (Map Name DType, DFamilyResultSig)
substFamilyResultSig Map Name DType
subst2 DFamilyResultSig
res_sig