{- Data/Singletons/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 package.
-}

{-# LANGUAGE TemplateHaskell, MultiWayIf, LambdaCase, TupleSections,
             ScopedTypeVariables #-}

module Data.Singletons.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 Data.Singletons.Names
import Data.Singletons.Promote.Monad
import Data.Singletons.Promote.Eq
import Data.Singletons.Promote.Defun
import Data.Singletons.Promote.Type
import Data.Singletons.Deriving.Ord
import Data.Singletons.Deriving.Bounded
import Data.Singletons.Deriving.Enum
import Data.Singletons.Deriving.Show
import Data.Singletons.Deriving.Util
import Data.Singletons.Partition
import Data.Singletons.TH.Options
import Data.Singletons.Util
import Data.Singletons.Syntax
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.List (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 and fixity declarations] in D.S.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 :: [Name] -> q [Dec]
genPromotions [Name]
names = do
  Options
opts <- q Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  -- See Note [Disable genQuotedDecs in genPromotions and genSingletons]
  Options -> OptionsM q [Dec] -> q [Dec]
forall (m :: * -> *) a. Options -> OptionsM m a -> m a
withOptions Options
opts{genQuotedDecs :: Bool
genQuotedDecs = Bool
False} (OptionsM q [Dec] -> q [Dec]) -> OptionsM q [Dec] -> q [Dec]
forall a b. (a -> b) -> a -> b
$ do
    [Name] -> OptionsM q ()
forall (q :: * -> *). Quasi q => [Name] -> q ()
checkForRep [Name]
names
    [Info]
infos <- (Name -> OptionsM q Info) -> [Name] -> OptionsM q [Info]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Name -> OptionsM q Info
forall (q :: * -> *). DsMonad q => Name -> q Info
reifyWithLocals [Name]
names
    [DInfo]
dinfos <- (Info -> OptionsM q DInfo) -> [Info] -> OptionsM q [DInfo]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Info -> OptionsM q DInfo
forall (q :: * -> *). DsMonad q => Info -> q DInfo
dsInfo [Info]
infos
    [DDec]
ddecs <- [Dec] -> PrM () -> OptionsM q [DDec]
forall (q :: * -> *). OptionsMonad q => [Dec] -> PrM () -> q [DDec]
promoteM_ [] (PrM () -> OptionsM q [DDec]) -> PrM () -> OptionsM q [DDec]
forall a b. (a -> b) -> a -> b
$ (DInfo -> PrM ()) -> [DInfo] -> PrM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ DInfo -> PrM ()
promoteInfo [DInfo]
dinfos
    [Dec] -> OptionsM q [Dec]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Dec] -> OptionsM q [Dec]) -> [Dec] -> OptionsM q [Dec]
forall a b. (a -> b) -> a -> b
$ [DDec] -> [Dec]
decsToTH [DDec]
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 :: q [Dec] -> q [Dec]
promote q [Dec]
qdecs = do
  Options
opts <- q Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  Options -> OptionsM q [Dec] -> q [Dec]
forall (m :: * -> *) a. Options -> OptionsM m a -> m a
withOptions Options
opts{genQuotedDecs :: Bool
genQuotedDecs = Bool
True} (OptionsM q [Dec] -> q [Dec]) -> OptionsM q [Dec] -> q [Dec]
forall a b. (a -> b) -> a -> b
$ OptionsM q [Dec] -> OptionsM q [Dec]
forall (q :: * -> *). OptionsMonad q => q [Dec] -> q [Dec]
promote' (OptionsM q [Dec] -> OptionsM q [Dec])
-> OptionsM q [Dec] -> OptionsM q [Dec]
forall a b. (a -> b) -> a -> b
$ q [Dec] -> OptionsM q [Dec]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift q [Dec]
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 :: q [Dec] -> q [Dec]
promoteOnly q [Dec]
qdecs = do
  Options
opts <- q Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  Options -> OptionsM q [Dec] -> q [Dec]
forall (m :: * -> *) a. Options -> OptionsM m a -> m a
withOptions Options
opts{genQuotedDecs :: Bool
genQuotedDecs = Bool
False} (OptionsM q [Dec] -> q [Dec]) -> OptionsM q [Dec] -> q [Dec]
forall a b. (a -> b) -> a -> b
$ OptionsM q [Dec] -> OptionsM q [Dec]
forall (q :: * -> *). OptionsMonad q => q [Dec] -> q [Dec]
promote' (OptionsM q [Dec] -> OptionsM q [Dec])
-> OptionsM q [Dec] -> OptionsM q [Dec]
forall a b. (a -> b) -> a -> b
$ q [Dec] -> OptionsM q [Dec]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift q [Dec]
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' :: q [Dec] -> q [Dec]
promote' q [Dec]
qdecs = do
  Options
opts     <- q Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  [Dec]
decs     <- q [Dec]
qdecs
  [DDec]
ddecs    <- [Dec] -> DsM q [DDec] -> q [DDec]
forall (q :: * -> *) a. DsMonad q => [Dec] -> DsM q a -> q a
withLocalDeclarations [Dec]
decs (DsM q [DDec] -> q [DDec]) -> DsM q [DDec] -> q [DDec]
forall a b. (a -> b) -> a -> b
$ [Dec] -> DsM q [DDec]
forall (q :: * -> *). DsMonad q => [Dec] -> q [DDec]
dsDecs [Dec]
decs
  [DDec]
promDecs <- [Dec] -> PrM () -> q [DDec]
forall (q :: * -> *). OptionsMonad q => [Dec] -> PrM () -> q [DDec]
promoteM_ [Dec]
decs (PrM () -> q [DDec]) -> PrM () -> q [DDec]
forall a b. (a -> b) -> a -> b
$ [DDec] -> PrM ()
promoteDecs [DDec]
ddecs
  let origDecs :: [Dec]
origDecs | Options -> Bool
genQuotedDecs Options
opts = [Dec]
decs
               | Bool
otherwise          = []
  [Dec] -> q [Dec]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Dec] -> q [Dec]) -> [Dec] -> q [Dec]
forall a b. (a -> b) -> a -> b
$ [Dec]
origDecs [Dec] -> [Dec] -> [Dec]
forall a. [a] -> [a] -> [a]
++ [DDec] -> [Dec]
decsToTH [DDec]
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 :: [Name] -> q [Dec]
genDefunSymbols [Name]
names = do
  [Name] -> q ()
forall (q :: * -> *). Quasi q => [Name] -> q ()
checkForRep [Name]
names
  [DInfo]
infos <- (Name -> q DInfo) -> [Name] -> q [DInfo]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t 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
  [DDec]
decs <- [Dec] -> PrM [DDec] -> q [DDec]
forall (q :: * -> *).
OptionsMonad q =>
[Dec] -> PrM [DDec] -> q [DDec]
promoteMDecs [] (PrM [DDec] -> q [DDec]) -> PrM [DDec] -> q [DDec]
forall a b. (a -> b) -> a -> b
$ (DInfo -> PrM [DDec]) -> [DInfo] -> PrM [DDec]
forall (monad :: * -> *) monoid (t :: * -> *) a.
(Monad monad, Monoid monoid, Traversable t) =>
(a -> monad monoid) -> t a -> monad monoid
concatMapM DInfo -> PrM [DDec]
defunInfo [DInfo]
infos
  [Dec] -> q [Dec]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Dec] -> q [Dec]) -> [Dec] -> q [Dec]
forall a b. (a -> b) -> a -> b
$ [DDec] -> [Dec]
decsToTH [DDec]
decs

