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

module Data.Singletons.Promote where

import Language.Haskell.TH hiding ( Q, cxt )
import Language.Haskell.TH.Syntax ( Quasi(..) )
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.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 qualified Data.Map.Strict as Map
import Data.Map.Strict ( Map )
import Data.Maybe
import qualified GHC.LanguageExtensions.Type as LangExt

-- | Generate promoted definitions from a type that is already defined.
-- This is generally only useful with classes.
genPromotions :: DsMonad q => [Name] -> q [Dec]
genPromotions :: [Name] -> q [Dec]
genPromotions names :: [Name]
names = do
  [Name] -> q ()
forall (q :: * -> *). Quasi q => [Name] -> q ()
checkForRep [Name]
names
  [Info]
infos <- (Name -> q Info) -> [Name] -> q [Info]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Name -> q Info
forall (q :: * -> *). DsMonad q => Name -> q Info
reifyWithLocals [Name]
names
  [DInfo]
dinfos <- (Info -> q DInfo) -> [Info] -> 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]
infos
  [DDec]
ddecs <- [Dec] -> PrM () -> q [DDec]
forall (q :: * -> *). DsMonad q => [Dec] -> PrM () -> q [DDec]
promoteM_ [] (PrM () -> q [DDec]) -> PrM () -> 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] -> 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]
ddecs

-- | Promote every declaration given to the type level, retaining the originals.
promote :: DsMonad q => q [Dec] -> q [Dec]
promote :: q [Dec] -> q [Dec]
promote qdec :: q [Dec]
qdec = do
  [Dec]
decls <- q [Dec]
qdec
  [DDec]
ddecls <- [Dec] -> DsM q [DDec] -> q [DDec]
forall (q :: * -> *) a. DsMonad q => [Dec] -> DsM q a -> q a
withLocalDeclarations [Dec]
decls (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]
decls
  [DDec]
promDecls <- [Dec] -> PrM () -> q [DDec]
forall (q :: * -> *). DsMonad q => [Dec] -> PrM () -> q [DDec]
promoteM_ [Dec]
decls (PrM () -> q [DDec]) -> PrM () -> q [DDec]
forall a b. (a -> b) -> a -> b
$ [DDec] -> PrM ()
promoteDecs [DDec]
ddecls
  [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]
decls [Dec] -> [Dec] -> [Dec]
forall a. [a] -> [a] -> [a]
++ [DDec] -> [Dec]
decsToTH [DDec]
promDecls

-- | 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 :: DsMonad q => q [Dec] -> q [Dec]
promoteOnly :: q [Dec] -> q [Dec]
promoteOnly qdec :: q [Dec]
qdec = do
  [Dec]
decls  <- q [Dec]
qdec
  [DDec]
ddecls <- [Dec] -> q [DDec]
forall (q :: * -> *). DsMonad q => [Dec] -> q [DDec]
dsDecs [Dec]
decls
  [DDec]
promDecls <- [Dec] -> PrM () -> q [DDec]
forall (q :: * -> *). DsMonad q => [Dec] -> PrM () -> q [DDec]
promoteM_ [Dec]
decls (PrM () -> q [DDec]) -> PrM () -> q [DDec]
forall a b. (a -> b) -> a -> b
$ [DDec] -> PrM ()
promoteDecs [DDec]
ddecls
  [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]
promDecls

-- | Generate defunctionalization symbols for existing type families.
--
-- 'genDefunSymbols' has reasonable support for type families that use
-- dependent quantification. For instance, this:
--
-- @
-- type family MyProxy k (a :: k) :: Type where
--   MyProxy k (a :: k) = Proxy a
--
-- $('genDefunSymbols' [''MyProxy])
-- @
--
-- Will generate the following defunctionalization symbols:
--
-- @
-- data MyProxySym0     :: Type  ~> k ~> Type
-- data MyProxySym1 (k  :: Type) :: k ~> Type
-- @
--
-- Note that @MyProxySym0@ is a bit more general than it ought to be, since
-- there is no dependency between the first kind (@Type@) and the second kind
-- (@k@). But this would require the ability to write something like:
--
-- @
-- data MyProxySym0 :: forall (k :: Type) ~> k ~> Type
-- @
--
-- Which currently isn't possible. So for the time being, the kind of
-- @MyProxySym0@ will be slightly more general, which means that under rare
-- circumstances, you may have to provide extra type signatures if you write
-- code which exploits the dependency in @MyProxy@'s kind.
genDefunSymbols :: DsMonad q => [Name] -> q [Dec]
genDefunSymbols :: [Name] -> q [Dec]
genDefunSymbols names :: [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 :: * -> *). DsMonad 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 :: DsMonad 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 :: * -> *). DsMonad q => Name -> q [Dec]
promoteEqInstance

-- | Produce instances for 'POrd' from the given types
promoteOrdInstances :: DsMonad 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 :: * -> *). DsMonad q => Name -> q [Dec]
promoteOrdInstance

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

-- | Produce instances for 'PBounded' from the given types
promoteBoundedInstances :: DsMonad 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 :: * -> *). DsMonad q => Name -> q [Dec]
promoteBoundedInstance

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

-- | Produce instances for 'PEnum' from the given types
promoteEnumInstances :: DsMonad 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 :: * -> *). DsMonad q => Name -> q [Dec]
promoteEnumInstance

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

-- | Produce instances for 'PShow' from the given types
promoteShowInstances :: DsMonad 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 :: * -> *). DsMonad q => Name -> q [Dec]
promoteShowInstance

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