-- | Produce instances for @(==)@ (type-level equality) from the given types
promoteEqInstances :: OptionsMonad q => [Name] -> q [Dec]
promoteEqInstances :: [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 instances for 'POrd' from the given types
promoteOrdInstances :: OptionsMonad q => [Name] -> q [Dec]
promoteOrdInstances :: [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 :: 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 :: [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 :: 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 :: [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 :: 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 :: [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 :: Name -> q [Dec]
promoteShowInstance = DerivDesc q -> String -> Name -> q [Dec]
forall (q :: * -> *).
OptionsMonad q =>
DerivDesc q -> String -> Name -> q [Dec]
promoteInstance (ShowMode -> DerivDesc q
forall (q :: * -> *). OptionsMonad q => ShowMode -> DerivDesc q
mkShowInstance ShowMode
ForPromotion) String
"Show"

-- | Produce an instance for @(==)@ (type-level equality) from the given type
promoteEqInstance :: OptionsMonad q => Name -> q [Dec]
promoteEqInstance :: Name -> q [Dec]
promoteEqInstance Name
name = do
  ([TyVarBndr]
tvbs, [Con]
cons) <- String -> Name -> q ([TyVarBndr], [Con])
forall (q :: * -> *).
DsMonad q =>
String -> Name -> q ([TyVarBndr], [Con])
getDataD String
"I cannot make an instance of (==) for it." Name
name
  [DTyVarBndr]
tvbs' <- (TyVarBndr -> q DTyVarBndr) -> [TyVarBndr] -> q [DTyVarBndr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM TyVarBndr -> q DTyVarBndr
forall (q :: * -> *). DsMonad q => TyVarBndr -> q DTyVarBndr
dsTvb [TyVarBndr]
tvbs
  let data_ty :: DType
data_ty = DType -> [DTyVarBndr] -> DType
foldTypeTvbs (Name -> DType
DConT Name
name) [DTyVarBndr]
tvbs'
  [DCon]
cons' <- (Con -> q [DCon]) -> [Con] -> q [DCon]
forall (monad :: * -> *) monoid (t :: * -> *) a.
(Monad monad, Monoid monoid, Traversable t) =>
(a -> monad monoid) -> t a -> monad monoid
concatMapM ([DTyVarBndr] -> DType -> Con -> q [DCon]
forall (q :: * -> *).
DsMonad q =>
[DTyVarBndr] -> DType -> Con -> q [DCon]
dsCon [DTyVarBndr]
tvbs' DType
data_ty) [Con]
cons
  DType
kind <- DType -> q DType
forall (m :: * -> *). MonadFail m => DType -> m DType
promoteType (DType -> [DTyVarBndr] -> DType
foldTypeTvbs (Name -> DType
DConT Name
name) [DTyVarBndr]
tvbs')
  [DDec]
inst_decs <- DType -> [DCon] -> q [DDec]
forall (q :: * -> *). OptionsMonad q => DType -> [DCon] -> q [DDec]
mkEqTypeInstance DType
kind [DCon]
cons'
  [Dec] -> q [Dec]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Dec] -> q [Dec]) -> [Dec] -> q [Dec]
forall a b. (a -> b) -> a -> b
$ [DDec] -> [Dec]
decsToTH [DDec]
inst_decs

promoteInstance :: OptionsMonad q => DerivDesc q -> String -> Name -> q [Dec]
promoteInstance :: DerivDesc q -> String -> Name -> q [Dec]
promoteInstance DerivDesc q
mk_inst String
class_name Name
name = do
  ([TyVarBndr]
tvbs, [Con]
cons) <- String -> Name -> q ([TyVarBndr], [Con])
forall (q :: * -> *).
DsMonad q =>
String -> Name -> q ([TyVarBndr], [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
  [DTyVarBndr]
tvbs' <- (TyVarBndr -> q DTyVarBndr) -> [TyVarBndr] -> q [DTyVarBndr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM TyVarBndr -> q DTyVarBndr
forall (q :: * -> *). DsMonad q => TyVarBndr -> q DTyVarBndr
dsTvb [TyVarBndr]
tvbs
  let data_ty :: DType
data_ty   = DType -> [DTyVarBndr] -> DType
foldTypeTvbs (Name -> DType
DConT Name
name) [DTyVarBndr]
tvbs'
  [DCon]
cons' <- (Con -> q [DCon]) -> [Con] -> q [DCon]
forall (monad :: * -> *) monoid (t :: * -> *) a.
(Monad monad, Monoid monoid, Traversable t) =>
(a -> monad monoid) -> t a -> monad monoid
concatMapM ([DTyVarBndr] -> DType -> Con -> q [DCon]
forall (q :: * -> *).
DsMonad q =>
[DTyVarBndr] -> DType -> Con -> q [DCon]
dsCon [DTyVarBndr]
tvbs' DType
data_ty) [Con]
cons
  let data_decl :: DataDecl
data_decl = Name -> [DTyVarBndr] -> [DCon] -> DataDecl
DataDecl Name
name [DTyVarBndr]
tvbs' [DCon]
cons'
  UInstDecl
raw_inst <- DerivDesc q
mk_inst Maybe DCxt
forall a. Maybe a
Nothing DType
data_ty DataDecl
data_decl
  [DDec]
decs <- [Dec] -> PrM () -> q [DDec]
forall (q :: * -> *). OptionsMonad q => [Dec] -> PrM () -> q [DDec]
promoteM_ [] (PrM () -> q [DDec]) -> PrM () -> q [DDec]
forall a b. (a -> b) -> a -> b
$ PrM AInstDecl -> PrM ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (PrM AInstDecl -> PrM ()) -> PrM AInstDecl -> PrM ()
forall a b. (a -> b) -> a -> b
$
          OMap Name DType
-> Map Name [DTyVarBndr] -> UInstDecl -> PrM AInstDecl
promoteInstanceDec OMap Name DType
forall k v. OMap k v
OMap.empty Map Name [DTyVarBndr]
forall k a. Map k a
Map.empty UInstDecl
raw_inst
  [Dec] -> q [Dec]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Dec] -> q [Dec]) -> [Dec] -> q [Dec]
forall a b. (a -> b) -> a -> b
$ [DDec] -> [Dec]
decsToTH [DDec]
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 (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 (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Promotion of individual values not supported"
promoteInfo (DTyVarI Name
_name DType
_ty) =
  String -> PrM ()
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Promotion of individual type variables not supported"
promoteInfo (DPatSynI {}) =
  String -> PrM ()
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Promotion of pattern synonyms not supported"

-- Note [Promoting declarations in two stages]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
--
-- It is necessary to know the types of things when promoting. So,
-- we promote in two stages: first, we build a LetDecEnv, which allows
-- for easy lookup. Then, we go through the actual elements of the LetDecEnv,
-- performing the promotion.
--
-- Why do we need the types? For kind annotations on the type family. We also
-- need to have both the types and the actual function definition at the same
-- time, because the function definition tells us how many patterns are
-- matched. Note that an eta-contracted function needs to return a TyFun,
-- not a proper type-level function.
--
-- Consider this example:
--
--   foo :: Nat -> Bool -> Bool
--   foo Zero = id
--   foo _    = not
--
-- Here the first parameter to foo is non-uniform, because it is
-- inspected in a pattern and can be different in each defining
-- equation of foo. The second parameter to foo, specified in the type
-- signature as Bool, is a uniform parameter - it is not inspected and
-- each defining equation of foo uses it the same way. The foo
-- function will be promoted to a type familty Foo like this:
--
--   type family Foo (n :: Nat) :: Bool ~> Bool where
--      Foo Zero = Id
--      Foo a    = Not
--
-- To generate type signature for Foo type family we must first learn
-- what is the actual number of patterns used in defining cequations
-- of foo. In this case there is only one so we declare Foo to take
-- one argument and have return type of Bool -> Bool.

-- Promote a list of top-level declarations.
promoteDecs :: [DDec] -> PrM ()
promoteDecs :: [DDec] -> PrM ()
promoteDecs [DDec]
raw_decls = do
  [DDec]
decls <- [DDec] -> PrM [DDec]
forall (q :: * -> *) a. (DsMonad q, Data a) => a -> q a
expand [DDec]
raw_decls     -- expand type synonyms
  [DDec] -> PrM ()
forall (q :: * -> *). Quasi q => [DDec] -> q ()
checkForRepInDecls [DDec]
decls
  PDecs { pd_let_decs :: PartitionedDecs -> [DLetDec]
pd_let_decs                = [DLetDec]
let_decs
        , pd_class_decs :: PartitionedDecs -> [UClassDecl]
pd_class_decs              = [UClassDecl]
classes
        , pd_instance_decs :: PartitionedDecs -> [UInstDecl]
pd_instance_decs           = [UInstDecl]
insts
        , pd_data_decs :: PartitionedDecs -> [DataDecl]
pd_data_decs               = [DataDecl]
datas
        , pd_ty_syn_decs :: PartitionedDecs -> [TySynDecl]
pd_ty_syn_decs             = [TySynDecl]
ty_syns
        , pd_open_type_family_decs :: PartitionedDecs -> [OpenTypeFamilyDecl]
pd_open_type_family_decs   = [OpenTypeFamilyDecl]
o_tyfams
        , pd_closed_type_family_decs :: PartitionedDecs -> [ClosedTypeFamilyDecl]
pd_closed_type_family_decs = [ClosedTypeFamilyDecl]
c_tyfams
        , pd_derived_eq_decs :: PartitionedDecs -> [DerivedEqDecl]
pd_derived_eq_decs         = [DerivedEqDecl]
derived_eq_decs } <- [DDec] -> PrM PartitionedDecs
forall (m :: * -> *). OptionsMonad m => [DDec] -> m PartitionedDecs
partitionDecs [DDec]
decls

  [TySynDecl]
-> [ClosedTypeFamilyDecl] -> [OpenTypeFamilyDecl] -> PrM ()
defunTopLevelTypeDecls [TySynDecl]
ty_syns [ClosedTypeFamilyDecl]
c_tyfams [OpenTypeFamilyDecl]
o_tyfams
  [DLetDec]
rec_sel_let_decs <- [DataDecl] -> PrM [DLetDec]
promoteDataDecs [DataDecl]
datas
    -- promoteLetDecs returns LetBinds, which we don't need at top level
  ([LetBind], ALetDecEnv)
_ <- Maybe Uniq -> [DLetDec] -> PrM ([LetBind], ALetDecEnv)
promoteLetDecs Maybe Uniq
forall a. Maybe a
Nothing ([DLetDec] -> PrM ([LetBind], ALetDecEnv))
-> [DLetDec] -> PrM ([LetBind], ALetDecEnv)
forall a b. (a -> b) -> a -> b
$ [DLetDec]
rec_sel_let_decs [DLetDec] -> [DLetDec] -> [DLetDec]
forall a. [a] -> [a] -> [a]
++ [DLetDec]
let_decs
  (UClassDecl -> PrM AClassDecl) -> [UClassDecl] -> PrM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ UClassDecl -> PrM AClassDecl
promoteClassDec [UClassDecl]
classes
  let orig_meth_sigs :: OMap Name DType
orig_meth_sigs = (UClassDecl -> OMap Name DType) -> [UClassDecl] -> OMap Name DType
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 :: Map Name [DTyVarBndr]
cls_tvbs_map   = [(Name, [DTyVarBndr])] -> Map Name [DTyVarBndr]
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Name, [DTyVarBndr])] -> Map Name [DTyVarBndr])
-> [(Name, [DTyVarBndr])] -> Map Name [DTyVarBndr]
forall a b. (a -> b) -> a -> b
$ (UClassDecl -> (Name, [DTyVarBndr]))
-> [UClassDecl] -> [(Name, [DTyVarBndr])]
forall a b. (a -> b) -> [a] -> [b]
map (\UClassDecl
cd -> (UClassDecl -> Name
forall (ann :: AnnotationFlag). ClassDecl ann -> Name
cd_name UClassDecl
cd, UClassDecl -> [DTyVarBndr]
forall (ann :: AnnotationFlag). ClassDecl ann -> [DTyVarBndr]
cd_tvbs UClassDecl
cd)) [UClassDecl]
classes
  (UInstDecl -> PrM AInstDecl) -> [UInstDecl] -> PrM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (OMap Name DType
-> Map Name [DTyVarBndr] -> UInstDecl -> PrM AInstDecl
promoteInstanceDec OMap Name DType
orig_meth_sigs Map Name [DTyVarBndr]
cls_tvbs_map) [UInstDecl]
insts
  (DerivedEqDecl -> PrM ()) -> [DerivedEqDecl] -> PrM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ DerivedEqDecl -> PrM ()
promoteDerivedEqDec   [DerivedEqDecl]
derived_eq_decs

-- curious about ALetDecEnv? See the LetDecEnv module for an explanation.
promoteLetDecs :: Maybe Uniq -- let-binding unique (if locally bound)
               -> [DLetDec] -> PrM ([LetBind], ALetDecEnv)
  -- See Note [Promoting declarations in two stages]
promoteLetDecs :: Maybe Uniq -> [DLetDec] -> PrM ([LetBind], ALetDecEnv)
promoteLetDecs Maybe Uniq
mb_let_uniq [DLetDec]
decls = do
  Options
opts <- PrM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  LetDecEnv Unannotated
let_dec_env <- [DLetDec] -> PrM (LetDecEnv Unannotated)
forall (q :: * -> *).
Quasi q =>
[DLetDec] -> q (LetDecEnv Unannotated)
buildLetDecEnv [DLetDec]
decls
  [Name]
all_locals <- PrM [Name]
forall (m :: * -> *). MonadReader PrEnv m => m [Name]
allLocals
  let binds :: [LetBind]
binds = [ (Name
name, DType -> DCxt -> DType
foldType (Name -> DType
DConT Name
sym) ((Name -> DType) -> [Name] -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map Name -> DType
DVarT [Name]
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 proName :: Name
proName = Options -> Name -> Maybe Uniq -> Name
promotedValueName Options
opts Name
name Maybe Uniq
mb_let_uniq
                    sym :: Name
sym = Options -> Name -> Int -> Name
defunctionalizedName Options
opts Name
proName ([Name] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
all_locals) ]
  ([DDec]
decs, ALetDecEnv
let_dec_env') <- [LetBind] -> PrM ([DDec], ALetDecEnv) -> PrM ([DDec], ALetDecEnv)
forall a. [LetBind] -> PrM a -> PrM a
letBind [LetBind]
binds (PrM ([DDec], ALetDecEnv) -> PrM ([DDec], ALetDecEnv))
-> PrM ([DDec], ALetDecEnv) -> PrM ([DDec], ALetDecEnv)
forall a b. (a -> b) -> a -> b
$ Maybe Uniq -> LetDecEnv Unannotated -> PrM ([DDec], ALetDecEnv)
promoteLetDecEnv Maybe Uniq
mb_let_uniq LetDecEnv Unannotated
let_dec_env
  [DDec] -> PrM ()
forall (m :: * -> *). MonadWriter [DDec] m => [DDec] -> m ()
emitDecs [DDec]
decs
  ([LetBind], ALetDecEnv) -> PrM ([LetBind], ALetDecEnv)
forall (m :: * -> *) a. Monad m => a -> m a
return ([LetBind]
binds, ALetDecEnv
let_dec_env' { lde_proms :: IfAnn Annotated (OMap Name DType) ()
lde_proms = [LetBind] -> OMap Name DType
forall k v. Ord k => [(k, v)] -> OMap k v
OMap.fromList [LetBind]
binds })

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.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 and record selectors] in D.S.Single.Data.
promoteDataDec :: DataDecl -> PrM [DLetDec]
promoteDataDec :: DataDecl -> PrM [DLetDec]
promoteDataDec (DataDecl Name
data_name [DTyVarBndr]
tvbs [DCon]
ctors) = do
  let arg_ty :: DType
arg_ty        = DType -> [DTyVarBndr] -> DType
foldTypeTvbs (Name -> DType
DConT Name
data_name) [DTyVarBndr]
tvbs
      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!
  [DLetDec]
rec_sel_let_decs <- DType -> [DCon] -> PrM [DLetDec]
forall (q :: * -> *). DsMonad q => DType -> [DCon] -> q [DLetDec]
getRecordSelectors DType
arg_ty [DCon]
ctors
  [DDec]
ctorSyms         <- [DCon] -> PrM [DDec]
buildDefunSymsDataD [DCon]
ctors
  [DDec]
infix_decs       <- [Name] -> PrM [DDec]
forall (q :: * -> *). OptionsMonad q => [Name] -> q [DDec]
promoteReifiedInfixDecls [Name]
rec_sel_names
  [DDec] -> PrM ()
forall (m :: * -> *). MonadWriter [DDec] m => [DDec] -> m ()
emitDecs ([DDec] -> PrM ()) -> [DDec] -> PrM ()
forall a b. (a -> b) -> a -> b
$ [DDec]
ctorSyms [DDec] -> [DDec] -> [DDec]
forall a. [a] -> [a] -> [a]
++ [DDec]
infix_decs
  [DLetDec] -> PrM [DLetDec]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [DLetDec]
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 -> [DTyVarBndr]
cd_tvbs = [DTyVarBndr]
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
lde_infix = OMap Name Fixity
infix_decls } }) = do
  Options
opts <- PrM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  let pClsName :: Name
pClsName = Options -> Name -> Name
promotedClassName Options
opts Name
cls_name
  OSet Name -> PrM AClassDecl -> PrM AClassDecl
forall a. OSet Name -> PrM a -> PrM a
forallBind OSet Name
cls_kvs_to_bind (PrM AClassDecl -> PrM AClassDecl)
-> PrM AClassDecl -> PrM AClassDecl
forall a b. (a -> b) -> a -> b
$ do
    let meth_sigs_list :: [LetBind]
meth_sigs_list = OMap Name DType -> [LetBind]
forall k v. OMap k v -> [(k, v)]
OMap.assocs OMap Name DType
meth_sigs
        meth_names :: [Name]
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 :: [(Name, LetDecRHS Unannotated)]
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]
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
    Maybe DType
mb_cls_sak <- Name -> PrM (Maybe DType)
forall (q :: * -> *). DsMonad q => Name -> q (Maybe DType)
dsReifyType Name
cls_name
    [DDec]
sig_decs <- (LetBind -> PrM DDec) -> [LetBind] -> PrM [DDec]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((Name -> DType -> PrM DDec) -> LetBind -> PrM DDec
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Name -> DType -> PrM DDec
promote_sig) [LetBind]
meth_sigs_list
    ([DDec]
default_decs, [ALetDecRHS]
ann_rhss, DCxt
prom_rhss)
      <- ((Name, LetDecRHS Unannotated) -> PrM (DDec, ALetDecRHS, DType))
-> [(Name, LetDecRHS Unannotated)]
-> PrM ([DDec], [ALetDecRHS], DCxt)
forall (m :: * -> *) a b c d.
Monad m =>
(a -> m (b, c, d)) -> [a] -> m ([b], [c], [d])
mapAndUnzip3M (MethodSort
-> OMap Name DType
-> (Name, LetDecRHS Unannotated)
-> PrM (DDec, ALetDecRHS, DType)
promoteMethod MethodSort
DefaultMethods OMap Name DType
meth_sigs) [(Name, LetDecRHS Unannotated)]
defaults_list
    [DTyVarBndr] -> [OpenTypeFamilyDecl] -> PrM ()
defunAssociatedTypeFamilies [DTyVarBndr]
tvbs [OpenTypeFamilyDecl]
atfs

    [DDec]
infix_decls' <- ((Name, Fixity) -> PrM (Maybe DDec))
-> [(Name, Fixity)] -> PrM [DDec]
forall (m :: * -> *) a b.
Monad m =>
(a -> m (Maybe b)) -> [a] -> m [b]
mapMaybeM ((Name -> Fixity -> PrM (Maybe DDec))
-> (Name, Fixity) -> PrM (Maybe DDec)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Maybe Uniq -> Name -> Fixity -> PrM (Maybe DDec)
forall (q :: * -> *).
OptionsMonad q =>
Maybe Uniq -> Name -> Fixity -> q (Maybe DDec)
promoteInfixDecl Maybe Uniq
forall a. Maybe a
Nothing)) ([(Name, Fixity)] -> PrM [DDec]) -> [(Name, Fixity)] -> PrM [DDec]
forall a b. (a -> b) -> a -> b
$
                    OMap Name Fixity -> [(Name, Fixity)]
forall k v. OMap k v -> [(k, v)]
OMap.assocs OMap Name Fixity
infix_decls
    [DDec]
cls_infix_decls <- [Name] -> PrM [DDec]
forall (q :: * -> *). OptionsMonad q => [Name] -> q [DDec]
promoteReifiedInfixDecls ([Name] -> PrM [DDec]) -> [Name] -> PrM [DDec]
forall a b. (a -> b) -> a -> b
$ Name
cls_nameName -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:[Name]
meth_names

    -- no need to do anything to the fundeps. They work as is!
    let pro_cls_dec :: DDec
pro_cls_dec = DCxt -> Name -> [DTyVarBndr] -> [FunDep] -> [DDec] -> DDec
DClassD [] Name
pClsName [DTyVarBndr]
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 :: Maybe DDec
mb_pro_cls_sak = (DType -> DDec) -> Maybe DType -> Maybe DDec
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name -> DType -> DDec
DKiSigD Name
pClsName) Maybe DType
mb_cls_sak
    [DDec] -> PrM ()
forall (m :: * -> *). MonadWriter [DDec] m => [DDec] -> m ()
emitDecs ([DDec] -> PrM ()) -> [DDec] -> PrM ()
forall a b. (a -> b) -> a -> b
$ Maybe DDec -> [DDec]
forall a. Maybe a -> [a]
maybeToList Maybe DDec
mb_pro_cls_sak [DDec] -> [DDec] -> [DDec]
forall a. [a] -> [a] -> [a]
++ DDec
pro_cls_decDDec -> [DDec] -> [DDec]
forall a. a -> [a] -> [a]
:[DDec]
cls_infix_decls
    let defaults_list' :: [(Name, ALetDecRHS)]
defaults_list'   = [Name] -> [ALetDecRHS] -> [(Name, ALetDecRHS)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
defaults_names [ALetDecRHS]
ann_rhss
        proms :: [LetBind]
proms            = [Name] -> DCxt -> [LetBind]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
defaults_names DCxt
prom_rhss
        cls_kvs_to_bind' :: OMap Name (OSet Name)
cls_kvs_to_bind' = OSet Name
cls_kvs_to_bind OSet Name -> OMap Name DType -> OMap Name (OSet Name)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ OMap Name DType
meth_sigs
    AClassDecl -> PrM AClassDecl
forall (m :: * -> *) a. Monad m => a -> m a
return (UClassDecl
decl { cd_lde :: ALetDecEnv
cd_lde = LetDecEnv Unannotated
lde { 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)]
defaults_list'
                                , lde_proms :: IfAnn Annotated (OMap Name DType) ()
lde_proms     = [LetBind] -> OMap Name DType
forall k v. Ord k => [(k, v)] -> OMap k v
OMap.fromList [LetBind]
proms
                                , lde_bound_kvs :: IfAnn Annotated (OMap Name (OSet Name)) ()
lde_bound_kvs = OMap Name (OSet Name)
IfAnn Annotated (OMap Name (OSet Name)) ()
cls_kvs_to_bind' } })
  where
    cls_kvb_names, cls_tvb_names, cls_kvs_to_bind :: OSet Name
    cls_kvb_names :: OSet Name
cls_kvb_names   = (DTyVarBndr -> OSet Name) -> [DTyVarBndr] -> OSet Name
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ((DType -> OSet Name) -> Maybe DType -> OSet Name
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap DType -> OSet Name
fvDType (Maybe DType -> OSet Name)
-> (DTyVarBndr -> Maybe DType) -> DTyVarBndr -> OSet Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DTyVarBndr -> Maybe DType
extractTvbKind) [DTyVarBndr]
tvbs
    cls_tvb_names :: OSet Name
cls_tvb_names   = [Name] -> OSet Name
forall a. Ord a => [a] -> OSet a
OSet.fromList ([Name] -> OSet Name) -> [Name] -> OSet Name
forall a b. (a -> b) -> a -> b
$ (DTyVarBndr -> Name) -> [DTyVarBndr] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndr -> Name
extractTvbName [DTyVarBndr]
tvbs
    cls_kvs_to_bind :: OSet Name
cls_kvs_to_bind = OSet Name
cls_kvb_names OSet Name -> OSet Name -> OSet Name
forall a. Ord a => OSet a -> OSet a -> OSet a
`OSet.union` OSet Name
cls_tvb_names

    promote_sig :: Name -> DType -> PrM DDec
    promote_sig :: Name -> DType -> PrM DDec
promote_sig Name
name DType
ty = do
      Options
opts <- PrM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
      let proName :: Name
proName = Options -> Name -> Name
promotedTopLevelValueName Options
opts Name
name
      -- When computing the kind to use for the defunctionalization symbols,
      -- /don't/ use the type variable binders from the method's type...
      ([DTyVarBndr]
_, DCxt
argKs, DType
resK) <- DType -> PrM ([DTyVarBndr], DCxt, DType)
forall (m :: * -> *).
MonadFail m =>
DType -> m ([DTyVarBndr], DCxt, DType)
promoteUnraveled DType
ty
      [Name]
args <- (DType -> PrM Name) -> DCxt -> PrM [Name]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (PrM Name -> DType -> PrM Name
forall a b. a -> b -> a
const (PrM Name -> DType -> PrM Name) -> PrM Name -> DType -> PrM Name
forall a b. (a -> b) -> a -> b
$ String -> PrM Name
forall (m :: * -> *). Quasi m => String -> m Name
qNewName String
"arg") DCxt
argKs
      let proTvbs :: [DTyVarBndr]
proTvbs = (Name -> DType -> DTyVarBndr) -> [Name] -> DCxt -> [DTyVarBndr]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Name -> DType -> DTyVarBndr
DKindedTV [Name]
args DCxt
argKs
      -- ...instead, compute the type variable binders in a left-to-right order,
      -- since that is the same order that the promoted method's kind will use.
      -- See Note [Promoted class methods and kind variable ordering]
          meth_sak_tvbs :: [DTyVarBndr]
meth_sak_tvbs = DCxt -> [DTyVarBndr]
toposortTyVarsOf (DCxt -> [DTyVarBndr]) -> DCxt -> [DTyVarBndr]
forall a b. (a -> b) -> a -> b
$ DCxt
argKs DCxt -> DCxt -> DCxt
forall a. [a] -> [a] -> [a]
++ [DType
resK]
          meth_sak :: DType
meth_sak      = [DTyVarBndr] -> DCxt -> DCxt -> DType -> DType
ravelVanillaDType [DTyVarBndr]
meth_sak_tvbs [] DCxt
argKs DType
resK
      Maybe Fixity
m_fixity <- Name -> PrM (Maybe Fixity)
forall (q :: * -> *). DsMonad q => Name -> q (Maybe Fixity)
reifyFixityWithLocals Name
name
      PrM [DDec] -> PrM ()
forall (m :: * -> *). MonadWriter [DDec] m => m [DDec] -> m ()
emitDecsM (PrM [DDec] -> PrM ()) -> PrM [DDec] -> PrM ()
forall a b. (a -> b) -> a -> b
$ Name -> Maybe Fixity -> DefunKindInfo -> PrM [DDec]
defunctionalize Name
proName Maybe Fixity
m_fixity (DefunKindInfo -> PrM [DDec]) -> DefunKindInfo -> PrM [DDec]
forall a b. (a -> b) -> a -> b
$ DType -> DefunKindInfo
DefunSAK DType
meth_sak

      DDec -> PrM DDec
forall (m :: * -> *) a. Monad m => a -> m a
return (DDec -> PrM DDec) -> DDec -> PrM DDec
forall a b. (a -> b) -> a -> b
$ DTypeFamilyHead -> DDec
DOpenTypeFamilyD (Name
-> [DTyVarBndr]
-> DFamilyResultSig
-> Maybe InjectivityAnn
-> DTypeFamilyHead
DTypeFamilyHead Name
proName
                                                 [DTyVarBndr]
proTvbs
                                                 (DType -> DFamilyResultSig
DKindSig DType
resK)
                                                 Maybe InjectivityAnn
forall a. Maybe a
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

There is one potential hack we could use to rectify this:

  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.
-}

-- returns (unpromoted method name, ALetDecRHS) pairs
promoteInstanceDec :: OMap Name DType
                      -- Class method type signatures
                   -> Map Name [DTyVarBndr]
                      -- 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 [DTyVarBndr] -> UInstDecl -> PrM AInstDecl
promoteInstanceDec OMap Name DType
orig_meth_sigs Map Name [DTyVarBndr]
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
  Options
opts <- PrM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  [DTyVarBndr]
cls_tvbs <- PrM [DTyVarBndr]
lookup_cls_tvbs
  DCxt
inst_kis <- (DType -> PrM DType) -> DCxt -> PrM DCxt
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM DType -> PrM DType
forall (m :: * -> *). MonadFail m => DType -> m DType
promoteType DCxt
inst_tys
  let pClsName :: Name
pClsName      = Options -> Name -> Name
promotedClassName Options
opts Name
cls_name
      cls_tvb_names :: [Name]
cls_tvb_names = (DTyVarBndr -> Name) -> [DTyVarBndr] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndr -> Name
extractTvbName [DTyVarBndr]
cls_tvbs
      kvs_to_bind :: OSet Name
kvs_to_bind   = (DType -> OSet Name) -> DCxt -> OSet Name
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap DType -> OSet Name
fvDType DCxt
inst_kis
  OSet Name -> PrM AInstDecl -> PrM AInstDecl
forall a. OSet Name -> PrM a -> PrM a
forallBind OSet Name
kvs_to_bind (PrM AInstDecl -> PrM AInstDecl) -> PrM AInstDecl -> PrM AInstDecl
forall a b. (a -> b) -> a -> b
$ do
    let subst :: Map Name DType
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 :: MethodSort
meth_impl = OMap Name DType -> Map Name DType -> MethodSort
InstanceMethods OMap Name DType
inst_sigs Map Name DType
subst
    ([DDec]
meths', [ALetDecRHS]
ann_rhss, DCxt
_)
      <- ((Name, LetDecRHS Unannotated) -> PrM (DDec, ALetDecRHS, DType))
-> [(Name, LetDecRHS Unannotated)]
-> PrM ([DDec], [ALetDecRHS], DCxt)
forall (m :: * -> *) a b c d.
Monad m =>
(a -> m (b, c, d)) -> [a] -> m ([b], [c], [d])
mapAndUnzip3M (MethodSort
-> OMap Name DType
-> (Name, LetDecRHS Unannotated)
-> PrM (DDec, ALetDecRHS, DType)
promoteMethod MethodSort
meth_impl OMap Name DType
orig_meth_sigs) [(Name, LetDecRHS Unannotated)]
meths
    [DDec] -> PrM ()
forall (m :: * -> *). MonadWriter [DDec] m => [DDec] -> m ()
emitDecs [Maybe Overlap
-> Maybe [DTyVarBndr] -> DCxt -> DType -> [DDec] -> DDec
DInstanceD Maybe Overlap
forall a. Maybe a
Nothing Maybe [DTyVarBndr]
forall a. Maybe a
Nothing [] (DType -> DCxt -> DType
foldType (Name -> DType
DConT Name
pClsName)
                                              DCxt
inst_kis) [DDec]
meths']
    AInstDecl -> PrM AInstDecl
forall (m :: * -> *) a. Monad m => a -> m a
return (UInstDecl
decl { id_meths :: [(Name, ALetDecRHS)]
id_meths = [Name] -> [ALetDecRHS] -> [(Name, ALetDecRHS)]
forall a b. [a] -> [b] -> [(a, b)]
zip (((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)]
meths) [ALetDecRHS]
ann_rhss })
  where
    lookup_cls_tvbs :: PrM [DTyVarBndr]
    lookup_cls_tvbs :: PrM [DTyVarBndr]
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 [DTyVarBndr] -> Maybe [DTyVarBndr]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
cls_name Map Name [DTyVarBndr]
cls_tvbs_map of
        Just [DTyVarBndr]
tvbs -> [DTyVarBndr] -> PrM [DTyVarBndr]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [DTyVarBndr]
tvbs
        Maybe [DTyVarBndr]
Nothing   -> PrM [DTyVarBndr]
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 [DTyVarBndr]
    reify_cls_tvbs :: PrM [DTyVarBndr]
reify_cls_tvbs = do
      Options
opts <- PrM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
      let pClsName :: Name
pClsName = Options -> Name -> Name
promotedClassName Options
opts Name
cls_name
          mk_tvbs :: MaybeT PrM [DTyVarBndr]
mk_tvbs  = PrM (Maybe DInfo) -> MaybeT PrM [DTyVarBndr]
extract_tvbs (Name -> PrM (Maybe DInfo)
forall (q :: * -> *). DsMonad q => Name -> q (Maybe DInfo)
dsReifyTypeNameInfo Name
pClsName)
                 MaybeT PrM [DTyVarBndr]
-> MaybeT PrM [DTyVarBndr] -> MaybeT PrM [DTyVarBndr]
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> PrM (Maybe DInfo) -> MaybeT PrM [DTyVarBndr]
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]
      Maybe [DTyVarBndr]
mb_tvbs <- MaybeT PrM [DTyVarBndr] -> PrM (Maybe [DTyVarBndr])
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT MaybeT PrM [DTyVarBndr]
mk_tvbs
      case Maybe [DTyVarBndr]
mb_tvbs of
        Just [DTyVarBndr]
tvbs -> [DTyVarBndr] -> PrM [DTyVarBndr]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [DTyVarBndr]
tvbs
        Maybe [DTyVarBndr]
Nothing -> String -> PrM [DTyVarBndr]
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> PrM [DTyVarBndr]) -> String -> PrM [DTyVarBndr]
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 [DTyVarBndr]
    extract_tvbs :: PrM (Maybe DInfo) -> MaybeT PrM [DTyVarBndr]