-- | Produce an instance for @(==)@ (type-level equality) from the given type
promoteEqInstance :: DsMonad q => Name -> q [Dec]
promoteEqInstance :: Name -> q [Dec]
promoteEqInstance name :: Name
name = do
  (tvbs :: [TyVarBndr]
tvbs, cons :: [Con]
cons) <- String -> Name -> q ([TyVarBndr], [Con])
forall (q :: * -> *).
DsMonad q =>
String -> Name -> q ([TyVarBndr], [Con])
getDataD "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 :: * -> *). Quasi 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 :: DsMonad q => DerivDesc q -> String -> Name -> q [Dec]
promoteInstance :: DerivDesc q -> String -> Name -> q [Dec]
promoteInstance mk_inst :: DerivDesc q
mk_inst class_name :: String
class_name name :: Name
name = do
  (tvbs :: [TyVarBndr]
tvbs, cons :: [Con]
cons) <- String -> Name -> q ([TyVarBndr], [Con])
forall (q :: * -> *).
DsMonad q =>
String -> Name -> q ([TyVarBndr], [Con])
getDataD ("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]
++ " 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 :: * -> *). DsMonad 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 -> UInstDecl -> PrM AInstDecl
promoteInstanceDec OMap Name DType
forall k v. OMap k v
OMap.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 dec :: DDec
dec _instances :: Maybe [DDec]
_instances) = [DDec] -> PrM ()
promoteDecs [DDec
dec]
promoteInfo (DPrimTyConI _name :: Name
_name _numArgs :: Int
_numArgs _unlifted :: Bool
_unlifted) =
  String -> PrM ()
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "Promotion of primitive type constructors not supported"
promoteInfo (DVarI _name :: Name
_name _ty :: DType
_ty _mdec :: Maybe Name
_mdec) =
  String -> PrM ()
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "Promotion of individual values not supported"
promoteInfo (DTyVarI _name :: Name
_name _ty :: DType
_ty) =
  String -> PrM ()
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "Promotion of individual type variables not supported"
promoteInfo (DPatSynI {}) =
  String -> PrM ()
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "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 raw_decls :: [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 :: * -> *). DsMonad m => [DDec] -> m PartitionedDecs
partitionDecs [DDec]
decls

  [TySynDecl]
-> [ClosedTypeFamilyDecl] -> [OpenTypeFamilyDecl] -> PrM ()
defunTypeDecls [TySynDecl]
ty_syns [ClosedTypeFamilyDecl]
c_tyfams [OpenTypeFamilyDecl]
o_tyfams
    -- promoteLetDecs returns LetBinds, which we don't need at top level
  ([LetBind], ALetDecEnv)
_ <- (String, String) -> [DLetDec] -> PrM ([LetBind], ALetDecEnv)
promoteLetDecs (String, String)
noPrefix [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
  (UInstDecl -> PrM AInstDecl) -> [UInstDecl] -> PrM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (OMap Name DType -> UInstDecl -> PrM AInstDecl
promoteInstanceDec OMap Name DType
orig_meth_sigs) [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
  [DataDecl] -> PrM ()
promoteDataDecs [DataDecl]
datas

promoteDataDecs :: [DataDecl] -> PrM ()
promoteDataDecs :: [DataDecl] -> PrM ()
promoteDataDecs data_decs :: [DataDecl]
data_decs = do
  [DLetDec]
rec_selectors <- (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]
extract_rec_selectors [DataDecl]
data_decs
  ([LetBind], ALetDecEnv)
_ <- (String, String) -> [DLetDec] -> PrM ([LetBind], ALetDecEnv)
promoteLetDecs (String, String)
noPrefix [DLetDec]
rec_selectors
  (DataDecl -> PrM ()) -> [DataDecl] -> PrM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ DataDecl -> PrM ()
promoteDataDec [DataDecl]
data_decs
  where
    extract_rec_selectors :: DataDecl -> PrM [DLetDec]
    extract_rec_selectors :: DataDecl -> PrM [DLetDec]
extract_rec_selectors (DataDecl data_name :: Name
data_name tvbs :: [DTyVarBndr]
tvbs cons :: [DCon]
cons) =
      let arg_ty :: DType
arg_ty = DType -> [DTyVarBndr] -> DType
foldTypeTvbs (Name -> DType
DConT Name
data_name) [DTyVarBndr]
tvbs
      in
      DType -> [DCon] -> PrM [DLetDec]
forall (q :: * -> *). DsMonad q => DType -> [DCon] -> q [DLetDec]
getRecordSelectors DType
arg_ty [DCon]
cons

-- curious about ALetDecEnv? See the LetDecEnv module for an explanation.
promoteLetDecs :: (String, String) -- (alpha, symb) prefixes to use
               -> [DLetDec] -> PrM ([LetBind], ALetDecEnv)
  -- See Note [Promoting declarations in two stages]
promoteLetDecs :: (String, String) -> [DLetDec] -> PrM ([LetBind], ALetDecEnv)
promoteLetDecs prefixes :: (String, String)
prefixes decls :: [DLetDec]
decls = do
  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
name, _) <- 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 = (String, String) -> Name -> Name
promoteValNameLhsPrefix (String, String)
prefixes Name
name
                    sym :: Name
sym = Name -> Int -> Name
promoteTySym Name
proName ([Name] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
all_locals) ]
  (decs :: [DDec]
decs, let_dec_env' :: 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
$ (String, String)
-> LetDecEnv Unannotated -> PrM ([DDec], ALetDecEnv)
promoteLetDecEnv (String, String)
prefixes 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 })