extract_tvbs PrM (Maybe DInfo)
reify_info = do
      Maybe DInfo
mb_info <- PrM (Maybe DInfo) -> MaybeT PrM (Maybe DInfo)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift PrM (Maybe DInfo)
reify_info
      case Maybe DInfo
mb_info of
        Just (DTyConI (DClassD DCxt
_ Name
_ [DTyVarBndr]
tvbs [FunDep]
_ [DDec]
_) Maybe [DDec]
_) -> [DTyVarBndr] -> MaybeT PrM [DTyVarBndr]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [DTyVarBndr]
tvbs
        Maybe DInfo
_                                       -> MaybeT PrM [DTyVarBndr]
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 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
showList :: [MethodSort] -> String -> String
$cshowList :: [MethodSort] -> String -> String
show :: MethodSort -> String
$cshow :: MethodSort -> String
showsPrec :: Int -> MethodSort -> String -> String
$cshowsPrec :: Int -> MethodSort -> String -> String
Show

promoteMethod :: MethodSort
              -> OMap Name DType    -- method types
              -> (Name, ULetDecRHS)
              -> PrM (DDec, ALetDecRHS, DType)
                 -- returns (type instance, ALetDecRHS, promoted RHS)
promoteMethod :: MethodSort
-> OMap Name DType
-> (Name, LetDecRHS Unannotated)
-> PrM (DDec, ALetDecRHS, DType)
promoteMethod MethodSort
meth_sort OMap Name DType
orig_sigs_map (Name
meth_name, LetDecRHS Unannotated
meth_rhs) = do
  Options
opts <- PrM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  ([DTyVarBndr]
meth_tvbs, DCxt
meth_arg_kis, DType
meth_res_ki) <- PrM ([DTyVarBndr], DCxt, DType)
promote_meth_ty
  [Name]
meth_arg_tvs <- Int -> PrM Name -> PrM [Name]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM (DCxt -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length DCxt
meth_arg_kis) (String -> PrM Name
forall (m :: * -> *). Quasi m => String -> m Name
qNewName String
"a")
  let proName :: Name
proName = Options -> Name -> Name
promotedTopLevelValueName Options
opts Name
meth_name
      helperNameBase :: String
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 :: DCxt
family_args = (Name -> DType) -> [Name] -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map Name -> DType
DVarT [Name]
meth_arg_tvs
  Name
helperName <- String -> PrM Name
forall (m :: * -> *). Quasi m => String -> m Name
newUniqueName String
helperNameBase
  let helperDefunName :: Name
helperDefunName = Options -> Name -> Name
defunctionalizedName0 Options
opts Name
helperName
  ([DDec]
pro_decs, [DDec]
defun_decs, ALetDecRHS
ann_rhs)
    <- LetDecRHSSort
-> OMap Name DType
-> OMap Name Fixity
-> Maybe Uniq
-> Name
-> LetDecRHS Unannotated
-> PrM ([DDec], [DDec], ALetDecRHS)
promoteLetDecRHS ([DTyVarBndr] -> DCxt -> DType -> LetDecRHSSort
ClassMethodRHS [DTyVarBndr]
meth_tvbs DCxt
meth_arg_kis DType
meth_res_ki)
                        OMap Name DType
forall k v. OMap k v
OMap.empty OMap Name Fixity
forall k v. OMap k v
OMap.empty
                        Maybe Uniq
forall a. Maybe a
Nothing Name
helperName LetDecRHS Unannotated
meth_rhs
  [DDec] -> PrM ()
forall (m :: * -> *). MonadWriter [DDec] m => [DDec] -> m ()
emitDecs ([DDec]
pro_decs [DDec] -> [DDec] -> [DDec]
forall a. [a] -> [a] -> [a]
++ [DDec]
defun_decs)
  (DDec, ALetDecRHS, DType) -> PrM (DDec, ALetDecRHS, DType)
forall (m :: * -> *) a. Monad m => a -> m a
return ( DTySynEqn -> DDec
DTySynInstD
             (Maybe [DTyVarBndr] -> DType -> DType -> DTySynEqn
DTySynEqn Maybe [DTyVarBndr]
forall a. Maybe a
Nothing
                        (DType -> DCxt -> DType
foldType (Name -> DType
DConT Name
proName) DCxt
family_args)
                        (DType -> DCxt -> DType
foldApply (Name -> DType
DConT Name
helperDefunName) ((Name -> DType) -> [Name] -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map Name -> DType
DVarT [Name]
meth_arg_tvs)))
         , ALetDecRHS
ann_rhs
         , Name -> DType
DConT Name
helperDefunName )
  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.)
    promote_meth_ty :: PrM ([DTyVarBndr], [DKind], DKind)
    promote_meth_ty :: PrM ([DTyVarBndr], 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 ([DTyVarBndr], 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.
              DType -> PrM ([DTyVarBndr], DCxt, DType)
forall (m :: * -> *).
MonadFail m =>
DType -> m ([DTyVarBndr], DCxt, DType)
promoteUnraveled DType
ty
            Maybe DType
Nothing -> do
              -- We don't have an InstanceSig, so we must compute the kind to use
              -- ourselves.
              ([DTyVarBndr]
_, DCxt
arg_kis, DType
res_ki) <- PrM ([DTyVarBndr], DCxt, DType)
lookup_meth_ty
              -- Substitute for the class variables in the method's type.
              -- See Note [Promoted class method kinds]
              let arg_kis' :: DCxt
arg_kis' = (DType -> DType) -> DCxt -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map (Map Name DType -> DType -> DType
substKind Map Name DType
cls_subst) DCxt
arg_kis
                  res_ki' :: DType
res_ki'  = Map Name DType -> DType -> DType
substKind Map Name DType
cls_subst DType
res_ki
                  -- Compute the type variable binders in a left-to-right
                  -- order, since that is the same order that the promoted
                  -- method's kind will use.
                  -- See Note [Promoted class methods and kind variable ordering]
                  tvbs' :: [DTyVarBndr]
tvbs'    = DCxt -> [DTyVarBndr]
toposortTyVarsOf (DCxt
arg_kis' DCxt -> DCxt -> DCxt
forall a. [a] -> [a] -> [a]
++ [DType
res_ki'])
              ([DTyVarBndr], DCxt, DType) -> PrM ([DTyVarBndr], DCxt, DType)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([DTyVarBndr]
tvbs', DCxt
arg_kis', DType
res_ki')

    -- Attempt to look up a class method's original type.
    lookup_meth_ty :: PrM ([DTyVarBndr], [DKind], DKind)
    lookup_meth_ty :: PrM ([DTyVarBndr], DCxt, DType)
lookup_meth_ty = do
      Options
opts <- PrM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
      let proName :: Name
proName = Options -> Name -> Name
promotedTopLevelValueName Options
opts Name
meth_name
      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
orig_sigs_map of
        Just DType
ty -> do
          -- The type of the method is in scope, so promote that.
          DType -> PrM ([DTyVarBndr], DCxt, DType)
forall (m :: * -> *).
MonadFail m =>
DType -> m ([DTyVarBndr], DCxt, DType)
promoteUnraveled DType
ty
        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.
          Maybe DInfo
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 Maybe DInfo
mb_info of
            Just (DTyConI (DOpenTypeFamilyD (DTypeFamilyHead Name
_ [DTyVarBndr]
tvbs DFamilyResultSig
mb_res_ki Maybe InjectivityAnn
_)) Maybe [DDec]
_)
              -> let arg_kis :: DCxt
arg_kis = (DTyVarBndr -> DType) -> [DTyVarBndr] -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map (Maybe DType -> DType
defaultMaybeToTypeKind (Maybe DType -> DType)
-> (DTyVarBndr -> Maybe DType) -> DTyVarBndr -> DType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DTyVarBndr -> Maybe DType
extractTvbKind) [DTyVarBndr]
tvbs
                     res_ki :: DType
res_ki  = Maybe DType -> DType
defaultMaybeToTypeKind (DFamilyResultSig -> Maybe DType
resultSigToMaybeKind DFamilyResultSig
mb_res_ki)
                     -- Compute the type variable binders in a left-to-right
                     -- order, since that is the same order that the promoted
                     -- method's kind will use.
                     -- See Note [Promoted class methods and kind variable ordering]
                     tvbs' :: [DTyVarBndr]
tvbs'   = DCxt -> [DTyVarBndr]
toposortTyVarsOf (DCxt
arg_kis DCxt -> DCxt -> DCxt
forall a. [a] -> [a] -> [a]
++ [DType
res_ki])
                  in ([DTyVarBndr], DCxt, DType) -> PrM ([DTyVarBndr], DCxt, DType)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([DTyVarBndr]
tvbs', DCxt
arg_kis, DType
res_ki)
            Maybe DInfo
_ -> String -> PrM ([DTyVarBndr], DCxt, DType)
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> PrM ([DTyVarBndr], DCxt, DType))
-> String -> PrM ([DTyVarBndr], 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
lde_infix = OMap Name Fixity
fix_env }) = do
  [DDec]
infix_decls <- ((Name, Fixity) -> PrM (Maybe DDec))
-> [(Name, Fixity)] -> PrM [DDec]
forall (m :: * -> *) a b.
Monad m =>
(a -> m (Maybe b)) -> [a] -> m [b]
mapMaybeM ((Name -> Fixity -> PrM (Maybe DDec))
-> (Name, Fixity) -> PrM (Maybe DDec)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Maybe Uniq -> Name -> Fixity -> PrM (Maybe DDec)
forall (q :: * -> *).
OptionsMonad q =>
Maybe Uniq -> Name -> Fixity -> q (Maybe DDec)
promoteInfixDecl Maybe Uniq
mb_let_uniq)) ([(Name, Fixity)] -> PrM [DDec]) -> [(Name, Fixity)] -> PrM [DDec]
forall a b. (a -> b) -> a -> b
$
                 OMap Name Fixity -> [(Name, Fixity)]
forall k v. OMap k v -> [(k, v)]
OMap.assocs OMap Name Fixity
fix_env

    -- promote all the declarations, producing annotated declarations
  let ([Name]
names, [LetDecRHS Unannotated]
rhss) = [(Name, LetDecRHS Unannotated)]
-> ([Name], [LetDecRHS Unannotated])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(Name, LetDecRHS Unannotated)]
 -> ([Name], [LetDecRHS Unannotated]))
-> [(Name, LetDecRHS Unannotated)]
-> ([Name], [LetDecRHS Unannotated])
forall a b. (a -> b) -> a -> b
$ OMap Name (LetDecRHS Unannotated)
-> [(Name, LetDecRHS Unannotated)]
forall k v. OMap k v -> [(k, v)]
OMap.assocs OMap Name (LetDecRHS Unannotated)
value_env
  ([[DDec]]
pro_decs, [[DDec]]
defun_decss, [ALetDecRHS]
ann_rhss)
    <- ([([DDec], [DDec], ALetDecRHS)]
 -> ([[DDec]], [[DDec]], [ALetDecRHS]))
-> PrM [([DDec], [DDec], ALetDecRHS)]
-> PrM ([[DDec]], [[DDec]], [ALetDecRHS])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [([DDec], [DDec], ALetDecRHS)]
-> ([[DDec]], [[DDec]], [ALetDecRHS])
forall a b c. [(a, b, c)] -> ([a], [b], [c])
unzip3 (PrM [([DDec], [DDec], ALetDecRHS)]
 -> PrM ([[DDec]], [[DDec]], [ALetDecRHS]))
-> PrM [([DDec], [DDec], ALetDecRHS)]
-> PrM ([[DDec]], [[DDec]], [ALetDecRHS])
forall a b. (a -> b) -> a -> b
$
       (Name -> LetDecRHS Unannotated -> PrM ([DDec], [DDec], ALetDecRHS))
-> [Name]
-> [LetDecRHS Unannotated]
-> PrM [([DDec], [DDec], ALetDecRHS)]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (LetDecRHSSort
-> OMap Name DType
-> OMap Name Fixity
-> Maybe Uniq
-> Name
-> LetDecRHS Unannotated
-> PrM ([DDec], [DDec], ALetDecRHS)
promoteLetDecRHS LetDecRHSSort
LetBindingRHS OMap Name DType
type_env OMap Name Fixity
fix_env Maybe Uniq
mb_let_uniq)
                [Name]
names [LetDecRHS Unannotated]
rhss

  [DDec] -> PrM ()
forall (m :: * -> *). MonadWriter [DDec] m => [DDec] -> m ()
emitDecs ([DDec] -> PrM ()) -> [DDec] -> PrM ()
forall a b. (a -> b) -> a -> b
$ [[DDec]] -> [DDec]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[DDec]]
defun_decss
  OSet Name
bound_kvs <- PrM (OSet Name)
allBoundKindVars
  let decs :: [DDec]
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' :: ALetDecEnv
let_dec_env' = LetDecEnv :: forall (ann :: AnnotationFlag).
OMap Name (LetDecRHS ann)
-> OMap Name DType
-> OMap Name Fixity
-> IfAnn ann (OMap Name DType) ()
-> IfAnn ann (OMap Name (OSet Name)) ()
-> LetDecEnv ann
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
lde_infix     = OMap Name Fixity
fix_env
                               , lde_proms :: IfAnn Annotated (OMap Name DType) ()
lde_proms     = IfAnn Annotated (OMap Name DType) ()
forall k v. OMap k v
OMap.empty  -- filled in promoteLetDecs
                               , lde_bound_kvs :: IfAnn Annotated (OMap Name (OSet Name)) ()
lde_bound_kvs = [(Name, OSet Name)] -> OMap Name (OSet Name)
forall k v. Ord k => [(k, v)] -> OMap k v
OMap.fromList ([(Name, OSet Name)] -> OMap Name (OSet Name))
-> [(Name, OSet Name)] -> OMap Name (OSet Name)
forall a b. (a -> b) -> a -> b
$ (Name -> (Name, OSet Name)) -> [Name] -> [(Name, OSet Name)]
forall a b. (a -> b) -> [a] -> [b]
map (, OSet Name
bound_kvs) [Name]
names }

  ([DDec], ALetDecEnv) -> PrM ([DDec], ALetDecEnv)