-- Promotion of data types to kinds is automatic (see "Giving Haskell a
-- Promotion" paper for more details). Here we "plug into" the promotion
-- mechanism to add some extra stuff to the promotion:
--
--  * if data type derives Eq we generate a type family that implements the
--    equality test for the data type.
--
--  * for each data constructor with arity greater than 0 we generate type level
--    symbols for use with Apply type family. In this way promoted data
--    constructors and promoted functions can be used in a uniform way at the
--    type level in the same way they can be used uniformly at the type level.
--
--  * for each nullary data constructor we generate a type synonym
promoteDataDec :: DataDecl -> PrM ()
promoteDataDec :: DataDecl -> PrM ()
promoteDataDec (DataDecl _name :: Name
_name _tvbs :: [DTyVarBndr]
_tvbs ctors :: [DCon]
ctors) = do
  [DDec]
ctorSyms <- [DCon] -> PrM [DDec]
buildDefunSymsDataD [DCon]
ctors
  [DDec] -> PrM ()
forall (m :: * -> *). MonadWriter [DDec] m => [DDec] -> m ()
emitDecs [DDec]
ctorSyms

-- Note [CUSKification]
-- ~~~~~~~~~~~~~~~~~~~~
-- GHC #12928 means that sometimes, this TH code will produce a declaration
-- that has a kind signature even when we want kind inference to work. There
-- seems to be no way to avoid this, so we embrace it:
--
--   * If a class type variable has no explicit kind, we make no effort to
--     guess it and default to *. This is OK because before GHC 8.0, we were
--     limited by KProxy anyway.
--
--   * If a class type variable has an explicit kind, it is preserved.
--
-- This way, we always get proper CUSKs where we need them.

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_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
  let
    -- a workaround for GHC Trac #12928; see Note [CUSKification]
    tvbs :: [DTyVarBndr]
tvbs = (DTyVarBndr -> DTyVarBndr) -> [DTyVarBndr] -> [DTyVarBndr]
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndr -> DTyVarBndr
cuskify [DTyVarBndr]
tvbs'
  let pClsName :: Name
pClsName = Name -> Name
promoteClassName 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
    [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) (OMap Name DType -> [LetBind]
forall k v. OMap k v -> [(k, v)]
OMap.assocs OMap Name DType
meth_sigs)
    let 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
    (default_decs :: [DDec]
default_decs, ann_rhss :: [ALetDecRHS]
ann_rhss, prom_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 (OMap Name DType
-> Maybe (Map Name DType)
-> OMap Name DType
-> (Name, LetDecRHS Unannotated)
-> PrM (DDec, ALetDecRHS, DType)
promoteMethod OMap Name DType
forall k v. OMap k v
OMap.empty Maybe (Map Name DType)
forall a. Maybe a
Nothing OMap Name DType
meth_sigs) [(Name, LetDecRHS Unannotated)]
defaults_list

    let infix_decls' :: [DDec]
infix_decls' = [Maybe DDec] -> [DDec]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe DDec] -> [DDec]) -> [Maybe DDec] -> [DDec]
forall a b. (a -> b) -> a -> b
$ ((Name, Fixity) -> Maybe DDec) -> [(Name, Fixity)] -> [Maybe DDec]
forall a b. (a -> b) -> [a] -> [b]
map ((Name -> Fixity -> Maybe DDec) -> (Name, Fixity) -> Maybe DDec
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Name -> Fixity -> Maybe DDec
promoteInfixDecl)
                                 ([(Name, Fixity)] -> [Maybe DDec])
-> [(Name, Fixity)] -> [Maybe 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

    -- no need to do anything to the fundeps. They work as is!
    [DDec] -> PrM ()
forall (m :: * -> *). MonadWriter [DDec] m => [DDec] -> m ()
emitDecs [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')]
    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
name ty :: DType
ty = do
      let proName :: Name
proName = Name -> Name
promoteValNameLhs Name
name
      (argKs :: DCxt
argKs, resK :: DType
resK) <- DType -> PrM (DCxt, DType)
forall (m :: * -> *). MonadFail m => DType -> m (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 "arg") DCxt
argKs
      let tvbs :: [DTyVarBndr]
tvbs = (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
      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 -> [DTyVarBndr] -> Maybe DType -> PrM [DDec]
defunReifyFixity Name
proName [DTyVarBndr]
tvbs (DType -> Maybe DType
forall a. a -> Maybe a
Just DType
resK)

      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]
tvbs
                                                 (DType -> DFamilyResultSig
DKindSig DType
resK)
                                                 Maybe InjectivityAnn
forall a. Maybe a
Nothing)

-- returns (unpromoted method name, ALetDecRHS) pairs
promoteInstanceDec :: OMap Name DType -> UInstDecl -> PrM AInstDecl
promoteInstanceDec :: OMap Name DType -> UInstDecl -> PrM AInstDecl
promoteInstanceDec orig_meth_sigs :: OMap Name DType
orig_meth_sigs
                   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
  [Name]
cls_tvb_names <- PrM [Name]
lookup_cls_tvb_names
  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 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
    (meths' :: [DDec]
meths', ann_rhss :: [ALetDecRHS]
ann_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 (OMap Name DType
-> Maybe (Map Name DType)
-> OMap Name DType
-> (Name, LetDecRHS Unannotated)
-> PrM (DDec, ALetDecRHS, DType)
promoteMethod OMap Name DType
inst_sigs (Map Name DType -> Maybe (Map Name DType)
forall a. a -> Maybe a
Just Map Name DType
subst) 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
    pClsName :: Name
pClsName = Name -> Name
promoteClassName Name
cls_name

    lookup_cls_tvb_names :: PrM [Name]
    lookup_cls_tvb_names :: PrM [Name]
lookup_cls_tvb_names = do
      let mk_tvb_names :: MaybeT PrM [Name]
mk_tvb_names = PrM (Maybe DInfo) -> MaybeT PrM [Name]
extract_tvb_names (Name -> PrM (Maybe DInfo)
forall (q :: * -> *). DsMonad q => Name -> q (Maybe DInfo)
dsReifyTypeNameInfo Name
pClsName)
                     MaybeT PrM [Name] -> MaybeT PrM [Name] -> MaybeT PrM [Name]
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> PrM (Maybe DInfo) -> MaybeT PrM [Name]
extract_tvb_names (Name -> PrM (Maybe DInfo)
forall (q :: * -> *). DsMonad q => Name -> q (Maybe DInfo)
dsReifyTypeNameInfo Name
cls_name)
                      -- See Note [Using dsReifyTypeNameInfo when promoting instances]
      Maybe [Name]
mb_tvb_names <- MaybeT PrM [Name] -> PrM (Maybe [Name])
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT MaybeT PrM [Name]
mk_tvb_names
      case Maybe [Name]
mb_tvb_names of
        Just tvb_names :: [Name]
tvb_names -> [Name] -> PrM [Name]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Name]
tvb_names
        Nothing -> String -> PrM [Name]
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> PrM [Name]) -> String -> PrM [Name]
forall a b. (a -> b) -> a -> b
$ "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_tvb_names :: PrM (Maybe DInfo) -> MaybeT PrM [Name]
    extract_tvb_names :: PrM (Maybe DInfo) -> MaybeT PrM [Name]
extract_tvb_names reify_info :: 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 _ _ tvbs :: [DTyVarBndr]
tvbs _ _) _)
          -> [Name] -> MaybeT PrM [Name]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Name] -> MaybeT PrM [Name]) -> [Name] -> MaybeT PrM [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
        _ -> MaybeT PrM [Name]
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.
-}

promoteMethod :: OMap Name DType -- InstanceSigs for methods
              -> Maybe (Map Name DKind)
                    -- ^ instantiations for class tyvars (Nothing for default decls)
                    --   See Note [Promoted class method kinds]
              -> OMap Name DType    -- method types
              -> (Name, ULetDecRHS)
              -> PrM (DDec, ALetDecRHS, DType)
                 -- returns (type instance, ALetDecRHS, promoted RHS)
promoteMethod :: OMap Name DType
-> Maybe (Map Name DType)
-> OMap Name DType
-> (Name, LetDecRHS Unannotated)
-> PrM (DDec, ALetDecRHS, DType)
promoteMethod inst_sigs_map :: OMap Name DType
inst_sigs_map m_subst :: Maybe (Map Name DType)
m_subst orig_sigs_map :: OMap Name DType
orig_sigs_map (meth_name :: Name
meth_name, meth_rhs :: LetDecRHS Unannotated
meth_rhs) = do
  (meth_arg_kis :: DCxt
meth_arg_kis, meth_res_ki :: DType
meth_res_ki) <- PrM (DCxt, DType)
lookup_meth_ty
  [Name]