forall (m :: * -> *) a. Monad m => a -> m a
return ([DDec]
decs, ALetDecEnv
let_dec_env')

-- Promote a fixity declaration.
promoteInfixDecl :: forall q. OptionsMonad q
                 => Maybe Uniq -> Name -> Fixity -> q (Maybe DDec)
promoteInfixDecl :: Maybe Uniq -> Name -> Fixity -> q (Maybe DDec)
promoteInfixDecl Maybe Uniq
mb_let_uniq Name
name Fixity
fixity = do
  Options
opts  <- q Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  Maybe NameSpace
mb_ns <- Name -> q (Maybe NameSpace)
forall (q :: * -> *). DsMonad q => Name -> q (Maybe NameSpace)
reifyNameSpace Name
name
  case Maybe NameSpace
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 NameSpace
DataName  -> q (Maybe DDec)
never_mind
    Just NameSpace
TcClsName -> do
      Maybe DInfo
mb_info <- Name -> q (Maybe DInfo)
forall (q :: * -> *). DsMonad q => Name -> q (Maybe DInfo)
dsReify Name
name
      case Maybe DInfo
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.
    finish :: Name -> q (Maybe DDec)
    finish :: Name -> q (Maybe DDec)
finish = Maybe DDec -> q (Maybe DDec)
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 -> Name -> DLetDec
DInfixD Fixity
fixity

    -- Don't produce a fixity declaration at all. This happens when promoting a
    -- fixity declaration for a name whose promoted counterpart is the same as
    -- the original name.
    -- See Note [singletons and fixity declarations] in D.S.Single.Fixity, wrinkle 1.
    never_mind :: q (Maybe DDec)
    never_mind :: q (Maybe DDec)
never_mind = Maybe DDec -> q (Maybe DDec)
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
    -- 'genQuotedDecs' is set to 'True', since that will run the risk of
    -- generating duplicate fixity declarations.
    -- See Note [singletons and fixity declarations] in D.S.Single.Fixity, wrinkle 1.
    promote_val :: q (Maybe DDec)
    promote_val :: q (Maybe DDec)
promote_val = do
      Options
opts <- q Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
      let promoted_name :: Name
          promoted_name :: Name
promoted_name = Options -> Name -> Maybe Uniq -> Name
promotedValueName Options
opts Name
name Maybe Uniq
mb_let_uniq
      if Name -> String
nameBase Name
name String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> String
nameBase Name
promoted_name Bool -> Bool -> Bool
&& Options -> Bool
genQuotedDecs Options
opts
         then q (Maybe DDec)
never_mind
         else Name -> q (Maybe DDec)
finish Name
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 and fixity declarations] in D.S.Single.Fixity, wrinkle 2.
promoteReifiedInfixDecls :: forall q. OptionsMonad q => [Name] -> q [DDec]
promoteReifiedInfixDecls :: [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 (m :: * -> *) a. Quasi m => m a -> m a -> m a
qRecover (Maybe DDec -> q (Maybe DDec)
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
        Maybe Fixity
mFixity <- Name -> q (Maybe Fixity)
forall (m :: * -> *). Quasi m => Name -> m (Maybe Fixity)
qReifyFixity Name
name
        case Maybe Fixity
mFixity of
          Maybe Fixity
Nothing     -> Maybe DDec -> q (Maybe DDec)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe DDec
forall a. Maybe a
Nothing
          Just Fixity
fixity -> Maybe Uniq -> Name -> Fixity -> q (Maybe DDec)
forall (q :: * -> *).
OptionsMonad q =>
Maybe Uniq -> Name -> Fixity -> q (Maybe DDec)
promoteInfixDecl Maybe Uniq
forall a. Maybe a
Nothing Name
name Fixity
fixity

-- 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
      [DTyVarBndr] [DKind] DKind
      -- The RHS's promoted type variable binders, argument types, and
      -- result type. 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
showList :: [LetDecRHSSort] -> String -> String
$cshowList :: [LetDecRHSSort] -> String -> String
show :: LetDecRHSSort -> String
$cshow :: LetDecRHSSort -> String
showsPrec :: Int -> LetDecRHSSort -> String -> String
$cshowsPrec :: Int -> 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
  Options
opts <- PrM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  [Name]
all_locals <- PrM [Name]
forall (m :: * -> *). MonadReader PrEnv m => m [Name]
allLocals
  case LetDecRHS Unannotated
let_dec_rhs of
    UValue exp -> do
      (Maybe LetDecRHSKindInfo
m_ldrki, Int
ty_num_args) <- [Name] -> Int -> PrM (Maybe LetDecRHSKindInfo, Int)
promote_let_dec_ty [Name]
all_locals Int
0
      if Int
ty_num_args Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0
      then
        let proName :: Name
proName = Options -> Name -> Maybe Uniq -> Name
promotedValueName Options
opts Name
name Maybe Uniq
mb_let_uniq
            prom_fun_lhs :: DType
prom_fun_lhs = DType -> DCxt -> DType
foldType (Name -> DType
DConT Name
proName) (DCxt -> DType) -> DCxt -> DType
forall a b. (a -> b) -> a -> b
$ (Name -> DType) -> [Name] -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map Name -> DType
DVarT [Name]
all_locals in
        [Name]
-> Maybe LetDecRHSKindInfo
-> Int
-> PrM (DType, ADExp)
-> (DType -> [DTySynEqn])
-> (DType -> Int -> ADExp -> ALetDecRHS)
-> PrM ([DDec], [DDec], ALetDecRHS)
forall prom_a a.
[Name]
-> Maybe LetDecRHSKindInfo
-> Int
-> PrM (prom_a, a)
-> (prom_a -> [DTySynEqn])
-> (DType -> Int -> a -> ALetDecRHS)
-> PrM ([DDec], [DDec], ALetDecRHS)
promote_let_dec_rhs [Name]
all_locals Maybe LetDecRHSKindInfo
m_ldrki Int
0 (DExp -> PrM (DType, ADExp)
promoteExp DExp
exp)
                            (\DType
exp' -> [Maybe [DTyVarBndr] -> DType -> DType -> DTySynEqn
DTySynEqn Maybe [DTyVarBndr]
forall a. Maybe a
Nothing DType
prom_fun_lhs DType
exp'])
                            DType -> Int -> ADExp -> ALetDecRHS
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.
        [Name] -> [DClause] -> PrM ([DDec], [DDec], ALetDecRHS)
promote_function_rhs [Name]
all_locals [[DPat] -> DExp -> DClause
DClause [] DExp
exp]
    UFunction clauses -> [Name] -> [DClause] -> PrM ([DDec], [DDec], ALetDecRHS)
promote_function_rhs [Name]
all_locals [DClause]
clauses
  where
    -- Promote the RHS of a UFunction (or a UValue with a function type).
    promote_function_rhs :: [Name]
                         -> [DClause] -> PrM ([DDec], [DDec], ALetDecRHS)
    promote_function_rhs :: [Name] -> [DClause] -> PrM ([DDec], [DDec], ALetDecRHS)
promote_function_rhs [Name]
all_locals [DClause]
clauses = do
      Options
opts <- PrM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
      Int
numArgs <- [DClause] -> PrM Int
count_args [DClause]
clauses
      let proName :: Name
proName = Options -> Name -> Maybe Uniq -> Name
promotedValueName Options
opts Name
name Maybe Uniq
mb_let_uniq
          prom_fun_lhs :: DType
prom_fun_lhs = DType -> DCxt -> DType
foldType (Name -> DType
DConT Name
proName) (DCxt -> DType) -> DCxt -> DType
forall a b. (a -> b) -> a -> b
$ (Name -> DType) -> [Name] -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map Name -> DType
DVarT [Name]
all_locals
      (Maybe LetDecRHSKindInfo
m_ldrki, Int
ty_num_args) <- [Name] -> Int -> PrM (Maybe LetDecRHSKindInfo, Int)
promote_let_dec_ty [Name]
all_locals Int
numArgs
      [DClause]
expClauses <- (DClause -> PrM DClause) -> [DClause] -> PrM [DClause]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Int -> Int -> DClause -> PrM DClause
etaContractOrExpand Int
ty_num_args Int
numArgs) [DClause]
clauses
      [Name]
-> Maybe LetDecRHSKindInfo
-> Int
-> PrM ([DTySynEqn], [ADClause])
-> ([DTySynEqn] -> [DTySynEqn])
-> (DType -> Int -> [ADClause] -> ALetDecRHS)
-> PrM ([DDec], [DDec], ALetDecRHS)
forall prom_a a.
[Name]
-> Maybe LetDecRHSKindInfo
-> Int
-> PrM (prom_a, a)
-> (prom_a -> [DTySynEqn])
-> (DType -> Int -> a -> ALetDecRHS)
-> PrM ([DDec], [DDec], ALetDecRHS)
promote_let_dec_rhs [Name]
all_locals Maybe LetDecRHSKindInfo
m_ldrki Int
ty_num_args
                          ((DClause -> PrM (DTySynEqn, ADClause))
-> [DClause] -> PrM ([DTySynEqn], [ADClause])
forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM (DType -> DClause -> PrM (DTySynEqn, ADClause)
promoteClause DType
prom_fun_lhs) [DClause]
expClauses)
                          [DTySynEqn] -> [DTySynEqn]
forall a. a -> a
id DType -> Int -> [ADClause] -> ALetDecRHS
AFunction

    -- 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
      :: [Name]                            -- 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
      -> (DType -> Int -> a -> ALetDecRHS) -- Build an ALetDecRHS
      -> PrM ([DDec], [DDec], ALetDecRHS)
    promote_let_dec_rhs :: [Name]
-> Maybe LetDecRHSKindInfo
-> Int
-> PrM (prom_a, a)
-> (prom_a -> [DTySynEqn])
-> (DType -> Int -> a -> ALetDecRHS)
-> PrM ([DDec], [DDec], ALetDecRHS)
promote_let_dec_rhs [Name]
all_locals Maybe LetDecRHSKindInfo
m_ldrki Int
ty_num_args
                        PrM (prom_a, a)
promote_thing prom_a -> [DTySynEqn]
mk_prom_eqns DType -> Int -> a -> ALetDecRHS
mk_alet_dec_rhs = do
      Options
opts <- PrM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
      [Name]
tyvarNames <- Int -> PrM Name -> PrM [Name]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
ty_num_args (String -> PrM Name
forall (m :: * -> *). Quasi m => String -> m Name
qNewName String
"a")
      let proName :: Name
proName    = Options -> Name -> Maybe Uniq -> Name
promotedValueName Options
opts Name
name Maybe Uniq
mb_let_uniq
          local_tvbs :: [DTyVarBndr]
local_tvbs = (Name -> DTyVarBndr) -> [Name] -> [DTyVarBndr]
forall a b. (a -> b) -> [a] -> [b]
map Name -> DTyVarBndr
DPlainTV [Name]
all_locals
          m_fixity :: Maybe Fixity
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 :: [DTyVarBndr] -> DFamilyResultSig -> DTypeFamilyHead
          mk_tf_head :: [DTyVarBndr] -> DFamilyResultSig -> DTypeFamilyHead
mk_tf_head [DTyVarBndr]
tvbs DFamilyResultSig
res_sig = Name
-> [DTyVarBndr]
-> DFamilyResultSig
-> Maybe InjectivityAnn
-> DTypeFamilyHead
DTypeFamilyHead Name
proName [DTyVarBndr]
tvbs DFamilyResultSig
res_sig Maybe InjectivityAnn
forall a. Maybe a
Nothing

          (OSet Name
lde_kvs_to_bind, Maybe DDec
m_sak_dec, DefunKindInfo
defun_ki, DTypeFamilyHead
tf_head) =
              -- There are three possible cases:
            case Maybe LetDecRHSKindInfo
m_ldrki of
              -- 1. We have no kind information whatsoever.
              Maybe LetDecRHSKindInfo
Nothing ->
                let all_args :: [DTyVarBndr]
all_args = [DTyVarBndr]
local_tvbs [DTyVarBndr] -> [DTyVarBndr] -> [DTyVarBndr]
forall a. [a] -> [a] -> [a]
++ (Name -> DTyVarBndr) -> [Name] -> [DTyVarBndr]
forall a b. (a -> b) -> [a] -> [b]
map Name -> DTyVarBndr
DPlainTV [Name]
tyvarNames in
                ( OSet Name
forall a. OSet a
OSet.empty
                , Maybe DDec
forall a. Maybe a
Nothing
                , [DTyVarBndr] -> Maybe DType -> DefunKindInfo
DefunNoSAK [DTyVarBndr]
all_args Maybe DType
forall a. Maybe a
Nothing
                , [DTyVarBndr] -> DFamilyResultSig -> DTypeFamilyHead
mk_tf_head [DTyVarBndr]
all_args DFamilyResultSig
DNoSig
                )
              -- 2. We have some kind information in the form of a LetDecRHSKindInfo.
              Just (LDRKI Maybe DType
m_sak [DTyVarBndr]
tvbs DCxt
argKs DType
resK) ->
                let all_args :: [DTyVarBndr]
all_args         = [DTyVarBndr]
local_tvbs [DTyVarBndr] -> [DTyVarBndr] -> [DTyVarBndr]
forall a. [a] -> [a] -> [a]
++ (Name -> DType -> DTyVarBndr) -> [Name] -> DCxt -> [DTyVarBndr]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Name -> DType -> DTyVarBndr
DKindedTV [Name]
tyvarNames DCxt
argKs
                    lde_kvs_to_bind' :: OSet Name
lde_kvs_to_bind' = [Name] -> OSet Name
forall a. Ord a => [a] -> OSet a
OSet.fromList ((DTyVarBndr -> Name) -> [DTyVarBndr] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndr -> Name
extractTvbName [DTyVarBndr]
tvbs) in
                case Maybe DType
m_sak of
                  -- 2(a). We do not have a standalone kind signature.
                  Maybe DType
Nothing ->
                    ( OSet Name
lde_kvs_to_bind'
                    , Maybe DDec
forall a. Maybe a
Nothing
                    , [DTyVarBndr] -> Maybe DType -> DefunKindInfo
DefunNoSAK [DTyVarBndr]
all_args (DType -> Maybe DType
forall a. a -> Maybe a
Just DType
resK)
                    , [DTyVarBndr] -> DFamilyResultSig -> DTypeFamilyHead
mk_tf_head [DTyVarBndr]
all_args (DType -> DFamilyResultSig
DKindSig DType
resK)
                    )
                  -- 2(b). We have a standalone kind signature.
                  Just DType
sak ->
                    ( OSet Name
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
                      -- If the promoted type family has a standalone kind
                      -- signature, then there is no need to annotate the arguments
                      -- or result with explicit kinds. A standalone kind signature
                      -- accomplishes the same thing, but better.
                    , [DTyVarBndr] -> DFamilyResultSig -> DTypeFamilyHead
mk_tf_head ((DTyVarBndr -> DTyVarBndr) -> [DTyVarBndr] -> [DTyVarBndr]
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndr -> DTyVarBndr
dropTvbKind [DTyVarBndr]
all_args) DFamilyResultSig
DNoSig
                    )

      [DDec]
defun_decs <- Name -> Maybe Fixity -> DefunKindInfo -> PrM [DDec]
defunctionalize Name
proName Maybe Fixity
m_fixity DefunKindInfo
defun_ki
      (prom_a
prom_thing, a
thing) <- OSet Name -> PrM (prom_a, a) -> PrM (prom_a, a)
forall a. OSet Name -> PrM a -> PrM a
forallBind OSet Name
lde_kvs_to_bind PrM (prom_a, a)
promote_thing
      DType
prom_fun_rhs <- Name -> PrM DType
lookupVarE Name
name
      ([DDec], [DDec], ALetDecRHS) -> PrM ([DDec], [DDec], ALetDecRHS)
forall (m :: * -> *) a. Monad m => a -> m a
return ( [Maybe DDec] -> [DDec]
forall a. [Maybe a] -> [a]
catMaybes [ Maybe DDec
m_sak_dec
                         , DDec -> Maybe DDec
forall a. a -> Maybe a
Just (DDec -> Maybe DDec) -> DDec -> Maybe DDec
forall a b. (a -> b) -> a -> b
$ DTypeFamilyHead -> [DTySynEqn] -> DDec
DClosedTypeFamilyD DTypeFamilyHead
tf_head (prom_a -> [DTySynEqn]
mk_prom_eqns prom_a
prom_thing)
                         ]
             , [DDec]
defun_decs
             , DType -> Int -> a -> ALetDecRHS
mk_alet_dec_rhs DType
prom_fun_rhs Int
ty_num_args a
thing )

    promote_let_dec_ty :: [Name] -- 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 :: [Name] -> Int -> PrM (Maybe LetDecRHSKindInfo, Int)
promote_let_dec_ty [Name]
all_locals Int
default_num_args =
      case LetDecRHSSort
rhs_sort of
        ClassMethodRHS [DTyVarBndr]
tvbs DCxt
arg_kis DType
res_ki
          -> -- For class method RHS helper functions, don't bother quantifying
             -- any type variables in their SAKS. We could certainly try, but
             -- given that these functions are only used internally, there's no
             -- point in trying to get the order of type variables correct,
             -- since we don't apply these functions with visible kind
             -- applications.
             let sak :: DType
sak = [DTyVarBndr] -> DCxt -> DCxt -> DType -> DType
ravelVanillaDType [] [] DCxt
arg_kis DType
res_ki in
             (Maybe LetDecRHSKindInfo, Int)
-> PrM (Maybe LetDecRHSKindInfo, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (LetDecRHSKindInfo -> Maybe LetDecRHSKindInfo
forall a. a -> Maybe a
Just (Maybe DType -> [DTyVarBndr] -> DCxt -> DType -> LetDecRHSKindInfo
LDRKI (DType -> Maybe DType
forall a. a -> Maybe a
Just DType
sak) [DTyVarBndr]
tvbs DCxt
arg_kis DType
res_ki), DCxt -> 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.
          ([DTyVarBndr]
tvbs, DCxt
argKs, DType
resultK) <- DType -> PrM ([DTyVarBndr], DCxt, DType)
forall (m :: * -> *).
MonadFail m =>
DType -> m ([DTyVarBndr], DCxt, DType)
promoteUnraveled DType
ty
          let m_sak :: Maybe DType
m_sak | [Name] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Name]
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] -> DCxt -> DCxt -> DType -> DType
ravelVanillaDType [DTyVarBndr]
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
          -- invariant: count_args ty == length argKs
          (Maybe LetDecRHSKindInfo, Int)
-> PrM (Maybe LetDecRHSKindInfo, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (LetDecRHSKindInfo -> Maybe LetDecRHSKindInfo
forall a. a -> Maybe a
Just (Maybe DType -> [DTyVarBndr] -> DCxt -> DType -> LetDecRHSKindInfo
LDRKI Maybe DType
m_sak [DTyVarBndr]
tvbs DCxt
argKs DType
resultK), DCxt -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length DCxt
argKs)

          |  Bool
otherwise
          -> (Maybe LetDecRHSKindInfo, Int)
-> PrM (Maybe LetDecRHSKindInfo, Int)
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
          [Name]
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 :: [DPat]
newPats = (Name -> DPat) -> [Name] -> [DPat]
forall a b. (a -> b) -> [a] -> [b]
map Name -> DPat
DVarP [Name]
names
              newArgs :: [DExp]
newArgs = (Name -> DExp) -> [Name] -> [DExp]
forall a b. (a -> b) -> [a] -> [b]
map Name -> DExp
DVarE [Name]
names
          DClause -> PrM DClause
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]
pats [DPat] -> [DPat] -> [DPat]
forall a. [a] -> [a] -> [a]
++ [DPat]
newPats) (DExp -> [DExp] -> DExp
foldExp DExp
exp [DExp]
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
          DExp
lamExp <- [DPat] -> DExp -> PrM DExp
forall (q :: * -> *). DsMonad q => [DPat] -> DExp -> q DExp
mkDLamEFromDPats [DPat]
lamPats DExp
exp
          DClause -> PrM DClause
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 (m :: * -> *) a. Monad m => a -> m a
return (Int -> PrM Int) -> Int -> PrM Int
forall a b. (a -> b) -> a -> b
$ [DPat] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [DPat]
pats
    count_args [DClause]
_ = String -> PrM Int
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]
        [DTyVarBndr]  -- 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.
-}

promoteClause :: DType -- What to use as the LHS of the promoted type family
                       -- equation. This should consist of the promoted name of
                       -- the function to which the clause belongs, applied to
                       -- any local arguments (e.g., `Go x y z`).
              -> DClause -> PrM (DTySynEqn, ADClause)
promoteClause :: DType -> DClause -> PrM (DTySynEqn, ADClause)
promoteClause DType
pro_clause_fun (DClause [DPat]
pats DExp
exp) = do
  -- promoting the patterns creates variable bindings. These are passed
  -- to the function promoted the RHS
  ((DCxt
types, [ADPat]
pats'), PromDPatInfos
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
$ (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 DPat -> QWithAux PromDPatInfos PrM (DType, ADPat)
promotePat [DPat]
pats
  let PromDPatInfos { prom_dpat_vars :: PromDPatInfos -> VarPromotions
prom_dpat_vars    = VarPromotions
new_vars
                    , prom_dpat_sig_kvs :: PromDPatInfos -> OSet Name
prom_dpat_sig_kvs = OSet Name
sig_kvs } = PromDPatInfos
prom_pat_infos
  (DType
ty, ADExp
ann_exp) <- OSet Name -> PrM (DType, ADExp) -> PrM (DType, ADExp)
forall a. OSet Name -> PrM a -> PrM a
forallBind OSet Name
sig_kvs (PrM (DType, ADExp) -> PrM (DType, ADExp))
-> PrM (DType, ADExp) -> PrM (DType, ADExp)
forall a b. (a -> b) -> a -> b
$
                   VarPromotions -> PrM (DType, ADExp) -> PrM (DType, ADExp)
forall a. VarPromotions -> PrM a -> PrM a
lambdaBind VarPromotions
new_vars (PrM (DType, ADExp) -> PrM (DType, ADExp))
-> PrM (DType, ADExp) -> PrM (DType, ADExp)
forall a b. (a -> b) -> a -> b
$
                   DExp -> PrM (DType, ADExp)
promoteExp DExp
exp
  (DTySynEqn, ADClause) -> PrM (DTySynEqn, ADClause)
forall (m :: * -> *) a. Monad m => a -> m a
return ( Maybe [DTyVarBndr] -> DType -> DType -> DTySynEqn
DTySynEqn Maybe [DTyVarBndr]
forall a. Maybe a
Nothing (DType -> DCxt -> DType
foldType DType
pro_clause_fun DCxt
types) DType
ty
         , VarPromotions -> [ADPat] -> ADExp -> ADClause
ADClause VarPromotions
new_vars [ADPat]
pats' ADExp
ann_exp )

promoteMatch :: DType -- What to use as the LHS of the promoted type family
                      -- equation. This should consist of the promoted name of
                      -- the case expression to which the match belongs, applied
                      -- to any local arguments (e.g., `Case x y z`).
             -> DMatch -> PrM (DTySynEqn, ADMatch)
promoteMatch :: DType -> DMatch -> PrM (DTySynEqn, ADMatch)
promoteMatch DType
pro_case_fun (DMatch DPat
pat DExp
exp) = do
  -- promoting the patterns creates variable bindings. These are passed
  -- to the function promoted the RHS
  ((DType
ty, ADPat
pat'), PromDPatInfos
prom_pat_infos) <- QWithAux PromDPatInfos PrM (DType, ADPat)
-> PrM ((DType, ADPat), PromDPatInfos)
forall m (q :: * -> *) a. QWithAux m q a -> q (a, m)
evalForPair (QWithAux PromDPatInfos PrM (DType, ADPat)
 -> PrM ((DType, ADPat), PromDPatInfos))
-> QWithAux PromDPatInfos PrM (DType, ADPat)
-> PrM ((DType, ADPat), PromDPatInfos)
forall a b. (a -> b) -> a -> b
$ DPat -> QWithAux PromDPatInfos PrM (DType, ADPat)
promotePat DPat
pat
  let PromDPatInfos { prom_dpat_vars :: PromDPatInfos -> VarPromotions
prom_dpat_vars    = VarPromotions
new_vars
                    , prom_dpat_sig_kvs :: PromDPatInfos -> OSet Name
prom_dpat_sig_kvs = OSet Name
sig_kvs } = PromDPatInfos
prom_pat_infos
  (DType
rhs, ADExp
ann_exp) <- OSet Name -> PrM (DType, ADExp) -> PrM (DType, ADExp)
forall a. OSet Name -> PrM a -> PrM a
forallBind OSet Name
sig_kvs (PrM (DType, ADExp) -> PrM (DType, ADExp))
-> PrM (DType, ADExp) -> PrM (DType, ADExp)
forall a b. (a -> b) -> a -> b
$
                    VarPromotions -> PrM (DType, ADExp) -> PrM (DType, ADExp)
forall a. VarPromotions -> PrM a -> PrM a
lambdaBind VarPromotions
new_vars (PrM (DType, ADExp) -> PrM (DType, ADExp))
-> PrM (DType, ADExp) -> PrM (DType, ADExp)
forall a b. (a -> b) -> a -> b
$
                    DExp -> PrM (DType, ADExp)
promoteExp DExp
exp
  (DTySynEqn, ADMatch) -> PrM (DTySynEqn, ADMatch)
forall (m :: * -> *) a. Monad m => a -> m a
return ((DTySynEqn, ADMatch) -> PrM (DTySynEqn, ADMatch))
-> (DTySynEqn, ADMatch) -> PrM (DTySynEqn, ADMatch)
forall a b. (a -> b) -> a -> b
$ ( Maybe [DTyVarBndr] -> DType -> DType -> DTySynEqn
DTySynEqn Maybe [DTyVarBndr]
forall a. Maybe a
Nothing (DType
pro_case_fun DType -> DType -> DType
`DAppT` DType
ty) DType
rhs
           , VarPromotions -> ADPat -> ADExp -> ADMatch
ADMatch VarPromotions
new_vars ADPat
pat' ADExp
ann_exp)

-- promotes a term pattern into a type pattern, accumulating bound variable names
promotePat :: DPat -> QWithAux PromDPatInfos PrM (DType, ADPat)
promotePat :: DPat -> QWithAux PromDPatInfos PrM (DType, ADPat)
promotePat (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 (DVarP Name
name) = do
      -- term vars can be symbols... type vars can't!
  Name
tyName <- Name -> QWithAux PromDPatInfos PrM Name
forall (q :: * -> *). Quasi q => Name -> q Name
mkTyName Name
name
  PromDPatInfos -> QWithAux PromDPatInfos PrM ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (PromDPatInfos -> QWithAux PromDPatInfos PrM ())
-> PromDPatInfos -> QWithAux PromDPatInfos PrM ()
forall a b. (a -> b) -> a -> b
$ VarPromotions -> OSet Name -> PromDPatInfos
PromDPatInfos [(Name
name, Name
tyName)] OSet Name
forall a. OSet a
OSet.empty
  (DType, ADPat) -> QWithAux PromDPatInfos PrM (DType, ADPat)
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> DType
DVarT Name
tyName, Name -> ADPat
ADVarP Name
name)
promotePat (DConP Name
name [DPat]
pats) = do
  (DCxt
types, [ADPat]
pats') <- (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 DPat -> QWithAux PromDPatInfos PrM (DType, ADPat)
promotePat [DPat]
pats
  let name' :: Name
name' = Name -> Name
unboxed_tuple_to_tuple Name
name
  (DType, ADPat) -> QWithAux PromDPatInfos PrM (DType, ADPat)
forall (m :: * -> *) a. Monad m => a -> m a
return (DType -> DCxt -> DType
foldType (Name -> DType
DConT Name
name') DCxt
types, Name -> [ADPat] -> ADPat
ADConP Name
name [ADPat]
pats')
  where
    unboxed_tuple_to_tuple :: Name -> Name
unboxed_tuple_to_tuple Name
n
      | Just Int
deg <- Name -> Maybe Int
unboxedTupleNameDegree_maybe Name
n = Int -> Name
tupleDataName Int
deg
      | Bool
otherwise                                  = Name
n
promotePat (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 (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
<$> DPat -> QWithAux PromDPatInfos PrM (DType, ADPat)
promotePat DPat
pat
promotePat (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 (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
<$> DPat -> QWithAux PromDPatInfos PrM (DType, ADPat)
promotePat DPat
pat
promotePat (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].
  DPat
wildless_pat <- DPat -> QWithAux PromDPatInfos PrM DPat
forall (q :: * -> *). DsMonad q => DPat -> q DPat
removeWilds DPat
pat
  (DType
promoted, ADPat
pat') <- DPat -> QWithAux PromDPatInfos PrM (DType, ADPat)
promotePat DPat
wildless_pat
  DType
ki <- DType -> QWithAux PromDPatInfos PrM DType
forall (m :: * -> *). MonadFail m => DType -> m DType
promoteType DType
ty
  PromDPatInfos -> QWithAux PromDPatInfos PrM ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (PromDPatInfos -> QWithAux PromDPatInfos PrM ())
-> PromDPatInfos -> QWithAux PromDPatInfos PrM ()
forall a b. (a -> b) -> a -> b
$ VarPromotions -> OSet Name -> PromDPatInfos
PromDPatInfos [] (DType -> OSet Name
fvDType DType
ki)
  (DType, ADPat) -> QWithAux PromDPatInfos PrM (DType, ADPat)
forall (m :: * -> *) a. Monad m => a -> m a
return (DType -> DType -> DType
DSigT DType
promoted DType
ki, DType -> ADPat -> DType -> ADPat
ADSigP DType
promoted ADPat
pat' DType
ki)
promotePat DPat
DWildP = (DType, ADPat) -> QWithAux PromDPatInfos PrM (DType, ADPat)
forall (m :: * -> *) a. Monad m => a -> m a
return (DType
DWildCardT, ADPat
ADWildP)

promoteExp :: DExp -> PrM (DType, ADExp)
promoteExp :: DExp -> PrM (DType, ADExp)
promoteExp (DVarE Name
name) = (DType -> (DType, ADExp)) -> PrM DType -> PrM (DType, ADExp)
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
  Options
opts <- PrM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  (DType, ADExp) -> PrM (DType, ADExp)
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> DType
DConT (Name -> DType) -> Name -> DType
forall a b. (a -> b) -> a -> b
$ Options -> Name -> Name
defunctionalizedName0 Options
opts Name
name, Name -> ADExp
ADConE Name
name)
promoteExp (DLitE Lit
lit)  = (DType -> (DType, ADExp)) -> PrM DType -> PrM (DType, ADExp)
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 :: * -> *). Quasi q => Lit -> q DType
promoteLitExp Lit
lit
promoteExp (DAppE DExp
exp1 DExp
exp2) = do
  (DType
exp1', ADExp
ann_exp1) <- DExp -> PrM (DType, ADExp)
promoteExp DExp
exp1
  (DType
exp2', ADExp
ann_exp2) <- DExp -> PrM (DType, ADExp)
promoteExp DExp
exp2
  (DType, ADExp) -> PrM (DType, ADExp)
forall (m :: * -> *) a. Monad m => a -> m a
return (DType -> DType -> DType
apply DType
exp1' DType
exp2', ADExp -> ADExp -> ADExp
ADAppE ADExp
ann_exp1 ADExp
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`."
  DExp -> PrM (DType, ADExp)
promoteExp DExp
exp
promoteExp (DLamE [Name]
names DExp
exp) = do
  Options
opts <- PrM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  Name
lambdaName <- String -> PrM Name
forall (m :: * -> *). Quasi m => String -> m Name
newUniqueName String
"Lambda"
  [Name]
tyNames <- (Name -> PrM Name) -> [Name] -> PrM [Name]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Name -> PrM Name
forall (q :: * -> *). Quasi q => Name -> q Name
mkTyName [Name]
names
  let var_proms :: VarPromotions
var_proms = [Name] -> [Name] -> VarPromotions
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
names [Name]
tyNames
  (DType
rhs, ADExp
ann_exp) <- VarPromotions -> PrM (DType, ADExp) -> PrM (DType, ADExp)
forall a. VarPromotions -> PrM a -> PrM a
lambdaBind VarPromotions
var_proms (PrM (DType, ADExp) -> PrM (DType, ADExp))
-> PrM (DType, ADExp) -> PrM (DType, ADExp)
forall a b. (a -> b) -> a -> b
$ DExp -> PrM (DType, ADExp)
promoteExp DExp
exp
  [Name]
all_locals <- PrM [Name]
forall (m :: * -> *). MonadReader PrEnv m => m [Name]
allLocals
  let all_args :: [Name]
all_args = [Name]
all_locals [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
tyNames
      tvbs :: [DTyVarBndr]
tvbs     = (Name -> DTyVarBndr) -> [Name] -> [DTyVarBndr]
forall a b. (a -> b) -> [a] -> [b]
map Name -> DTyVarBndr
DPlainTV [Name]
all_args
  [DDec] -> PrM ()
forall (m :: * -> *). MonadWriter [DDec] m => [DDec] -> m ()
emitDecs [DTypeFamilyHead -> [DTySynEqn] -> DDec
DClosedTypeFamilyD (Name
-> [DTyVarBndr]
-> DFamilyResultSig
-> Maybe InjectivityAnn
-> DTypeFamilyHead
DTypeFamilyHead
                                 Name
lambdaName
                                 [DTyVarBndr]
tvbs
                                 DFamilyResultSig
DNoSig
                                 Maybe InjectivityAnn
forall a. Maybe a
Nothing)
                               [Maybe [DTyVarBndr] -> DType -> DType -> DTySynEqn
DTySynEqn Maybe [DTyVarBndr]
forall a. Maybe a
Nothing
                                          (DType -> DCxt -> DType
foldType (Name -> DType
DConT Name
lambdaName) (DCxt -> DType) -> DCxt -> DType
forall a b. (a -> b) -> a -> b
$
                                           (Name -> DType) -> [Name] -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map Name -> DType
DVarT [Name]
all_args)
                                          DType
rhs]]
  PrM [DDec] -> PrM ()
forall (m :: * -> *). MonadWriter [DDec] m => m [DDec] -> m ()
emitDecsM (PrM [DDec] -> PrM ()) -> PrM [DDec] -> PrM ()
forall a b. (a -> b) -> a -> b
$ Name -> Maybe Fixity -> DefunKindInfo -> PrM [DDec]
defunctionalize Name
lambdaName Maybe Fixity
forall a. Maybe a
Nothing (DefunKindInfo -> PrM [DDec]) -> DefunKindInfo -> PrM [DDec]
forall a b. (a -> b) -> a -> b
$ [DTyVarBndr] -> Maybe DType -> DefunKindInfo
DefunNoSAK [DTyVarBndr]
tvbs Maybe DType
forall a. Maybe a
Nothing
  let promLambda :: DType
promLambda = (DType -> DType -> DType) -> DType -> DCxt -> DType
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl DType -> DType -> DType
apply (Name -> DType
DConT (Options -> Name -> Int -> Name
defunctionalizedName Options
opts Name
lambdaName Int
0))
                               ((Name -> DType) -> [Name] -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map Name -> DType
DVarT [Name]
all_locals)
  (DType, ADExp) -> PrM (DType, ADExp)
forall (m :: * -> *) a. Monad m => a -> m a
return (DType
promLambda, [Name] -> DType -> [Name] -> ADExp -> ADExp
ADLamE [Name]
tyNames DType
promLambda [Name]
names ADExp
ann_exp)
promoteExp (DCaseE DExp
exp [DMatch]
matches) = do
  Name
caseTFName <- String -> PrM Name
forall (m :: * -> *). Quasi m => String -> m Name
newUniqueName String
"Case"
  [Name]
all_locals <- PrM [Name]
forall (m :: * -> *). MonadReader PrEnv m => m [Name]
allLocals
  let prom_case :: DType
prom_case = DType -> DCxt -> DType
foldType (Name -> DType
DConT Name
caseTFName) ((Name -> DType) -> [Name] -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map Name -> DType
DVarT [Name]
all_locals)
  (DType
exp', ADExp
ann_exp)     <- DExp -> PrM (DType, ADExp)
promoteExp DExp
exp
  ([DTySynEqn]
eqns, [ADMatch]
ann_matches) <- (DMatch -> PrM (DTySynEqn, ADMatch))
-> [DMatch] -> PrM ([DTySynEqn], [ADMatch])
forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM (DType -> DMatch -> PrM (DTySynEqn, ADMatch)
promoteMatch DType
prom_case) [DMatch]
matches
  Name
tyvarName  <- String -> PrM Name
forall (m :: * -> *). Quasi m => String -> m Name
qNewName String
"t"
  let all_args :: [Name]
all_args = [Name]
all_locals [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name
tyvarName]
      tvbs :: [DTyVarBndr]
tvbs     = (Name -> DTyVarBndr) -> [Name] -> [DTyVarBndr]
forall a b. (a -> b) -> [a] -> [b]
map Name -> DTyVarBndr
DPlainTV [Name]
all_args
  [DDec] -> PrM ()
forall (m :: * -> *). MonadWriter [DDec] m => [DDec] -> m ()
emitDecs [DTypeFamilyHead -> [DTySynEqn] -> DDec
DClosedTypeFamilyD (Name
-> [DTyVarBndr]
-> DFamilyResultSig
-> Maybe InjectivityAnn
-> DTypeFamilyHead
DTypeFamilyHead Name
caseTFName [DTyVarBndr]
tvbs DFamilyResultSig
DNoSig Maybe InjectivityAnn
forall a. Maybe a
Nothing) [DTySynEqn]
eqns]
    -- See Note [Annotate case return type] in Single
  let applied_case :: DType
applied_case = DType
prom_case DType -> DType -> DType
`DAppT` DType
exp'
  (DType, ADExp) -> PrM (DType, ADExp)
forall (m :: * -> *) a. Monad m => a -> m a
return ( DType
applied_case
         , ADExp -> [ADMatch] -> DType -> ADExp
ADCaseE ADExp
ann_exp [ADMatch]
ann_matches DType
applied_case )
promoteExp (DLetE [DLetDec]
decs DExp
exp) = do
  Uniq
unique <- PrM Uniq
forall (q :: * -> *). DsMonad q => q Uniq
qNewUnique
  ([LetBind]
binds, ALetDecEnv
ann_env) <- Maybe Uniq -> [DLetDec] -> PrM ([LetBind], ALetDecEnv)
promoteLetDecs (Uniq -> Maybe Uniq
forall a. a -> Maybe a
Just Uniq
unique) [DLetDec]
decs
  (DType
exp', ADExp
ann_exp) <- [LetBind] -> PrM (DType, ADExp) -> PrM (DType, ADExp)
forall a. [LetBind] -> PrM a -> PrM a
letBind [LetBind]
binds (PrM (DType, ADExp) -> PrM (DType, ADExp))
-> PrM (DType, ADExp) -> PrM (DType, ADExp)
forall a b. (a -> b) -> a -> b
$ DExp -> PrM (DType, ADExp)
promoteExp DExp
exp
  (DType, ADExp) -> PrM (DType, ADExp)
forall (m :: * -> *) a. Monad m => a -> m a
return (DType
exp', ALetDecEnv -> ADExp -> ADExp
ADLetE ALetDecEnv
ann_env ADExp
ann_exp)
promoteExp (DSigE DExp
exp DType
ty) = do
  (DType
exp', ADExp
ann_exp) <- DExp -> PrM (DType, ADExp)
promoteExp DExp
exp
  DType
ty' <- DType -> PrM DType
forall (m :: * -> *). MonadFail m => DType -> m DType
promoteType DType
ty
  (DType, ADExp) -> PrM (DType, ADExp)
forall (m :: * -> *) a. Monad m => a -> m a
return (DType -> DType -> DType
DSigT DType
exp' DType
ty', DType -> ADExp -> DType -> ADExp
ADSigE DType
exp' ADExp
ann_exp DType
ty')
promoteExp e :: DExp
e@(DStaticE DExp
_) = String -> PrM (DType, ADExp)
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)

promoteLitExp :: Quasi q => Lit -> q DType
promoteLitExp :: Lit -> q DType
promoteLitExp (IntegerL Uniq
n)
  | Uniq
n Uniq -> Uniq -> Bool
forall a. Ord a => a -> a -> Bool
>= Uniq
0    = DType -> q DType
forall (m :: * -> *) a. Monad m => a -> m a
return (DType -> q DType) -> DType -> q DType
forall a b. (a -> b) -> a -> b
$ (Name -> DType
DConT Name
tyFromIntegerName DType -> DType -> DType
`DAppT` TyLit -> DType
DLitT (Uniq -> TyLit
NumTyLit Uniq
n))
  | Bool
otherwise = DType -> q DType
forall (m :: * -> *) a. Monad m => a -> m a
return (DType -> q DType) -> DType -> q DType
forall a b. (a -> b) -> a -> b
$ (Name -> DType
DConT Name
tyNegateName DType -> DType -> DType
`DAppT`
                          (Name -> DType
DConT Name
tyFromIntegerName DType -> DType -> DType
`DAppT` TyLit -> DType
DLitT (Uniq -> TyLit
NumTyLit (-Uniq
n))))
promoteLitExp (StringL String
str) = do
  let prom_str_lit :: DType
prom_str_lit = TyLit -> DType
DLitT (String -> TyLit
StrTyLit String
str)
  Bool
os_enabled <- Extension -> q Bool
forall (m :: * -> *). Quasi m => Extension -> m Bool
qIsExtEnabled Extension
LangExt.OverloadedStrings
  DType -> q DType
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DType -> q DType) -> DType -> q DType
forall a b. (a -> b) -> a -> b
$ if Bool
os_enabled
         then Name -> DType
DConT Name
tyFromStringName DType -> DType -> DType
`DAppT` DType
prom_str_lit
         else DType
prom_str_lit
promoteLitExp Lit
lit =
  String -> q DType
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"Only string and natural number 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 :: 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 (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 (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 (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 Lit
lit =
  String -> m DType
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"Only string and natural number literals can be promoted: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Lit -> String
forall a. Show a => a -> String
show Lit
lit)

-- See Note [DerivedDecl]
promoteDerivedEqDec :: DerivedEqDecl -> PrM ()
promoteDerivedEqDec :: DerivedEqDecl -> PrM ()
promoteDerivedEqDec (DerivedDecl { ded_type :: forall (cls :: * -> Constraint). DerivedDecl cls -> DType
ded_type = DType
ty
                                 , ded_decl :: forall (cls :: * -> Constraint). DerivedDecl cls -> DataDecl
ded_decl = DataDecl Name
_ [DTyVarBndr]
_ [DCon]
cons }) = do
  DType
kind <- DType -> PrM DType
forall (m :: * -> *). MonadFail m => DType -> m DType
promoteType DType
ty
  [DDec]
inst_decs <- DType -> [DCon] -> PrM [DDec]
forall (q :: * -> *). OptionsMonad q => DType -> [DCon] -> q [DDec]
mkEqTypeInstance DType
kind [DCon]
cons
  [DDec] -> PrM ()
forall (m :: * -> *). MonadWriter [DDec] m => [DDec] -> m ()
emitDecs [DDec]
inst_decs