meth_arg_tvs <- (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 "a") DCxt
meth_arg_kis
  let helperNameBase :: String
helperNameBase = case Name -> String
nameBase Name
proName of
                         first :: Char
first:_ | Bool -> Bool
not (Char -> Bool
isHsLetter Char
first) -> "TFHelper"
                         alpha :: 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 proHelperName :: Name
proHelperName = Name -> Name
promoteValNameLhs Name
helperName
  ((_, _, _, eqns :: [DTySynEqn]
eqns), _defuns :: [DDec]
_defuns, ann_rhs :: ALetDecRHS
ann_rhs)
    <- Maybe (DCxt, DType)
-> OMap Name DType
-> OMap Name Fixity
-> (String, String)
-> Name
-> LetDecRHS Unannotated
-> PrM
     ((Name, [DTyVarBndr], Maybe DType, [DTySynEqn]), [DDec],
      ALetDecRHS)
promoteLetDecRHS ((DCxt, DType) -> Maybe (DCxt, DType)
forall a. a -> Maybe a
Just (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
                        (String, String)
noPrefix Name
helperName LetDecRHS Unannotated
meth_rhs
  let tvbs :: [DTyVarBndr]
tvbs = (Name -> DType -> DTyVarBndr) -> [Name] -> DCxt -> [DTyVarBndr]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Name -> DType -> DTyVarBndr
DKindedTV [Name]
meth_arg_tvs DCxt
meth_arg_kis
  [DDec] -> PrM ()
forall (m :: * -> *). MonadWriter [DDec] m => [DDec] -> m ()
emitDecs [DTypeFamilyHead -> [DTySynEqn] -> DDec
DClosedTypeFamilyD (Name
-> [DTyVarBndr]
-> DFamilyResultSig
-> Maybe InjectivityAnn
-> DTypeFamilyHead
DTypeFamilyHead
                                  Name
proHelperName
                                  [DTyVarBndr]
tvbs
                                  (DType -> DFamilyResultSig
DKindSig DType
meth_res_ki)
                                  Maybe InjectivityAnn
forall a. Maybe a
Nothing)
                               [DTySynEqn]
eqns]
  PrM [DDec] -> PrM ()
forall (m :: * -> *). MonadWriter [DDec] m => m [DDec] -> m ()
emitDecsM (Name -> Maybe Fixity -> [DTyVarBndr] -> Maybe DType -> PrM [DDec]
defunctionalize Name
proHelperName Maybe Fixity
forall a. Maybe a
Nothing [DTyVarBndr]
tvbs (DType -> Maybe DType
forall a. a -> Maybe a
Just DType
meth_res_ki))
  (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
promoteValRhs Name
helperName) ((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 -> Int -> Name
promoteTySym Name
helperName 0) )
  where
    proName :: Name
proName = Name -> Name
promoteValNameLhs Name
meth_name

    lookup_meth_ty :: PrM ([DKind], DKind)
    lookup_meth_ty :: PrM (DCxt, DType)
lookup_meth_ty =
      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 ty :: DType
ty ->
          -- We have an InstanceSig. These are easy: no substitution for clas
          -- variables is required at all!
          DType -> PrM (DCxt, DType)
forall (m :: * -> *). MonadFail m => DType -> m (DCxt, DType)
promoteUnraveled DType
ty
        Nothing -> do
          -- We don't have an InstanceSig, so we must compute the kind to use
          -- ourselves (possibly substituting for class variables below).
          (arg_kis :: DCxt
arg_kis, res_ki :: DType
res_ki) <-
            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
              Nothing -> do
                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 _ tvbs :: [DTyVarBndr]
tvbs mb_res_ki :: DFamilyResultSig
mb_res_ki _)) _)
                    -> let arg_kis :: DCxt
arg_kis = (DTyVarBndr -> DType) -> [DTyVarBndr] -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map (Maybe DType -> DType
default_to_star (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
default_to_star (DFamilyResultSig -> Maybe DType
resultSigToMaybeKind DFamilyResultSig
mb_res_ki)
                        in (DCxt, DType) -> PrM (DCxt, DType)
forall (m :: * -> *) a. Monad m => a -> m a
return (DCxt
arg_kis, DType
res_ki)
                  _ -> String -> PrM (DCxt, DType)
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> PrM (DCxt, DType)) -> String -> PrM (DCxt, DType)
forall a b. (a -> b) -> a -> b
$ "Cannot find type annotation for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
proName
              Just ty :: DType
ty -> DType -> PrM (DCxt, DType)
forall (m :: * -> *). MonadFail m => DType -> m (DCxt, DType)
promoteUnraveled DType
ty
          let -- If we're dealing with an associated type family instance, substitute
              -- in the kind of the instance for better kind information in the RHS
              -- helper function. If we're dealing with a default family implementation
              -- (m_subst = Nothing), there's no need for a substitution.
              -- See Note [Promoted class method kinds]
              do_subst :: DType -> DType
do_subst      = (DType -> DType)
-> (Map Name DType -> DType -> DType)
-> Maybe (Map Name DType)
-> DType
-> DType
forall b a. b -> (a -> b) -> Maybe a -> b
maybe DType -> DType
forall a. a -> a
id Map Name DType -> DType -> DType
substKind Maybe (Map Name DType)
m_subst
              meth_arg_kis' :: DCxt
meth_arg_kis' = (DType -> DType) -> DCxt -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map DType -> DType
do_subst DCxt
arg_kis
              meth_res_ki' :: DType
meth_res_ki'  = DType -> DType
do_subst DType
res_ki
          (DCxt, DType) -> PrM (DCxt, DType)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DCxt
meth_arg_kis', DType
meth_res_ki')

    default_to_star :: Maybe DType -> DType
default_to_star Nothing  = Name -> DType
DConT Name
typeKindName
    default_to_star (Just k :: DType
k) = DType
k

{-
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) (z :: Bool)
    type M x y z = MHelper1 x y z

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

  type family MHelper1 (x :: a)   (y :: Bool) (z :: Bool) where ...
  type family MHelper2 (x :: [a]) (y :: Bool) (z :: Bool) 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 :: (String, String) -> ULetDecEnv -> PrM ([DDec], ALetDecEnv)
promoteLetDecEnv :: (String, String)
-> LetDecEnv Unannotated -> PrM ([DDec], ALetDecEnv)
promoteLetDecEnv prefixes :: (String, String)
prefixes (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
  let infix_decls :: [DDec]
infix_decls = [Maybe DDec] -> [DDec]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe DDec] -> [DDec]) -> [Maybe DDec] -> [DDec]
forall a b. (a -> b) -> a -> b
$ ((Name, Fixity) -> Maybe DDec) -> [(Name, Fixity)] -> [Maybe DDec]
forall a b. (a -> b) -> [a] -> [b]
map ((Name -> Fixity -> Maybe DDec) -> (Name, Fixity) -> Maybe DDec
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Name -> Fixity -> Maybe DDec
promoteInfixDecl)
                              ([(Name, Fixity)] -> [Maybe DDec])
-> [(Name, Fixity)] -> [Maybe 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 (names :: [Name]
names, rhss :: [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
  (payloads :: [(Name, [DTyVarBndr], Maybe DType, [DTySynEqn])]
payloads, defun_decss :: [[DDec]]
defun_decss, ann_rhss :: [ALetDecRHS]
ann_rhss)
    <- ([((Name, [DTyVarBndr], Maybe DType, [DTySynEqn]), [DDec],
   ALetDecRHS)]
 -> ([(Name, [DTyVarBndr], Maybe DType, [DTySynEqn])], [[DDec]],
     [ALetDecRHS]))
-> PrM
     [((Name, [DTyVarBndr], Maybe DType, [DTySynEqn]), [DDec],
       ALetDecRHS)]
-> PrM
     ([(Name, [DTyVarBndr], Maybe DType, [DTySynEqn])], [[DDec]],
      [ALetDecRHS])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [((Name, [DTyVarBndr], Maybe DType, [DTySynEqn]), [DDec],
  ALetDecRHS)]
-> ([(Name, [DTyVarBndr], Maybe DType, [DTySynEqn])], [[DDec]],
    [ALetDecRHS])
forall a b c. [(a, b, c)] -> ([a], [b], [c])
unzip3 (PrM
   [((Name, [DTyVarBndr], Maybe DType, [DTySynEqn]), [DDec],
     ALetDecRHS)]
 -> PrM
      ([(Name, [DTyVarBndr], Maybe DType, [DTySynEqn])], [[DDec]],
       [ALetDecRHS]))
-> PrM
     [((Name, [DTyVarBndr], Maybe DType, [DTySynEqn]), [DDec],
       ALetDecRHS)]
-> PrM
     ([(Name, [DTyVarBndr], Maybe DType, [DTySynEqn])], [[DDec]],
      [ALetDecRHS])
forall a b. (a -> b) -> a -> b
$ (Name
 -> LetDecRHS Unannotated
 -> PrM
      ((Name, [DTyVarBndr], Maybe DType, [DTySynEqn]), [DDec],
       ALetDecRHS))
-> [Name]
-> [LetDecRHS Unannotated]
-> PrM
     [((Name, [DTyVarBndr], Maybe DType, [DTySynEqn]), [DDec],
       ALetDecRHS)]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (Maybe (DCxt, DType)
-> OMap Name DType
-> OMap Name Fixity
-> (String, String)
-> Name
-> LetDecRHS Unannotated
-> PrM
     ((Name, [DTyVarBndr], Maybe DType, [DTySynEqn]), [DDec],
      ALetDecRHS)
promoteLetDecRHS Maybe (DCxt, DType)
forall a. Maybe a
Nothing OMap Name DType
type_env OMap Name Fixity
fix_env (String, String)
prefixes) [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 = ((Name, [DTyVarBndr], Maybe DType, [DTySynEqn]) -> DDec)
-> [(Name, [DTyVarBndr], Maybe DType, [DTySynEqn])] -> [DDec]
forall a b. (a -> b) -> [a] -> [b]
map (Name, [DTyVarBndr], Maybe DType, [DTySynEqn]) -> DDec
payload_to_dec [(Name, [DTyVarBndr], Maybe DType, [DTySynEqn])]
payloads [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)] -> IfAnn Annotated (OMap Name (OSet Name)) ()
forall k v. Ord k => [(k, v)] -> OMap k v
OMap.fromList ([(Name, OSet Name)] -> IfAnn Annotated (OMap Name (OSet Name)) ())
-> [(Name, OSet Name)]
-> IfAnn Annotated (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')
  where
    payload_to_dec :: (Name, [DTyVarBndr], Maybe DType, [DTySynEqn]) -> DDec
payload_to_dec (name :: Name
name, tvbs :: [DTyVarBndr]
tvbs, m_ki :: Maybe DType
m_ki, eqns :: [DTySynEqn]
eqns) = DTypeFamilyHead -> [DTySynEqn] -> DDec
DClosedTypeFamilyD
                                                (Name
-> [DTyVarBndr]
-> DFamilyResultSig
-> Maybe InjectivityAnn
-> DTypeFamilyHead
DTypeFamilyHead Name
name [DTyVarBndr]
tvbs DFamilyResultSig
sig Maybe InjectivityAnn
forall a. Maybe a
Nothing)
                                                [DTySynEqn]
eqns
      where
        sig :: DFamilyResultSig
sig = DFamilyResultSig
-> (DType -> DFamilyResultSig) -> Maybe DType -> DFamilyResultSig
forall b a. b -> (a -> b) -> Maybe a -> b
maybe DFamilyResultSig
DNoSig DType -> DFamilyResultSig
DKindSig Maybe DType
m_ki

promoteInfixDecl :: Name -> Fixity -> Maybe DDec
promoteInfixDecl :: Name -> Fixity -> Maybe DDec
promoteInfixDecl name :: Name
name fixity :: Fixity
fixity
 | Name -> String
nameBase Name
name String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> String
nameBase Name
promoted_name
   -- If a name and its promoted counterpart are the same (modulo module
   -- prefixes), then there's no need to promote a fixity declaration for
   -- that name, since the existing fixity declaration will cover both
   -- the term- and type-level versions of that name. Names that fall into this
   -- category include data constructor names and infix names.
 = Maybe DDec
forall a. Maybe a
Nothing
 | Bool
otherwise
 = DDec -> Maybe DDec
forall a. a -> Maybe a
Just (DDec -> Maybe DDec) -> DDec -> Maybe DDec
forall a b. (a -> b) -> a -> b
$ DLetDec -> DDec
DLetDec (DLetDec -> DDec) -> DLetDec -> DDec
forall a b. (a -> b) -> a -> b
$ Fixity -> Name -> DLetDec
DInfixD Fixity
fixity Name
promoted_name
 where
  promoted_name :: Name
promoted_name = Name -> Name
promoteValNameLhs Name
name

-- 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 :: Maybe ([DKind], DKind)  -- the promoted type of the RHS (if known)
                                            -- needed to fix #136
                 -> OMap Name DType      -- local type env't
                 -> OMap Name Fixity     -- local fixity env't
                 -> (String, String)     -- let-binding prefixes
                 -> Name                 -- name of the thing being promoted
                 -> ULetDecRHS           -- body of the thing
                 -> PrM ( (Name, [DTyVarBndr], Maybe DKind, [DTySynEqn]) -- "type family"
                        , [DDec]        -- defunctionalization
                        , ALetDecRHS )  -- annotated RHS
promoteLetDecRHS :: Maybe (DCxt, DType)
-> OMap Name DType
-> OMap Name Fixity
-> (String, String)
-> Name
-> LetDecRHS Unannotated
-> PrM
     ((Name, [DTyVarBndr], Maybe DType, [DTySynEqn]), [DDec],
      ALetDecRHS)
promoteLetDecRHS m_rhs_ki :: Maybe (DCxt, DType)
m_rhs_ki type_env :: OMap Name DType
type_env fix_env :: OMap Name Fixity
fix_env prefixes :: (String, String)
prefixes name :: Name
name (UValue exp) = do
  (res_kind :: Maybe DType
res_kind, num_arrows :: Int
num_arrows)
    <- case Maybe (DCxt, DType)
m_rhs_ki of
         Just (arg_kis :: DCxt
arg_kis, res_ki :: DType
res_ki) -> (Maybe DType, Int) -> PrM (Maybe DType, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ( DType -> Maybe DType
forall a. a -> Maybe a
Just (DCxt -> DType
ravelTyFun (DCxt
arg_kis DCxt -> DCxt -> DCxt
forall a. [a] -> [a] -> [a]
++ [DType
res_ki]))
                                          , DCxt -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length DCxt
arg_kis )
         _ |  Just ty :: 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 DType
ki <- DType -> PrM DType
forall (m :: * -> *). MonadFail m => DType -> m DType
promoteType DType
ty
                 (Maybe DType, Int) -> PrM (Maybe DType, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (DType -> Maybe DType
forall a. a -> Maybe a
Just DType
ki, DType -> Int
countArgs DType
ty)
           |  Bool
otherwise
           -> (Maybe DType, Int) -> PrM (Maybe DType, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe DType
forall a. Maybe a
Nothing, 0)
  case Int
num_arrows of
    0 -> do
      [Name]
all_locals <- PrM [Name]
forall (m :: * -> *). MonadReader PrEnv m => m [Name]
allLocals
      let lde_kvs_to_bind :: OSet Name
lde_kvs_to_bind = (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
res_kind
      (exp' :: DType
exp', ann_exp :: ADExp
ann_exp) <- OSet Name -> PrM (DType, ADExp) -> PrM (DType, ADExp)
forall a. OSet Name -> PrM a -> PrM a
forallBind OSet Name
lde_kvs_to_bind (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
      let proName :: Name
proName = (String, String) -> Name -> Name
promoteValNameLhsPrefix (String, String)
prefixes Name
name
          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
          tvbs :: [DTyVarBndr]
tvbs = (Name -> DTyVarBndr) -> [Name] -> [DTyVarBndr]
forall a b. (a -> b) -> [a] -> [b]
map Name -> DTyVarBndr
DPlainTV [Name]
all_locals
      [DDec]
defuns <- Name -> Maybe Fixity -> [DTyVarBndr] -> Maybe DType -> PrM [DDec]
defunctionalize Name
proName Maybe Fixity
m_fixity [DTyVarBndr]
tvbs Maybe DType
res_kind
      ((Name, [DTyVarBndr], Maybe DType, [DTySynEqn]), [DDec],
 ALetDecRHS)
-> PrM
     ((Name, [DTyVarBndr], Maybe DType, [DTySynEqn]), [DDec],
      ALetDecRHS)
forall (m :: * -> *) a. Monad m => a -> m a
return ( ( Name
proName, [DTyVarBndr]
tvbs, Maybe DType
res_kind
               , [Maybe [DTyVarBndr] -> DType -> DType -> DTySynEqn
DTySynEqn Maybe [DTyVarBndr]
forall a. Maybe a
Nothing (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) DType
exp'] )
             , [DDec]
defuns
             , DType -> Int -> ADExp -> ALetDecRHS
AValue (DType -> DCxt -> DType
foldType (Name -> DType
DConT Name
proName) ((Name -> DType) -> [Name] -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map Name -> DType
DVarT [Name]
all_locals))
                      Int
num_arrows ADExp
ann_exp )
    _ -> do
      [Name]
names <- Int -> PrM Name -> PrM [Name]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
num_arrows (String -> PrM Name
forall (m :: * -> *). Quasi m => String -> m Name
newUniqueName "a")
      let pats :: [DPat]
pats    = (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
      Maybe (DCxt, DType)
-> OMap Name DType
-> OMap Name Fixity
-> (String, String)
-> Name
-> LetDecRHS Unannotated
-> PrM
     ((Name, [DTyVarBndr], Maybe DType, [DTySynEqn]), [DDec],
      ALetDecRHS)
promoteLetDecRHS Maybe (DCxt, DType)
m_rhs_ki OMap Name DType
type_env OMap Name Fixity
fix_env (String, String)
prefixes Name
name
                       ([DClause] -> LetDecRHS Unannotated
UFunction [[DPat] -> DExp -> DClause
DClause [DPat]
pats (DExp -> [DExp] -> DExp
foldExp DExp
exp [DExp]
newArgs)])

promoteLetDecRHS m_rhs_ki :: Maybe (DCxt, DType)
m_rhs_ki type_env :: OMap Name DType
type_env fix_env :: OMap Name Fixity
fix_env prefixes :: (String, String)
prefixes name :: Name
name (UFunction clauses) = do
  Int
numArgs <- [DClause] -> PrM Int
forall (m :: * -> *). MonadFail m => [DClause] -> m Int
count_args [DClause]
clauses
  (m_argKs :: [Maybe DType]
m_argKs, m_resK :: Maybe DType
m_resK, ty_num_args :: Int
ty_num_args) <- case Maybe (DCxt, DType)
m_rhs_ki of
    Just (arg_kis :: DCxt
arg_kis, res_ki :: DType
res_ki) -> ([Maybe DType], Maybe DType, Int)
-> PrM ([Maybe DType], Maybe DType, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((DType -> Maybe DType) -> DCxt -> [Maybe DType]
forall a b. (a -> b) -> [a] -> [b]
map DType -> Maybe DType
forall a. a -> Maybe a
Just DCxt
arg_kis, DType -> Maybe DType
forall a. a -> Maybe a
Just DType
res_ki, DCxt -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length DCxt
arg_kis)
    _ |  Just ty :: 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 arrows into TyFun. So, we unravel first to
      -- avoid this behavior. Note the use of ravelTyFun in resultK
      -- to make the return kind work out
      (argKs :: DCxt
argKs, resultK :: DType
resultK) <- DType -> PrM (DCxt, DType)
forall (m :: * -> *). MonadFail m => DType -> m (DCxt, DType)
promoteUnraveled DType
ty
      -- invariant: countArgs ty == length argKs
      ([Maybe DType], Maybe DType, Int)
-> PrM ([Maybe DType], Maybe DType, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((DType -> Maybe DType) -> DCxt -> [Maybe DType]
forall a b. (a -> b) -> [a] -> [b]
map DType -> Maybe DType
forall a. a -> Maybe a
Just DCxt
argKs, DType -> Maybe DType
forall a. a -> Maybe a
Just DType
resultK, DCxt -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length DCxt
argKs)

      |  Bool
otherwise
      -> ([Maybe DType], Maybe DType, Int)
-> PrM ([Maybe DType], Maybe DType, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Maybe DType -> [Maybe DType]
forall a. Int -> a -> [a]
replicate Int
numArgs Maybe DType
forall a. Maybe a
Nothing, Maybe DType
forall a. Maybe a
Nothing, Int
numArgs)
  let proName :: Name
proName  = (String, String) -> Name -> Name
promoteValNameLhsPrefix (String, String)
prefixes Name
name
      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
  [Name]
all_locals <- PrM [Name]
forall (m :: * -> *). MonadReader PrEnv m => m [Name]
allLocals
  let local_tvbs :: [DTyVarBndr]
local_tvbs = (Name -> DTyVarBndr) -> [Name] -> [DTyVarBndr]
forall a b. (a -> b) -> [a] -> [b]
map Name -> DTyVarBndr
DPlainTV [Name]
all_locals
  [Name]
tyvarNames <- (Maybe DType -> PrM Name) -> [Maybe DType] -> PrM [Name]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (PrM Name -> Maybe DType -> PrM Name
forall a b. a -> b -> a
const (PrM Name -> Maybe DType -> PrM Name)
-> PrM Name -> Maybe DType -> PrM Name
forall a b. (a -> b) -> a -> b
$ String -> PrM Name
forall (m :: * -> *). Quasi m => String -> m Name
qNewName "a") [Maybe DType]
m_argKs
  let args :: [DTyVarBndr]
args     = (Name -> Maybe DType -> DTyVarBndr)
-> [Name] -> [Maybe DType] -> [DTyVarBndr]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Name -> Maybe DType -> DTyVarBndr
inferMaybeKindTV [Name]
tyvarNames [Maybe DType]
m_argKs
      all_args :: [DTyVarBndr]
all_args = [DTyVarBndr]
local_tvbs [DTyVarBndr] -> [DTyVarBndr] -> [DTyVarBndr]
forall a. [a] -> [a] -> [a]
++ [DTyVarBndr]
args
  [DDec]
defun_decs <- Name -> Maybe Fixity -> [DTyVarBndr] -> Maybe DType -> PrM [DDec]
defunctionalize Name
proName Maybe Fixity
m_fixity [DTyVarBndr]
all_args Maybe DType
m_resK
  [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
  let lde_kvs_to_bind :: OSet Name
lde_kvs_to_bind = (Maybe DType -> OSet Name) -> [Maybe DType] -> 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]
m_argKs OSet Name -> OSet Name -> OSet Name
forall a. Semigroup a => a -> a -> a
<> (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
m_resK
  (eqns :: [DTySynEqn]
eqns, ann_clauses :: [ADClause]
ann_clauses) <- OSet Name
-> PrM ([DTySynEqn], [ADClause]) -> PrM ([DTySynEqn], [ADClause])
forall a. OSet Name -> PrM a -> PrM a
forallBind OSet Name
lde_kvs_to_bind (PrM ([DTySynEqn], [ADClause]) -> PrM ([DTySynEqn], [ADClause]))
-> PrM ([DTySynEqn], [ADClause]) -> PrM ([DTySynEqn], [ADClause])
forall a b. (a -> b) -> a -> b
$
                         (DClause -> PrM (DTySynEqn, ADClause))
-> [DClause] -> PrM ([DTySynEqn], [ADClause])
forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM (Name -> DClause -> PrM (DTySynEqn, ADClause)
promoteClause Name
proName) [DClause]
expClauses
  DType
prom_fun <- Name -> PrM DType
lookupVarE Name
name
  ((Name, [DTyVarBndr], Maybe DType, [DTySynEqn]), [DDec],
 ALetDecRHS)
-> PrM
     ((Name, [DTyVarBndr], Maybe DType, [DTySynEqn]), [DDec],
      ALetDecRHS)
forall (m :: * -> *) a. Monad m => a -> m a
return ( (Name
proName, [DTyVarBndr]
all_args, Maybe DType
m_resK, [DTySynEqn]
eqns)
         , [DDec]
defun_decs
         , DType -> Int -> [ADClause] -> ALetDecRHS
AFunction DType
prom_fun Int
ty_num_args [ADClause]
ann_clauses )

  where
    etaContractOrExpand :: Int -> Int -> DClause -> PrM DClause
    etaContractOrExpand :: Int -> Int -> DClause -> PrM DClause
etaContractOrExpand ty_num_args :: Int
ty_num_args clause_num_args :: Int
clause_num_args (DClause pats :: [DPat]
pats exp :: DExp
exp)
      | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= 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 "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 (clausePats :: [DPat]
clausePats, lamPats :: [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] -> m Int
count_args (DClause pats :: [DPat]
pats _ : _) = Int -> m Int
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> m Int) -> Int -> m Int
forall a b. (a -> b) -> a -> b
$ [DPat] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [DPat]
pats
    count_args _ = String -> m Int
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> m Int) -> String -> m Int
forall a b. (a -> b) -> a -> b
$ "Impossible! A function without clauses."

promoteClause :: Name -> DClause -> PrM (DTySynEqn, ADClause)
promoteClause :: Name -> DClause -> PrM (DTySynEqn, ADClause)
promoteClause proName :: Name
proName (DClause pats :: [DPat]
pats exp :: DExp
exp) = do
  -- promoting the patterns creates variable bindings. These are passed
  -- to the function promoted the RHS
  ((types :: DCxt
types, pats' :: [ADPat]
pats'), prom_pat_infos :: 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
  (ty :: DType
ty, ann_exp :: 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
  [Name]
all_locals <- PrM [Name]
forall (m :: * -> *). MonadReader PrEnv m => m [Name]
allLocals   -- these are bound *outside* of this clause
  (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 (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 DCxt -> DCxt -> DCxt
forall a. [a] -> [a] -> [a]
++ DCxt
types) DType
ty
         , VarPromotions -> [ADPat] -> ADExp -> ADClause
ADClause VarPromotions
new_vars [ADPat]
pats' ADExp
ann_exp )

promoteMatch :: Name -> DMatch -> PrM (DTySynEqn, ADMatch)
promoteMatch :: Name -> DMatch -> PrM (DTySynEqn, ADMatch)
promoteMatch caseTFName :: Name
caseTFName (DMatch pat :: DPat
pat exp :: DExp
exp) = do
  -- promoting the patterns creates variable bindings. These are passed
  -- to the function promoted the RHS
  ((ty :: DType
ty, pat' :: ADPat
pat'), prom_pat_infos :: 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
  (rhs :: DType
rhs, ann_exp :: 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
  [Name]
all_locals <- PrM [Name]
forall (m :: * -> *). MonadReader PrEnv m => m [Name]
allLocals
  (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 -> DCxt -> DType
foldType (Name -> DType
DConT Name
caseTFName) (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 DCxt -> DCxt -> DCxt
forall a. [a] -> [a] -> [a]
++ [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) = (, 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
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
name pats :: [DPat]
pats) = do
  (types :: DCxt
types, pats' :: [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 n :: Name
n
      | Just deg :: Int
deg <- Name -> Maybe Int
unboxedTupleNameDegree_maybe Name
n = Int -> Name
tupleDataName Int
deg
      | Bool
otherwise                                  = Name
n
promotePat (DTildeP pat :: DPat
pat) = do
  String -> QWithAux PromDPatInfos PrM ()
forall (q :: * -> *). Quasi q => String -> q ()
qReportWarning "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 pat :: DPat
pat) = do
  String -> QWithAux PromDPatInfos PrM ()
forall (q :: * -> *). Quasi q => String -> q ()
qReportWarning "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 pat :: DPat
pat ty :: 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
  (promoted :: DType
promoted, pat' :: 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 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
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
name) = (DType, ADExp) -> PrM (DType, ADExp)
forall (m :: * -> *) a. Monad m => a -> m a
return ((DType, ADExp) -> PrM (DType, ADExp))
-> (DType, ADExp) -> PrM (DType, ADExp)
forall a b. (a -> b) -> a -> b
$ (Name -> DType
promoteValRhs Name
name, Name -> ADExp
ADConE Name
name)
promoteExp (DLitE lit :: 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 exp1 :: DExp
exp1 exp2 :: DExp
exp2) = do
  (exp1' :: DType
exp1', ann_exp1 :: ADExp
ann_exp1) <- DExp -> PrM (DType, ADExp)
promoteExp DExp
exp1
  (exp2' :: DType
exp2', ann_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 exp :: DExp
exp _) = do
  String -> PrM ()
forall (q :: * -> *). Quasi q => String -> q ()
qReportWarning "Visible type applications are ignored by `singletons`."
  DExp -> PrM (DType, ADExp)
promoteExp DExp
exp
promoteExp (DLamE names :: [Name]
names exp :: DExp
exp) = do
  Name
lambdaName <- String -> PrM Name
forall (m :: * -> *). Quasi m => String -> m Name
newUniqueName "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
  (rhs :: DType
rhs, ann_exp :: 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]
tyFamLamTypes <- (Name -> PrM Name) -> [Name] -> PrM [Name]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (PrM Name -> Name -> PrM Name
forall a b. a -> b -> a
const (PrM Name -> Name -> PrM Name) -> PrM Name -> Name -> PrM Name
forall a b. (a -> b) -> a -> b
$ String -> PrM Name
forall (m :: * -> *). Quasi m => String -> m Name
qNewName "t") [Name]
names
  [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]
tyFamLamTypes
      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_locals [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
tyNames))
                                          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 -> [DTyVarBndr] -> Maybe DType -> PrM [DDec]
defunctionalize Name
lambdaName Maybe Fixity
forall a. Maybe a
Nothing [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 (Name -> Int -> Name
promoteTySym Name
lambdaName 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 exp :: DExp
exp matches :: [DMatch]
matches) = do
  Name
caseTFName <- String -> PrM Name
forall (m :: * -> *). Quasi m => String -> m Name
newUniqueName "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)
  (exp' :: DType
exp', ann_exp :: ADExp
ann_exp)     <- DExp -> PrM (DType, ADExp)
promoteExp DExp
exp
  (eqns :: [DTySynEqn]
eqns, ann_matches :: [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 (Name -> DMatch -> PrM (DTySynEqn, ADMatch)
promoteMatch Name
caseTFName) [DMatch]
matches
  Name
tyvarName  <- String -> PrM Name
forall (m :: * -> *). Quasi m => String -> m Name
qNewName "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 decs :: [DLetDec]
decs exp :: DExp
exp) = do
  Int
unique <- PrM Int
forall (q :: * -> *). DsMonad q => q Int
qNewUnique
  let letPrefixes :: (String, String)
letPrefixes = String -> String -> Int -> (String, String)
uniquePrefixes "Let" "<<<" Int
unique
  (binds :: [LetBind]
binds, ann_env :: ALetDecEnv
ann_env) <- (String, String) -> [DLetDec] -> PrM ([LetBind], ALetDecEnv)
promoteLetDecs (String, String)
letPrefixes [DLetDec]
decs
  (exp' :: DType
exp', ann_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 exp :: DExp
exp ty :: DType
ty) = do
  (exp' :: DType
exp', ann_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 _) = String -> PrM (DType, ADExp)
forall (m :: * -> *) a. MonadFail m => String -> m a
fail ("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 n :: Integer
n)
  | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= 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 (Integer -> TyLit
NumTyLit Integer
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 (Integer -> TyLit
NumTyLit (-Integer
n))))
promoteLitExp (StringL str :: 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
lit =
  String -> q DType
forall (m :: * -> *) a. MonadFail m => String -> m a
fail ("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 n :: Integer
n)
  | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= 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 (Integer -> TyLit
NumTyLit Integer
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
$ "Negative literal patterns are not allowed,\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
           "because literal patterns are promoted to natural numbers."
promoteLitPat (StringL str :: 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
lit =
  String -> m DType
forall (m :: * -> *) a. MonadFail m => String -> m a
fail ("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 _ _ cons :: [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 :: * -> *). Quasi q => DType -> [DCon] -> q [DDec]
mkEqTypeInstance DType
kind [DCon]
cons
  [DDec] -> PrM ()
forall (m :: * -> *). MonadWriter [DDec] m => [DDec] -> m ()
emitDecs [DDec]
inst_decs