{-# LANGUAGE LambdaCase #-}

{- Data/Singletons/TH/Util.hs

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

This file contains helper functions internal to the singletons-th package.
Users of the package should not need to consult this file.
-}

module Data.Singletons.TH.Util where

import Prelude hiding ( exp, foldl, concat, mapM, any, pred )
import Language.Haskell.TH ( pprint )
import Language.Haskell.TH.Syntax hiding ( lift )
import Language.Haskell.TH.Desugar
import qualified Language.Haskell.TH.Desugar.Subst.Capturing as SC
import Data.Char
import Control.Monad ( liftM, unless, when )
import Control.Monad.Except ( ExceptT, runExceptT, MonadError(..) )
import Control.Monad.IO.Class ( MonadIO )
import Control.Monad.Reader ( MonadReader(..), Reader, ReaderT(..) )
import Control.Monad.Trans ( MonadTrans )
import Control.Monad.Writer ( MonadWriter(..), WriterT(..), execWriterT )
import qualified Data.Map as Map
import Data.Map ( Map )
import Data.Foldable
import Data.Functor.Identity
import Data.Traversable
import Data.Generics
import Data.Maybe

import Data.Singletons.TH.Syntax.LocalVar

-- like reportWarning, but generalized to any Quasi
qReportWarning :: Quasi q => String -> q ()
qReportWarning :: forall (q :: * -> *). Quasi q => String -> q ()
qReportWarning = Bool -> String -> q ()
forall (m :: * -> *). Quasi m => Bool -> String -> m ()
qReport Bool
False

-- like reportError, but generalized to any Quasi
qReportError :: Quasi q => String -> q ()
qReportError :: forall (q :: * -> *). Quasi q => String -> q ()
qReportError = Bool -> String -> q ()
forall (m :: * -> *). Quasi m => Bool -> String -> m ()
qReport Bool
True

-- | Generate a new Unique
qNewUnique :: DsMonad q => q Uniq
qNewUnique :: forall (q :: * -> *). DsMonad q => q Uniq
qNewUnique = do
  Name _ flav <- String -> q Name
forall (m :: * -> *). Quasi m => String -> m Name
qNewName String
"x"
  case flav of
    NameU Uniq
n -> Uniq -> q Uniq
forall a. a -> q a
forall (m :: * -> *) a. Monad m => a -> m a
return Uniq
n
    NameFlavour
_       -> String -> q Uniq
forall a. HasCallStack => String -> a
error String
"Internal error: `qNewName` didn't return a NameU"

checkForRep :: Quasi q => [Name] -> q ()
checkForRep :: forall (q :: * -> *). Quasi q => [Name] -> q ()
checkForRep [Name]
names =
  Bool -> q () -> q ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ((Name -> Bool) -> [Name] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"Rep") (String -> Bool) -> (Name -> String) -> Name -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> String
nameBase) [Name]
names)
    (String -> q ()
forall a. String -> q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> q ()) -> String -> q ()
forall a b. (a -> b) -> a -> b
$ String
"A data type named <<Rep>> is a special case.\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
            String
"Promoting it will not work as expected.\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
            String
"Please choose another name for your data type.")

checkForRepInDecls :: Quasi q => [DDec] -> q ()
checkForRepInDecls :: forall (q :: * -> *). Quasi q => [DDec] -> q ()
checkForRepInDecls [DDec]
decls =
  [Name] -> q ()
forall (q :: * -> *). Quasi q => [Name] -> q ()
checkForRep ([DDec] -> [Name]
forall a. Data a => a -> [Name]
allNamesIn [DDec]
decls)

tysOfConFields :: DConFields -> [DType]
tysOfConFields :: DConFields -> [DType]
tysOfConFields (DNormalC Bool
_ [DBangType]
stys) = (DBangType -> DType) -> [DBangType] -> [DType]
forall a b. (a -> b) -> [a] -> [b]
map DBangType -> DType
forall a b. (a, b) -> b
snd [DBangType]
stys
tysOfConFields (DRecC [DVarBangType]
vstys)   = (DVarBangType -> DType) -> [DVarBangType] -> [DType]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
_,Bang
_,DType
ty) -> DType
ty) [DVarBangType]
vstys

recSelsOfConFields :: DConFields -> [Name]
recSelsOfConFields :: DConFields -> [Name]
recSelsOfConFields DNormalC{}    = []
recSelsOfConFields (DRecC [DVarBangType]
vstys) = (DVarBangType -> Name) -> [DVarBangType] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
n,Bang
_,DType
_) -> Name
n) [DVarBangType]
vstys

-- Extract a data constructor's name and the number of arguments it accepts.
extractNameArgs :: DCon -> (Name, Int)
extractNameArgs :: DCon -> (Name, Int)
extractNameArgs (DCon [DTyVarBndrSpec]
_ [DType]
_ Name
n DConFields
fields DType
_) = (Name
n, [DType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (DConFields -> [DType]
tysOfConFields DConFields
fields))

-- Extract a data constructor's name.
extractName :: DCon -> Name
extractName :: DCon -> Name
extractName (DCon [DTyVarBndrSpec]
_ [DType]
_ Name
n DConFields
_ DType
_) = Name
n

-- Extract the names of a data constructor's record selectors.
extractRecSelNames :: DCon -> [Name]
extractRecSelNames :: DCon -> [Name]
extractRecSelNames (DCon [DTyVarBndrSpec]
_ [DType]
_ Name
_ DConFields
fields DType
_) = DConFields -> [Name]
recSelsOfConFields DConFields
fields

-- | is a valid Haskell infix data constructor (i.e., does it begin with a colon?)
isInfixDataCon :: String -> Bool
isInfixDataCon :: String -> Bool
isInfixDataCon (Char
':':String
_) = Bool
True
isInfixDataCon String
_       = Bool
False

-- | Is an identifier a legal data constructor name in Haskell? That is, is its
-- first character an uppercase letter (prefix) or a colon (infix)?
isDataConName :: Name -> Bool
isDataConName :: Name -> Bool
isDataConName Name
n = let first :: Char
first = String -> Char
headNameStr (Name -> String
nameBase Name
n) in Char -> Bool
isUpper Char
first Bool -> Bool -> Bool
|| Char
first Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
':'

-- | Is an identifier uppercase?
--
-- Note that this will always return 'False' for infix names, since the concept
-- of upper- and lower-case doesn't make sense for non-alphabetic characters.
-- If you want to check if a name is legal as a data constructor, use the
-- 'isDataConName' function.
isUpcase :: Name -> Bool
isUpcase :: Name -> Bool
isUpcase Name
n = let first :: Char
first = String -> Char
headNameStr (Name -> String
nameBase Name
n) in Char -> Bool
isUpper Char
first

-- Make an identifier uppercase. If the identifier is infix, this acts as the
-- identity function.
upcase :: Name -> Name
upcase :: Name -> Name
upcase = String -> Name
mkName (String -> Name) -> (Name -> String) -> Name -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, String) -> Name -> String
toUpcaseStr (String, String)
noPrefix

-- make an identifier uppercase and return it as a String
toUpcaseStr :: (String, String)  -- (alpha, symb) prefixes to prepend
            -> Name -> String
toUpcaseStr :: (String, String) -> Name -> String
toUpcaseStr (String
alpha, String
symb) Name
n
  | Char -> Bool
isHsLetter Char
first
  = String
upcase_alpha

  | Bool
otherwise
  = String
upcase_symb

  where
    str :: String
str   = Name -> String
nameBase Name
n
    first :: Char
first = String -> Char
headNameStr String
str

    upcase_alpha :: String
upcase_alpha = String
alpha String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Char -> Char
toUpper Char
first) Char -> String -> String
forall a. a -> [a] -> [a]
: String -> String
tailNameStr String
str
    upcase_symb :: String
upcase_symb = String
symb String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
str

noPrefix :: (String, String)
noPrefix :: (String, String)
noPrefix = (String
"", String
"")

-- Put an uppercase prefix on a constructor name. Takes two prefixes:
-- one for identifiers and one for symbols.
--
-- This is different from 'prefixName' in that infix constructor names always
-- start with a colon, so we must insert the prefix after the colon in order
-- for the new name to be syntactically valid.
prefixConName :: String -> String -> Name -> Name
prefixConName :: String -> String -> Name -> Name
prefixConName String
pre String
tyPre Name
n = case (Name -> String
nameBase Name
n) of
    (Char
':' : String
rest) -> String -> Name
mkName (Char
':' Char -> String -> String
forall a. a -> [a] -> [a]
: String
tyPre String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
rest)
    String
alpha -> String -> Name
mkName (String
pre String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
alpha)

-- Put a prefix on a name. Takes two prefixes: one for identifiers
-- and one for symbols.
prefixName :: String -> String -> Name -> Name
prefixName :: String -> String -> Name -> Name
prefixName String
pre String
tyPre Name
n =
  let str :: String
str = Name -> String
nameBase Name
n
      first :: Char
first = String -> Char
headNameStr String
str in
    if Char -> Bool
isHsLetter Char
first
     then String -> Name
mkName (String
pre String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
str)
     else String -> Name
mkName (String
tyPre String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
str)

-- Put a suffix on a name. Takes two suffixes: one for identifiers
-- and one for symbols.
suffixName :: String -> String -> Name -> Name
suffixName :: String -> String -> Name -> Name
suffixName String
ident String
symb Name
n =
  let str :: String
str = Name -> String
nameBase Name
n
      first :: Char
first = String -> Char
headNameStr String
str in
  if Char -> Bool
isHsLetter Char
first
  then String -> Name
mkName (String
str String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ident)
  else String -> Name
mkName (String
str String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
symb)

-- Return the first character in a Name's string (i.e., nameBase).
-- Precondition: the string is non-empty.
headNameStr :: String -> Char
headNameStr :: String -> Char
headNameStr String
str =
  case String
str of
    (Char
c:String
_) -> Char
c
    [] -> String -> Char
forall a. HasCallStack => String -> a
error String
"headNameStr: Expected non-empty string"

-- Drop the first character in a Name's string (i.e., nameBase).
-- Precondition: the string is non-empty.
tailNameStr :: String -> String
tailNameStr :: String -> String
tailNameStr String
str =
  case String
str of
    (Char
_:String
cs) -> String
cs
    [] -> String -> String
forall a. HasCallStack => String -> a
error String
"tailNameStr: Expected non-empty string"

-- convert a number into both alphanumeric and symoblic forms
uniquePrefixes :: String   -- alphanumeric prefix
               -> String   -- symbolic prefix
               -> Uniq
               -> (String, String)  -- (alphanum, symbolic)
uniquePrefixes :: String -> String -> Uniq -> (String, String)
uniquePrefixes String
alpha String
symb Uniq
n = (String
alpha String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
n_str, String
symb String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
convert String
n_str)
  where
    n_str :: String
n_str = Uniq -> String
forall a. Show a => a -> String
show Uniq
n

    convert :: String -> String
convert [] = []
    convert (Char
d : String
ds) =
      let d' :: Char
d' = case Char
d of
                 Char
'0' -> Char
'!'
                 Char
'1' -> Char
'#'
                 Char
'2' -> Char
'$'
                 Char
'3' -> Char
'%'
                 Char
'4' -> Char
'&'
                 Char
'5' -> Char
'*'
                 Char
'6' -> Char
'+'
                 Char
'7' -> Char
'.'
                 Char
'8' -> Char
'/'
                 Char
'9' -> Char
'>'
                 Char
_   -> String -> Char
forall a. HasCallStack => String -> a
error String
"non-digit in show #"
      in Char
d' Char -> String -> String
forall a. a -> [a] -> [a]
: String -> String
convert String
ds

-- extract the kind from a TyVarBndr
extractTvbKind :: DTyVarBndr flag -> Maybe DKind
extractTvbKind :: forall flag. DTyVarBndr flag -> Maybe DType
extractTvbKind (DPlainTV Name
_ flag
_)    = Maybe DType
forall a. Maybe a
Nothing
extractTvbKind (DKindedTV Name
_ flag
_ DType
k) = DType -> Maybe DType
forall a. a -> Maybe a
Just DType
k

-- extract the name from a TyVarBndr.
extractTvbName :: DTyVarBndr flag -> Name
extractTvbName :: forall flag. DTyVarBndr flag -> Name
extractTvbName (DPlainTV Name
n flag
_)    = Name
n
extractTvbName (DKindedTV Name
n flag
_ DType
_) = Name
n

-- extract the flag from a TyVarBndr.
extractTvbFlag :: DTyVarBndr flag -> flag
extractTvbFlag :: forall flag. DTyVarBndr flag -> flag
extractTvbFlag (DPlainTV Name
_ flag
f)    = flag
f
extractTvbFlag (DKindedTV Name
_ flag
f DType
_) = flag
f

tvbToType :: DTyVarBndr flag -> DType
tvbToType :: forall flag. DTyVarBndr flag -> DType
tvbToType = Name -> DType
DVarT (Name -> DType)
-> (DTyVarBndr flag -> Name) -> DTyVarBndr flag -> DType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DTyVarBndr flag -> Name
forall flag. DTyVarBndr flag -> Name
extractTvbName

-- If a type variable binder lacks an explicit kind, pick a default kind of
-- Type. Otherwise, leave the binder alone.
defaultTvbToTypeKind :: DTyVarBndr flag -> DTyVarBndr flag
defaultTvbToTypeKind :: forall flag. DTyVarBndr flag -> DTyVarBndr flag
defaultTvbToTypeKind (DPlainTV Name
tvname flag
f) = Name -> flag -> DType -> DTyVarBndr flag
forall flag. Name -> flag -> DType -> DTyVarBndr flag
DKindedTV Name
tvname flag
f (DType -> DTyVarBndr flag) -> DType -> DTyVarBndr flag
forall a b. (a -> b) -> a -> b
$ Name -> DType
DConT Name
typeKindName
defaultTvbToTypeKind DTyVarBndr flag
tvb                 = DTyVarBndr flag
tvb

-- If @Nothing@, return @Type@. If @Just k@, return @k@.
defaultMaybeToTypeKind :: Maybe DKind -> DKind
defaultMaybeToTypeKind :: Maybe DType -> DType
defaultMaybeToTypeKind (Just DType
k) = DType
k
defaultMaybeToTypeKind Maybe DType
Nothing  = Name -> DType
DConT Name
typeKindName

inferMaybeKindTV :: Name -> Maybe DKind -> DTyVarBndrUnit
inferMaybeKindTV :: Name -> Maybe DType -> DTyVarBndrUnit
inferMaybeKindTV Name
n Maybe DType
Nothing  = Name -> () -> DTyVarBndrUnit
forall flag. Name -> flag -> DTyVarBndr flag
DPlainTV Name
n ()
inferMaybeKindTV Name
n (Just DType
k) = Name -> () -> DType -> DTyVarBndrUnit
forall flag. Name -> flag -> DType -> DTyVarBndr flag
DKindedTV Name
n () DType
k

resultSigToMaybeKind :: DFamilyResultSig -> Maybe DKind
resultSigToMaybeKind :: DFamilyResultSig -> Maybe DType
resultSigToMaybeKind DFamilyResultSig
DNoSig                        = Maybe DType
forall a. Maybe a
Nothing
resultSigToMaybeKind (DKindSig DType
k)                  = DType -> Maybe DType
forall a. a -> Maybe a
Just DType
k
resultSigToMaybeKind (DTyVarSig DPlainTV{})        = Maybe DType
forall a. Maybe a
Nothing
resultSigToMaybeKind (DTyVarSig (DKindedTV Name
_ ()
_ DType
k)) = DType -> Maybe DType
forall a. a -> Maybe a
Just DType
k

maybeKindToResultSig :: Maybe DKind -> DFamilyResultSig
maybeKindToResultSig :: Maybe DType -> DFamilyResultSig
maybeKindToResultSig = DFamilyResultSig
-> (DType -> DFamilyResultSig) -> Maybe DType -> DFamilyResultSig
forall b a. b -> (a -> b) -> Maybe a -> b
maybe DFamilyResultSig
DNoSig DType -> DFamilyResultSig
DKindSig

maybeSigT :: DType -> Maybe DKind -> DType
maybeSigT :: DType -> Maybe DType -> DType
maybeSigT DType
ty Maybe DType
Nothing   = DType
ty
maybeSigT DType
ty (Just DType
ki) = DType
ty DType -> DType -> DType
`DSigT` DType
ki

-- | Convert a list of 'DTyVarBndrSpec's to a list of 'DTyVarBndrVis'es. Type
-- variable binders with a 'SpecifiedSpec' are converted to 'BndrInvis', and
-- type variable binders with an 'InferredSpec' are dropped entirely.
--
-- As an example, if you have this list of 'DTyVarBndrSpec's:
--
-- @
-- forall a {b} c {d e} f. <...>
-- @
--
-- The corresponding list of 'DTyVarBndrVis'es would be:
--
-- @
-- \@a \@b \@f
-- @
--
-- Note that note of @b@, @d@, or @e@ appear in the list.
--
-- See also 'dtvbForAllTyFlagsToBndrVis', which takes a list of @'DTyVarBndr'
-- 'ForAllTyFlag'@ as arguments instead of a list of 'DTyVarBndrSpec's. Note
-- that @'dtvbSpecsToBndrVis' . 'dtvbForAllTyFlagsToSpecs'@ is /not/ the same
-- thing as 'dtvbForAllTyFlagsToBndrVis'. This is because 'dtvbSpecsToBndrVis'
-- only produces 'BndrInvis' binders as output, whereas
-- 'dtvbForAllTyFlagsToBndrVis' can produce both 'BndrReq' and 'BndrInvis'
-- binders.
dtvbSpecsToBndrVis :: [DTyVarBndrSpec] -> [DTyVarBndrVis]
dtvbSpecsToBndrVis :: [DTyVarBndrSpec] -> [DTyVarBndrVis]
dtvbSpecsToBndrVis = (DTyVarBndrSpec -> Maybe DTyVarBndrVis)
-> [DTyVarBndrSpec] -> [DTyVarBndrVis]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ((Specificity -> Maybe BndrVis)
-> DTyVarBndrSpec -> Maybe DTyVarBndrVis
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> DTyVarBndr a -> f (DTyVarBndr b)
traverse Specificity -> Maybe BndrVis
specificityToBndrVis)
  where
    specificityToBndrVis :: Specificity -> Maybe BndrVis
    specificityToBndrVis :: Specificity -> Maybe BndrVis
specificityToBndrVis Specificity
SpecifiedSpec = BndrVis -> Maybe BndrVis
forall a. a -> Maybe a
Just BndrVis
BndrInvis
    specificityToBndrVis Specificity
InferredSpec  = Maybe BndrVis
forall a. Maybe a
Nothing

-- Reconstruct a vanilla function type from its individual type variable
-- binders, constraints, argument types, and result type. (See
-- Note [Vanilla-type validity checking during promotion] in
-- Data.Singletons.TH.Promote.Type for what "vanilla" means.)
ravelVanillaDType :: [DTyVarBndrSpec] -> DCxt -> [DType] -> DType -> DType
ravelVanillaDType :: [DTyVarBndrSpec] -> [DType] -> [DType] -> DType -> DType
ravelVanillaDType [DTyVarBndrSpec]
tvbs [DType]
ctxt [DType]
args DType
res =
  [DTyVarBndrSpec]
-> ([DTyVarBndrSpec] -> DType -> DType) -> DType -> DType
forall a b. [a] -> ([a] -> b -> b) -> b -> b
ifNonEmpty [DTyVarBndrSpec]
tvbs (DForallTelescope -> DType -> DType
DForallT (DForallTelescope -> DType -> DType)
-> ([DTyVarBndrSpec] -> DForallTelescope)
-> [DTyVarBndrSpec]
-> DType
-> DType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [DTyVarBndrSpec] -> DForallTelescope
DForallInvis) (DType -> DType) -> DType -> DType
forall a b. (a -> b) -> a -> b
$
  [DType] -> ([DType] -> DType -> DType) -> DType -> DType
forall a b. [a] -> ([a] -> b -> b) -> b -> b
ifNonEmpty [DType]
ctxt [DType] -> DType -> DType
DConstrainedT (DType -> DType) -> DType -> DType
forall a b. (a -> b) -> a -> b
$
  [DType] -> DType
go [DType]
args
  where
    ifNonEmpty :: [a] -> ([a] -> b -> b) -> b -> b
    ifNonEmpty :: forall a b. [a] -> ([a] -> b -> b) -> b -> b
ifNonEmpty [] [a] -> b -> b
_ b
z = b
z
    ifNonEmpty [a]
l  [a] -> b -> b
f b
z = [a] -> b -> b
f [a]
l b
z

    go :: [DType] -> DType
    go :: [DType] -> DType
go []    = DType
res
    go (DType
h:[DType]
t) = DType -> DType -> DType
DAppT (DType -> DType -> DType
DAppT DType
DArrowT DType
h) ([DType] -> DType
go [DType]
t)

-- Decompose a vanilla function type into its type variables, its context, its
-- argument types, and its result type. (See
-- Note [Vanilla-type validity checking during promotion] in
-- Data.Singletons.TH.Promote.Type for what "vanilla" means.)
-- If a non-vanilla construct is encountered while decomposing the function
-- type, an error is thrown monadically.
--
-- This should be contrasted with the 'unravelDType' function from
-- @th-desugar@, which supports the full gamut of function types. @singletons-th@
-- only supports a subset of these types, which is why this function is used
-- to decompose them instead.
unravelVanillaDType :: forall m. MonadFail m
                    => DType -> m ([DTyVarBndrSpec], DCxt, [DType], DType)
unravelVanillaDType :: forall (m :: * -> *).
MonadFail m =>
DType -> m ([DTyVarBndrSpec], [DType], [DType], DType)
unravelVanillaDType DType
ty =
  case DType -> Either String ([DTyVarBndrSpec], [DType], [DType], DType)
unravelVanillaDType_either DType
ty of
    Left String
err      -> String -> m ([DTyVarBndrSpec], [DType], [DType], DType)
forall a. String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
err
    Right ([DTyVarBndrSpec], [DType], [DType], DType)
payload -> ([DTyVarBndrSpec], [DType], [DType], DType)
-> m ([DTyVarBndrSpec], [DType], [DType], DType)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([DTyVarBndrSpec], [DType], [DType], DType)
payload

-- Ensures that a 'DType' is a vanilla type. (See
-- Note [Vanilla-type validity checking during promotion] in
-- Data.Singletons.TH.Promote.Type for what "vanilla" means.)
--
-- The only monadic thing that this function can do is 'fail', which it does
-- if a non-vanilla construct is encountered.
checkVanillaDType :: forall m. MonadFail m => DType -> m ()
checkVanillaDType :: forall (m :: * -> *). MonadFail m => DType -> m ()
checkVanillaDType DType
ty =
  case DType -> Either String ([DTyVarBndrSpec], [DType], [DType], DType)
unravelVanillaDType_either DType
ty of
    Left String
err -> String -> m ()
forall a. String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
err
    Right ([DTyVarBndrSpec], [DType], [DType], DType)
_  -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- The workhorse that powers unravelVanillaDType and checkVanillaDType.
-- Returns @Right payload@ upon success, and @Left error_msg@ upon failure.
unravelVanillaDType_either ::
  DType -> Either String ([DTyVarBndrSpec], DCxt, [DType], DType)
unravelVanillaDType_either :: DType -> Either String ([DTyVarBndrSpec], [DType], [DType], DType)
unravelVanillaDType_either DType
ty =
  Identity
  (Either String ([DTyVarBndrSpec], [DType], [DType], DType))
-> Either String ([DTyVarBndrSpec], [DType], [DType], DType)
forall a. Identity a -> a
runIdentity (Identity
   (Either String ([DTyVarBndrSpec], [DType], [DType], DType))
 -> Either String ([DTyVarBndrSpec], [DType], [DType], DType))
-> Identity
     (Either String ([DTyVarBndrSpec], [DType], [DType], DType))
-> Either String ([DTyVarBndrSpec], [DType], [DType], DType)
forall a b. (a -> b) -> a -> b
$ (Reader
   Bool (Either String ([DTyVarBndrSpec], [DType], [DType], DType))
 -> Bool
 -> Identity
      (Either String ([DTyVarBndrSpec], [DType], [DType], DType)))
-> Bool
-> Reader
     Bool (Either String ([DTyVarBndrSpec], [DType], [DType], DType))
-> Identity
     (Either String ([DTyVarBndrSpec], [DType], [DType], DType))
forall a b c. (a -> b -> c) -> b -> a -> c
flip Reader
  Bool (Either String ([DTyVarBndrSpec], [DType], [DType], DType))
-> Bool
-> Identity
     (Either String ([DTyVarBndrSpec], [DType], [DType], DType))
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT Bool
True (Reader
   Bool (Either String ([DTyVarBndrSpec], [DType], [DType], DType))
 -> Identity
      (Either String ([DTyVarBndrSpec], [DType], [DType], DType)))
-> Reader
     Bool (Either String ([DTyVarBndrSpec], [DType], [DType], DType))
-> Identity
     (Either String ([DTyVarBndrSpec], [DType], [DType], DType))
forall a b. (a -> b) -> a -> b
$ ExceptT
  String (Reader Bool) ([DTyVarBndrSpec], [DType], [DType], DType)
-> Reader
     Bool (Either String ([DTyVarBndrSpec], [DType], [DType], DType))
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT
   String (Reader Bool) ([DTyVarBndrSpec], [DType], [DType], DType)
 -> Reader
      Bool (Either String ([DTyVarBndrSpec], [DType], [DType], DType)))
-> ExceptT
     String (Reader Bool) ([DTyVarBndrSpec], [DType], [DType], DType)
-> Reader
     Bool (Either String ([DTyVarBndrSpec], [DType], [DType], DType))
forall a b. (a -> b) -> a -> b
$ UnravelM ([DTyVarBndrSpec], [DType], [DType], DType)
-> ExceptT
     String (Reader Bool) ([DTyVarBndrSpec], [DType], [DType], DType)
forall a. UnravelM a -> ExceptT String (Reader Bool) a
runUnravelM (UnravelM ([DTyVarBndrSpec], [DType], [DType], DType)
 -> ExceptT
      String (Reader Bool) ([DTyVarBndrSpec], [DType], [DType], DType))
-> UnravelM ([DTyVarBndrSpec], [DType], [DType], DType)
-> ExceptT
     String (Reader Bool) ([DTyVarBndrSpec], [DType], [DType], DType)
forall a b. (a -> b) -> a -> b
$ DType -> UnravelM ([DTyVarBndrSpec], [DType], [DType], DType)
go_ty DType
ty
  where
    go_ty :: DType -> UnravelM ([DTyVarBndrSpec], DCxt, [DType], DType)
    go_ty :: DType -> UnravelM ([DTyVarBndrSpec], [DType], [DType], DType)
go_ty DType
typ = do
      let (DFunArgs
args1, DType
res) = DType -> (DFunArgs, DType)
unravelDType DType
typ
      (args2, tvbs) <- DFunArgs -> UnravelM (DFunArgs, [DTyVarBndrSpec])
take_tvbs  DFunArgs
args1
      (args3, ctxt) <- take_ctxt  args2
      anons         <- take_anons args3
      pure (tvbs, ctxt, anons, res)

    -- Process a type in a higher-order position (e.g., the @forall a. a -> a@ in
    -- @(forall a. a -> a) -> b -> b@). This is only done to check for the
    -- presence of higher-rank foralls or constraints, which are not permitted
    -- in vanilla types.
    go_higher_order_ty :: DType -> UnravelM ()
    go_higher_order_ty :: DType -> UnravelM ()
go_higher_order_ty DType
typ = () ()
-> UnravelM ([DTyVarBndrSpec], [DType], [DType], DType)
-> UnravelM ()
forall a b. a -> UnravelM b -> UnravelM a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ (Bool -> Bool)
-> UnravelM ([DTyVarBndrSpec], [DType], [DType], DType)
-> UnravelM ([DTyVarBndrSpec], [DType], [DType], DType)
forall a. (Bool -> Bool) -> UnravelM a -> UnravelM a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (Bool -> Bool -> Bool
forall a b. a -> b -> a
const Bool
False) (DType -> UnravelM ([DTyVarBndrSpec], [DType], [DType], DType)
go_ty DType
typ)

    take_tvbs :: DFunArgs -> UnravelM (DFunArgs, [DTyVarBndrSpec])
    take_tvbs :: DFunArgs -> UnravelM (DFunArgs, [DTyVarBndrSpec])
take_tvbs (DFAForalls (DForallInvis [DTyVarBndrSpec]
tvbs) DFunArgs
args) = do
      rank_1 <- UnravelM Bool
forall r (m :: * -> *). MonadReader r m => m r
ask
      unless rank_1 $ fail_forall "higher-rank"
      _ <- traverse_ (traverse_ go_higher_order_ty . extractTvbKind) tvbs
      (args', tvbs') <- take_tvbs args
      pure (args', tvbs ++ tvbs')
    take_tvbs (DFAForalls DForallVis{} DFunArgs
_) = UnravelM (DFunArgs, [DTyVarBndrSpec])
forall (m :: * -> *) a. MonadError String m => m a
fail_vdq
    take_tvbs DFunArgs
args = (DFunArgs, [DTyVarBndrSpec])
-> UnravelM (DFunArgs, [DTyVarBndrSpec])
forall a. a -> UnravelM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DFunArgs
args, [])

    take_ctxt :: DFunArgs -> UnravelM (DFunArgs, DCxt)
    take_ctxt :: DFunArgs -> UnravelM (DFunArgs, [DType])
take_ctxt (DFACxt [DType]
ctxt DFunArgs
args) = do
      rank_1 <- UnravelM Bool
forall r (m :: * -> *). MonadReader r m => m r
ask
      unless rank_1 $ fail_ctxt "higher-rank"
      traverse_ go_higher_order_ty ctxt
      (args', ctxt') <- take_ctxt args
      pure (args', ctxt ++ ctxt')
    take_ctxt (DFAForalls DForallTelescope
tele DFunArgs
_) =
      case DForallTelescope
tele of
        DForallInvis{} -> String -> UnravelM (DFunArgs, [DType])
forall (m :: * -> *) a. MonadError String m => String -> m a
fail_forall String
"nested"
        DForallVis{}   -> UnravelM (DFunArgs, [DType])
forall (m :: * -> *) a. MonadError String m => m a
fail_vdq
    take_ctxt DFunArgs
args = (DFunArgs, [DType]) -> UnravelM (DFunArgs, [DType])
forall a. a -> UnravelM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DFunArgs
args, [])

    take_anons :: DFunArgs -> UnravelM [DType]
    take_anons :: DFunArgs -> UnravelM [DType]
take_anons (DFAAnon DType
anon DFunArgs
args) = do
      DType -> UnravelM ()
go_higher_order_ty DType
anon
      anons <- DFunArgs -> UnravelM [DType]
take_anons DFunArgs
args
      pure (anon:anons)
    take_anons (DFAForalls DForallTelescope
tele DFunArgs
_) =
      case DForallTelescope
tele of
        DForallInvis{} -> String -> UnravelM [DType]
forall (m :: * -> *) a. MonadError String m => String -> m a
fail_forall String
"nested"
        DForallVis{}   -> UnravelM [DType]
forall (m :: * -> *) a. MonadError String m => m a
fail_vdq
    take_anons (DFACxt [DType]
_ DFunArgs
_) = String -> UnravelM [DType]
forall (m :: * -> *) a. MonadError String m => String -> m a
fail_ctxt String
"nested"
    take_anons DFunArgs
DFANil = [DType] -> UnravelM [DType]
forall a. a -> UnravelM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []

    failWith :: MonadError String m => String -> m a
    failWith :: forall (m :: * -> *) a. MonadError String m => String -> m a
failWith String
thing = String -> m a
forall a. String -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> m a) -> String -> m a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
      [ String
"`singletons-th` does not support " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
thing
      , String
"In the type: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Ppr a => a -> String
pprint (DType -> Type
forall th ds. Desugar th ds => ds -> th
sweeten DType
ty)
      ]

    fail_forall :: MonadError String m => String -> m a
    fail_forall :: forall (m :: * -> *) a. MonadError String m => String -> m a
fail_forall String
sort = String -> m a
forall (m :: * -> *) a. MonadError String m => String -> m a
failWith (String -> m a) -> String -> m a
forall a b. (a -> b) -> a -> b
$ String
sort String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" `forall`s"

    fail_vdq :: MonadError String m => m a
    fail_vdq :: forall (m :: * -> *) a. MonadError String m => m a
fail_vdq = String -> m a
forall (m :: * -> *) a. MonadError String m => String -> m a
failWith String
"visible dependent quantification"

    fail_ctxt :: MonadError String m => String -> m a
    fail_ctxt :: forall (m :: * -> *) a. MonadError String m => String -> m a
fail_ctxt String
sort = String -> m a
forall (m :: * -> *) a. MonadError String m => String -> m a
failWith (String -> m a) -> String -> m a
forall a b. (a -> b) -> a -> b
$ String
sort String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" contexts"

-- The monad that powers the internals of unravelVanillaDType_either.
--
-- * ExceptT String: records the error message upon failure.
--
-- * Reader Bool: True if we are in a rank-1 position in a type, False otherwise
newtype UnravelM a = UnravelM { forall a. UnravelM a -> ExceptT String (Reader Bool) a
runUnravelM :: ExceptT String (Reader Bool) a }
  deriving ((forall a b. (a -> b) -> UnravelM a -> UnravelM b)
-> (forall a b. a -> UnravelM b -> UnravelM a) -> Functor UnravelM
forall a b. a -> UnravelM b -> UnravelM a
forall a b. (a -> b) -> UnravelM a -> UnravelM b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> UnravelM a -> UnravelM b
fmap :: forall a b. (a -> b) -> UnravelM a -> UnravelM b
$c<$ :: forall a b. a -> UnravelM b -> UnravelM a
<$ :: forall a b. a -> UnravelM b -> UnravelM a
Functor, Functor UnravelM
Functor UnravelM =>
(forall a. a -> UnravelM a)
-> (forall a b. UnravelM (a -> b) -> UnravelM a -> UnravelM b)
-> (forall a b c.
    (a -> b -> c) -> UnravelM a -> UnravelM b -> UnravelM c)
-> (forall a b. UnravelM a -> UnravelM b -> UnravelM b)
-> (forall a b. UnravelM a -> UnravelM b -> UnravelM a)
-> Applicative UnravelM
forall a. a -> UnravelM a
forall a b. UnravelM a -> UnravelM b -> UnravelM a
forall a b. UnravelM a -> UnravelM b -> UnravelM b
forall a b. UnravelM (a -> b) -> UnravelM a -> UnravelM b
forall a b c.
(a -> b -> c) -> UnravelM a -> UnravelM b -> UnravelM c
forall (f :: * -> *).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
$cpure :: forall a. a -> UnravelM a
pure :: forall a. a -> UnravelM a
$c<*> :: forall a b. UnravelM (a -> b) -> UnravelM a -> UnravelM b
<*> :: forall a b. UnravelM (a -> b) -> UnravelM a -> UnravelM b
$cliftA2 :: forall a b c.
(a -> b -> c) -> UnravelM a -> UnravelM b -> UnravelM c
liftA2 :: forall a b c.
(a -> b -> c) -> UnravelM a -> UnravelM b -> UnravelM c
$c*> :: forall a b. UnravelM a -> UnravelM b -> UnravelM b
*> :: forall a b. UnravelM a -> UnravelM b -> UnravelM b
$c<* :: forall a b. UnravelM a -> UnravelM b -> UnravelM a
<* :: forall a b. UnravelM a -> UnravelM b -> UnravelM a
Applicative, Applicative UnravelM
Applicative UnravelM =>
(forall a b. UnravelM a -> (a -> UnravelM b) -> UnravelM b)
-> (forall a b. UnravelM a -> UnravelM b -> UnravelM b)
-> (forall a. a -> UnravelM a)
-> Monad UnravelM
forall a. a -> UnravelM a
forall a b. UnravelM a -> UnravelM b -> UnravelM b
forall a b. UnravelM a -> (a -> UnravelM b) -> UnravelM b
forall (m :: * -> *).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
$c>>= :: forall a b. UnravelM a -> (a -> UnravelM b) -> UnravelM b
>>= :: forall a b. UnravelM a -> (a -> UnravelM b) -> UnravelM b
$c>> :: forall a b. UnravelM a -> UnravelM b -> UnravelM b
>> :: forall a b. UnravelM a -> UnravelM b -> UnravelM b
$creturn :: forall a. a -> UnravelM a
return :: forall a. a -> UnravelM a
Monad, MonadError String, MonadReader Bool)

-- count the number of arguments in a type
countArgs :: DType -> Int
countArgs :: DType -> Int
countArgs DType
ty = [DVisFunArg] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([DVisFunArg] -> Int) -> [DVisFunArg] -> Int
forall a b. (a -> b) -> a -> b
$ DFunArgs -> [DVisFunArg]
filterDVisFunArgs DFunArgs
args
  where (DFunArgs
args, DType
_) = DType -> (DFunArgs, DType)
unravelDType DType
ty

-- Collect the invisible type variable binders from a sequence of DFunArgs.
filterInvisTvbArgs :: DFunArgs -> [DTyVarBndrSpec]
filterInvisTvbArgs :: DFunArgs -> [DTyVarBndrSpec]
filterInvisTvbArgs DFunArgs
DFANil           = []
filterInvisTvbArgs (DFACxt  [DType]
_ DFunArgs
args) = DFunArgs -> [DTyVarBndrSpec]
filterInvisTvbArgs DFunArgs
args
filterInvisTvbArgs (DFAAnon DType
_ DFunArgs
args) = DFunArgs -> [DTyVarBndrSpec]
filterInvisTvbArgs DFunArgs
args
filterInvisTvbArgs (DFAForalls DForallTelescope
tele DFunArgs
args) =
  let res :: [DTyVarBndrSpec]
res = DFunArgs -> [DTyVarBndrSpec]
filterInvisTvbArgs DFunArgs
args in
  case DForallTelescope
tele of
    DForallVis   [DTyVarBndrUnit]
_     -> [DTyVarBndrSpec]
res
    DForallInvis [DTyVarBndrSpec]
tvbs' -> [DTyVarBndrSpec]
tvbs' [DTyVarBndrSpec] -> [DTyVarBndrSpec] -> [DTyVarBndrSpec]
forall a. [a] -> [a] -> [a]
++ [DTyVarBndrSpec]
res

-- Change all unique Names with a NameU or NameL namespace to non-unique Names
-- by performing a syb-based traversal. See Note [Pitfalls of NameU/NameL] for
-- why this is useful.
noExactTyVars :: Data a => a -> a
noExactTyVars :: forall a. Data a => a -> a
noExactTyVars = (forall a. Data a => a -> a) -> forall a. Data a => a -> a
everywhere a -> a
forall a. Data a => a -> a
go
  where
    go :: Data a => a -> a
    go :: forall a. Data a => a -> a
go = (DTyVarBndrSpec -> DTyVarBndrSpec) -> a -> a
forall a b. (Typeable a, Typeable b) => (b -> b) -> a -> a
mkT (forall flag. Typeable flag => DTyVarBndr flag -> DTyVarBndr flag
fix_tvb @Specificity)
      (a -> a) -> (DTyVarBndrUnit -> DTyVarBndrUnit) -> a -> a
forall a b.
(Typeable a, Typeable b) =>
(a -> a) -> (b -> b) -> a -> a
`extT` forall flag. Typeable flag => DTyVarBndr flag -> DTyVarBndr flag
fix_tvb @()
      (a -> a) -> (DTyVarBndrVis -> DTyVarBndrVis) -> a -> a
forall a b.
(Typeable a, Typeable b) =>
(a -> a) -> (b -> b) -> a -> a
`extT` forall flag. Typeable flag => DTyVarBndr flag -> DTyVarBndr flag
fix_tvb @BndrVis
      (a -> a) -> (DType -> DType) -> a -> a
forall a b.
(Typeable a, Typeable b) =>
(a -> a) -> (b -> b) -> a -> a
`extT` DType -> DType
fix_ty
      (a -> a) -> (InjectivityAnn -> InjectivityAnn) -> a -> a
forall a b.
(Typeable a, Typeable b) =>
(a -> a) -> (b -> b) -> a -> a
`extT` InjectivityAnn -> InjectivityAnn
fix_inj_ann
      (a -> a) -> (LocalVar -> LocalVar) -> a -> a
forall a b.
(Typeable a, Typeable b) =>
(a -> a) -> (b -> b) -> a -> a
`extT` LocalVar -> LocalVar
fix_local_var

    fix_tvb :: Typeable flag => DTyVarBndr flag -> DTyVarBndr flag
    fix_tvb :: forall flag. Typeable flag => DTyVarBndr flag -> DTyVarBndr flag
fix_tvb (DPlainTV Name
n flag
f)    = Name -> flag -> DTyVarBndr flag
forall flag. Name -> flag -> DTyVarBndr flag
DPlainTV (Name -> Name
noExactName Name
n) flag
f
    fix_tvb (DKindedTV Name
n flag
f DType
k) = Name -> flag -> DType -> DTyVarBndr flag
forall flag. Name -> flag -> DType -> DTyVarBndr flag
DKindedTV (Name -> Name
noExactName Name
n) flag
f DType
k

    fix_ty :: DType -> DType
fix_ty (DVarT Name
n)           = Name -> DType
DVarT (Name -> Name
noExactName Name
n)
    fix_ty DType
ty                  = DType
ty

    fix_inj_ann :: InjectivityAnn -> InjectivityAnn
fix_inj_ann (InjectivityAnn Name
lhs [Name]
rhs)
      = Name -> [Name] -> InjectivityAnn
InjectivityAnn (Name -> Name
noExactName Name
lhs) ((Name -> Name) -> [Name] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Name
noExactName [Name]
rhs)

    fix_local_var :: LocalVar -> LocalVar
    fix_local_var :: LocalVar -> LocalVar
fix_local_var (LocalVar { lvName :: LocalVar -> Name
lvName = Name
n, lvKind :: LocalVar -> Maybe DType
lvKind =  Maybe DType
mbKind })
      = LocalVar { lvName :: Name
lvName = Name -> Name
noExactName Name
n, lvKind :: Maybe DType
lvKind = Maybe DType
mbKind }

-- Changes a unique Name with a NameU or NameL namespace to a non-unique Name.
-- See Note [Pitfalls of NameU/NameL] for why this is useful.
noExactName :: Name -> Name
noExactName :: Name -> Name
noExactName n :: Name
n@(Name (OccName String
occ) NameFlavour
ns) =
  case NameFlavour
ns of
    NameU Uniq
unique -> Uniq -> Name
forall {a}. Show a => a -> Name
mk_name Uniq
unique
    NameL Uniq
unique -> Uniq -> Name
forall {a}. Show a => a -> Name
mk_name Uniq
unique
    NameFlavour
_            -> Name
n
  where
    mk_name :: a -> Name
mk_name a
unique = String -> Name
mkName (String
occ String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
unique)

{-
Note [Pitfalls of NameU/NameL]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Most of the Names used in singletons-th come from reified or quoted Template
Haskell definitions. Because these definitions have passed through GHC's
renamer, they have unique Names with unique a NameU/NameL namespace. For the
sake of convenience, we often reuse these Names in the definitions that we
generate. For example, if singletons-th is given a declaration
`f :: forall a_123. a_123 -> a_123`, it will produce a standalone kind signature
`type F :: forall a_123. a_123 -> a_123`, reusing the unique Name `a_123`.

While reusing unique Names is convenient, it does have a downside. In
particular, GHC can sometimes get confused when the same unique Name is reused
in distinct type variable scopes. In the best case, this can lead to confusing
type errors, but in the worst case, it can cause GHC to panic, as seen in the
following issues (all of which were first observed in singletons-th):

* https://gitlab.haskell.org/ghc/ghc/-/issues/11812
* https://gitlab.haskell.org/ghc/ghc/-/issues/17537
* https://gitlab.haskell.org/ghc/ghc/-/issues/19743

This is pretty terrible. Arguably, we are abusing Template Haskell here, since
GHC likely assumes the invariant that each unique Name only has a single
binding site. On the other hand, rearchitecting singletons-th to uphold this
invariant would require a substantial amount of work.

A far easier solution is to identify any problematic areas where unique Names
are reused and work around the issue by changing unique Names to non-unique
Names. The issues above all have a common theme: they arise when unique Names
are reused in the type variable binders of a data type or type family
declaration. For instance, when promoting a function like this:

  f :: forall a_123. a_123 -> a_123
  f x_456 = g
    where
      g = x_456

We must promote `f` and `g` to something like this:

    type F :: forall a_123. a_123 -> a_123
    type family F (arg :: a_123) :: a_123 where
      F x_456 = G x_456

    type family LetG x_456 where
      LetG x_456 = x_456

This looks sensible enough. But note that we are reusing the same unique Name
`x_456` in three different scopes: once in the equation for `F`, once in the
the equation for `G`, and once more in the type variable binder in
`type family LetG x_456`. The last of these scopes in particular is enough to
confuse GHC in some situations and trigger GHC#11812.

Our workaround is to apply the `noExactName` function to such names, which
converts any Names with NameU/NameL namespaces into non-unique Names with
longer OccNames. For instance, `noExactName x_456` will return a non-unique
Name with the OccName `x456`. We use `noExactName` when generating `LetG` so
that it will instead be:

    type family LetG x456 where
      LetG x_456 = x_456

Here, `x456` is a non-unique Name, and `x_456` is a Unique name. Thankfully,
this is sufficient to work around GHC#11812. There is still some amount of
risk, since we are reusing `x_456` in two different type family equations (one
for `LetG` and one for `F`), but GHC accepts this for now. We prefer to use the
`noExactName` in as few places as possible, as using longer OccNames makes the
Haddocks harder to read, so we will continue to reuse unique Names unless GHC
forces us to behave differently.

In addition to the type family example above, we also make use of `noExactName`
(as well as its cousin, `noExactTyVars`) when generating defunctionalization
symbols, as these also require reusing Unique names in several type family and
data type declarations. See references to this Note in the code for particular
locations where we must apply this workaround.
-}

substFamilyResultSig :: Map Name DKind -> DFamilyResultSig -> (Map Name DKind, DFamilyResultSig)
substFamilyResultSig :: Map Name DType
-> DFamilyResultSig -> (Map Name DType, DFamilyResultSig)
substFamilyResultSig Map Name DType
s frs :: DFamilyResultSig
frs@DFamilyResultSig
DNoSig      = (Map Name DType
s, DFamilyResultSig
frs)
substFamilyResultSig Map Name DType
s (DKindSig DType
k)    = (Map Name DType
s, DType -> DFamilyResultSig
DKindSig (Map Name DType -> DType -> DType
SC.substTy Map Name DType
s DType
k))
substFamilyResultSig Map Name DType
s (DTyVarSig DTyVarBndrUnit
tvb) = let (Map Name DType
s', DTyVarBndrUnit
tvb') = Map Name DType
-> DTyVarBndrUnit -> (Map Name DType, DTyVarBndrUnit)
forall flag.
Map Name DType
-> DTyVarBndr flag -> (Map Name DType, DTyVarBndr flag)
SC.substTyVarBndr Map Name DType
s DTyVarBndrUnit
tvb in
                                         (Map Name DType
s', DTyVarBndrUnit -> DFamilyResultSig
DTyVarSig DTyVarBndrUnit
tvb')

dropTvbKind :: DTyVarBndr flag -> DTyVarBndr flag
dropTvbKind :: forall flag. DTyVarBndr flag -> DTyVarBndr flag
dropTvbKind tvb :: DTyVarBndr flag
tvb@(DPlainTV {}) = DTyVarBndr flag
tvb
dropTvbKind (DKindedTV Name
n flag
f DType
_) = Name -> flag -> DTyVarBndr flag
forall flag. Name -> flag -> DTyVarBndr flag
DPlainTV Name
n flag
f

-- apply a type to a list of types
foldType :: DType -> [DType] -> DType
foldType :: DType -> [DType] -> DType
foldType = (DType -> DType -> DType) -> DType -> [DType] -> DType
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl DType -> DType -> DType
DAppT

-- apply a type to a list of type variable binders
foldTypeTvbs :: DType -> [DTyVarBndrVis] -> DType
foldTypeTvbs :: DType -> [DTyVarBndrVis] -> DType
foldTypeTvbs DType
ty = DType -> [DTypeArg] -> DType
applyDType DType
ty ([DTypeArg] -> DType)
-> ([DTyVarBndrVis] -> [DTypeArg]) -> [DTyVarBndrVis] -> DType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DTyVarBndrVis -> DTypeArg) -> [DTyVarBndrVis] -> [DTypeArg]
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndrVis -> DTypeArg
dTyVarBndrVisToDTypeArg

-- Construct a data type's variable binders, possibly using fresh variables
-- from the data type's kind signature. This function is used when constructing
-- a @DataDecl@ to ensure that it has a number of binders equal in length to the
-- number of visible quantifiers (i.e., the number of function arrows plus the
-- number of visible @forall@–bound variables) in the data type's kind.
buildDataDTvbs :: DsMonad q => [DTyVarBndrVis] -> Maybe DKind -> q [DTyVarBndrVis]
buildDataDTvbs :: forall (q :: * -> *).
DsMonad q =>
[DTyVarBndrVis] -> Maybe DType -> q [DTyVarBndrVis]
buildDataDTvbs [DTyVarBndrVis]
tvbs Maybe DType
mk = do
  extra_tvbs <- DType -> q [DTyVarBndrVis]
forall (q :: * -> *). DsMonad q => DType -> q [DTyVarBndrVis]
mkExtraDKindBinders (DType -> q [DTyVarBndrVis]) -> DType -> q [DTyVarBndrVis]
forall a b. (a -> b) -> a -> b
$ DType -> Maybe DType -> DType
forall a. a -> Maybe a -> a
fromMaybe (Name -> DType
DConT Name
typeKindName) Maybe DType
mk
  pure $ tvbs ++ extra_tvbs

-- apply an expression to a list of expressions
foldExp :: DExp -> [DExp] -> DExp
foldExp :: DExp -> [DExp] -> DExp
foldExp = (DExp -> DExp -> DExp) -> DExp -> [DExp] -> DExp
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl DExp -> DExp -> DExp
DAppE

-- choose the first non-empty list
orIfEmpty :: [a] -> [a] -> [a]
orIfEmpty :: forall a. [a] -> [a] -> [a]
orIfEmpty [] [a]
x = [a]
x
orIfEmpty [a]
x  [a]
_ = [a]
x

-- build a pattern match over several expressions, each with only one pattern
multiCase :: [DExp] -> [DPat] -> DExp -> DExp
multiCase :: [DExp] -> [DPat] -> DExp -> DExp
multiCase [] [] DExp
body = DExp
body
multiCase [DExp]
scruts [DPat]
pats DExp
body = [DExp] -> [DClause] -> DExp
dCasesE [DExp]
scruts [[DPat] -> DExp -> DClause
DClause [DPat]
pats DExp
body]

-- a monad transformer for writing a monoid alongside returning a Q
newtype QWithAux m q a = QWA { forall m (q :: * -> *) a. QWithAux m q a -> WriterT m q a
runQWA :: WriterT m q a }
  deriving ( (forall a b. (a -> b) -> QWithAux m q a -> QWithAux m q b)
-> (forall a b. a -> QWithAux m q b -> QWithAux m q a)
-> Functor (QWithAux m q)
forall a b. a -> QWithAux m q b -> QWithAux m q a
forall a b. (a -> b) -> QWithAux m q a -> QWithAux m q b
forall m (q :: * -> *) a b.
Functor q =>
a -> QWithAux m q b -> QWithAux m q a
forall m (q :: * -> *) a b.
Functor q =>
(a -> b) -> QWithAux m q a -> QWithAux m q b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall m (q :: * -> *) a b.
Functor q =>
(a -> b) -> QWithAux m q a -> QWithAux m q b
fmap :: forall a b. (a -> b) -> QWithAux m q a -> QWithAux m q b
$c<$ :: forall m (q :: * -> *) a b.
Functor q =>
a -> QWithAux m q b -> QWithAux m q a
<$ :: forall a b. a -> QWithAux m q b -> QWithAux m q a
Functor, Functor (QWithAux m q)
Functor (QWithAux m q) =>
(forall a. a -> QWithAux m q a)
-> (forall a b.
    QWithAux m q (a -> b) -> QWithAux m q a -> QWithAux m q b)
-> (forall a b c.
    (a -> b -> c)
    -> QWithAux m q a -> QWithAux m q b -> QWithAux m q c)
-> (forall a b. QWithAux m q a -> QWithAux m q b -> QWithAux m q b)
-> (forall a b. QWithAux m q a -> QWithAux m q b -> QWithAux m q a)
-> Applicative (QWithAux m q)
forall a. a -> QWithAux m q a
forall a b. QWithAux m q a -> QWithAux m q b -> QWithAux m q a
forall a b. QWithAux m q a -> QWithAux m q b -> QWithAux m q b
forall a b.
QWithAux m q (a -> b) -> QWithAux m q a -> QWithAux m q b
forall a b c.
(a -> b -> c) -> QWithAux m q a -> QWithAux m q b -> QWithAux m q c
forall m (q :: * -> *).
(Monoid m, Applicative q) =>
Functor (QWithAux m q)
forall m (q :: * -> *) a.
(Monoid m, Applicative q) =>
a -> QWithAux m q a
forall m (q :: * -> *) a b.
(Monoid m, Applicative q) =>
QWithAux m q a -> QWithAux m q b -> QWithAux m q a
forall m (q :: * -> *) a b.
(Monoid m, Applicative q) =>
QWithAux m q a -> QWithAux m q b -> QWithAux m q b
forall m (q :: * -> *) a b.
(Monoid m, Applicative q) =>
QWithAux m q (a -> b) -> QWithAux m q a -> QWithAux m q b
forall m (q :: * -> *) a b c.
(Monoid m, Applicative q) =>
(a -> b -> c) -> QWithAux m q a -> QWithAux m q b -> QWithAux m q c
forall (f :: * -> *).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
$cpure :: forall m (q :: * -> *) a.
(Monoid m, Applicative q) =>
a -> QWithAux m q a
pure :: forall a. a -> QWithAux m q a
$c<*> :: forall m (q :: * -> *) a b.
(Monoid m, Applicative q) =>
QWithAux m q (a -> b) -> QWithAux m q a -> QWithAux m q b
<*> :: forall a b.
QWithAux m q (a -> b) -> QWithAux m q a -> QWithAux m q b
$cliftA2 :: forall m (q :: * -> *) a b c.
(Monoid m, Applicative q) =>
(a -> b -> c) -> QWithAux m q a -> QWithAux m q b -> QWithAux m q c
liftA2 :: forall a b c.
(a -> b -> c) -> QWithAux m q a -> QWithAux m q b -> QWithAux m q c
$c*> :: forall m (q :: * -> *) a b.
(Monoid m, Applicative q) =>
QWithAux m q a -> QWithAux m q b -> QWithAux m q b
*> :: forall a b. QWithAux m q a -> QWithAux m q b -> QWithAux m q b
$c<* :: forall m (q :: * -> *) a b.
(Monoid m, Applicative q) =>
QWithAux m q a -> QWithAux m q b -> QWithAux m q a
<* :: forall a b. QWithAux m q a -> QWithAux m q b -> QWithAux m q a
Applicative, Applicative (QWithAux m q)
Applicative (QWithAux m q) =>
(forall a b.
 QWithAux m q a -> (a -> QWithAux m q b) -> QWithAux m q b)
-> (forall a b. QWithAux m q a -> QWithAux m q b -> QWithAux m q b)
-> (forall a. a -> QWithAux m q a)
-> Monad (QWithAux m q)
forall a. a -> QWithAux m q a
forall a b. QWithAux m q a -> QWithAux m q b -> QWithAux m q b
forall a b.
QWithAux m q a -> (a -> QWithAux m q b) -> QWithAux m q b
forall m (q :: * -> *).
(Monoid m, Monad q) =>
Applicative (QWithAux m q)
forall m (q :: * -> *) a.
(Monoid m, Monad q) =>
a -> QWithAux m q a
forall m (q :: * -> *) a b.
(Monoid m, Monad q) =>
QWithAux m q a -> QWithAux m q b -> QWithAux m q b
forall m (q :: * -> *) a b.
(Monoid m, Monad q) =>
QWithAux m q a -> (a -> QWithAux m q b) -> QWithAux m q b
forall (m :: * -> *).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
$c>>= :: forall m (q :: * -> *) a b.
(Monoid m, Monad q) =>
QWithAux m q a -> (a -> QWithAux m q b) -> QWithAux m q b
>>= :: forall a b.
QWithAux m q a -> (a -> QWithAux m q b) -> QWithAux m q b
$c>> :: forall m (q :: * -> *) a b.
(Monoid m, Monad q) =>
QWithAux m q a -> QWithAux m q b -> QWithAux m q b
>> :: forall a b. QWithAux m q a -> QWithAux m q b -> QWithAux m q b
$creturn :: forall m (q :: * -> *) a.
(Monoid m, Monad q) =>
a -> QWithAux m q a
return :: forall a. a -> QWithAux m q a
Monad, (forall (m :: * -> *). Monad m => Monad (QWithAux m m)) =>
(forall (m :: * -> *) a. Monad m => m a -> QWithAux m m a)
-> MonadTrans (QWithAux m)
forall m (m :: * -> *). (Monoid m, Monad m) => Monad (QWithAux m m)
forall m (m :: * -> *) a.
(Monoid m, Monad m) =>
m a -> QWithAux m m a
forall (m :: * -> *). Monad m => Monad (QWithAux m m)
forall (m :: * -> *) a. Monad m => m a -> QWithAux m m a
forall (t :: (* -> *) -> * -> *).
(forall (m :: * -> *). Monad m => Monad (t m)) =>
(forall (m :: * -> *) a. Monad m => m a -> t m a) -> MonadTrans t
$clift :: forall m (m :: * -> *) a.
(Monoid m, Monad m) =>
m a -> QWithAux m m a
lift :: forall (m :: * -> *) a. Monad m => m a -> QWithAux m m a
MonadTrans
           , MonadWriter m, MonadReader r
           , Monad (QWithAux m q)
Monad (QWithAux m q) =>
(forall a. String -> QWithAux m q a) -> MonadFail (QWithAux m q)
forall a. String -> QWithAux m q a
forall m (q :: * -> *).
(Monoid m, MonadFail q) =>
Monad (QWithAux m q)
forall m (q :: * -> *) a.
(Monoid m, MonadFail q) =>
String -> QWithAux m q a
forall (m :: * -> *).
Monad m =>
(forall a. String -> m a) -> MonadFail m
$cfail :: forall m (q :: * -> *) a.
(Monoid m, MonadFail q) =>
String -> QWithAux m q a
fail :: forall a. String -> QWithAux m q a
MonadFail, Monad (QWithAux m q)
Monad (QWithAux m q) =>
(forall a. IO a -> QWithAux m q a) -> MonadIO (QWithAux m q)
forall a. IO a -> QWithAux m q a
forall m (q :: * -> *).
(Monoid m, MonadIO q) =>
Monad (QWithAux m q)
forall m (q :: * -> *) a.
(Monoid m, MonadIO q) =>
IO a -> QWithAux m q a
forall (m :: * -> *).
Monad m =>
(forall a. IO a -> m a) -> MonadIO m
$cliftIO :: forall m (q :: * -> *) a.
(Monoid m, MonadIO q) =>
IO a -> QWithAux m q a
liftIO :: forall a. IO a -> QWithAux m q a
MonadIO, MonadFail (QWithAux m q)
MonadIO (QWithAux m q)
QWithAux m q String
QWithAux m q [Extension]
QWithAux m q Loc
Bool -> String -> QWithAux m q (Maybe Name)
Bool -> String -> QWithAux m q ()
String -> QWithAux m q String
String -> QWithAux m q Name
String -> QWithAux m q ()
[Dec] -> QWithAux m q ()
Q () -> QWithAux m q ()
Name -> QWithAux m q [Role]
Name -> QWithAux m q [DecidedStrictness]
Name -> QWithAux m q (Maybe Fixity)
Name -> QWithAux m q Type
Name -> QWithAux m q Info
Name -> [Type] -> QWithAux m q [Dec]
(MonadIO (QWithAux m q), MonadFail (QWithAux m q)) =>
(String -> QWithAux m q Name)
-> (Bool -> String -> QWithAux m q ())
-> (forall a. QWithAux m q a -> QWithAux m q a -> QWithAux m q a)
-> (Bool -> String -> QWithAux m q (Maybe Name))
-> (Name -> QWithAux m q Info)
-> (Name -> QWithAux m q (Maybe Fixity))
-> (Name -> QWithAux m q Type)
-> (Name -> [Type] -> QWithAux m q [Dec])
-> (Name -> QWithAux m q [Role])
-> (forall a. Data a => AnnLookup -> QWithAux m q [a])
-> (Module -> QWithAux m q ModuleInfo)
-> (Name -> QWithAux m q [DecidedStrictness])
-> QWithAux m q Loc
-> (forall a. IO a -> QWithAux m q a)
-> QWithAux m q String
-> (String -> QWithAux m q ())
-> (String -> QWithAux m q String)
-> ([Dec] -> QWithAux m q ())
-> (ForeignSrcLang -> String -> QWithAux m q ())
-> (Q () -> QWithAux m q ())
-> (String -> QWithAux m q ())
-> (forall a. Typeable a => QWithAux m q (Maybe a))
-> (forall a. Typeable a => a -> QWithAux m q ())
-> (Extension -> QWithAux m q Bool)
-> QWithAux m q [Extension]
-> (DocLoc -> String -> QWithAux m q ())
-> (DocLoc -> QWithAux m q (Maybe String))
-> Quasi (QWithAux m q)
Extension -> QWithAux m q Bool
ForeignSrcLang -> String -> QWithAux m q ()
DocLoc -> QWithAux m q (Maybe String)
DocLoc -> String -> QWithAux m q ()
Module -> QWithAux m q ModuleInfo
forall a. Data a => AnnLookup -> QWithAux m q [a]
forall a. Typeable a => QWithAux m q (Maybe a)
forall a. Typeable a => a -> QWithAux m q ()
forall a. IO a -> QWithAux m q a
forall a. QWithAux m q a -> QWithAux m q a -> QWithAux m q a
forall m (q :: * -> *).
(Quasi q, Monoid m) =>
MonadFail (QWithAux m q)
forall m (q :: * -> *).
(Quasi q, Monoid m) =>
MonadIO (QWithAux m q)
forall m (q :: * -> *). (Quasi q, Monoid m) => QWithAux m q String
forall m (q :: * -> *).
(Quasi q, Monoid m) =>
QWithAux m q [Extension]
forall m (q :: * -> *). (Quasi q, Monoid m) => QWithAux m q Loc
forall m (q :: * -> *).
(Quasi q, Monoid m) =>
Bool -> String -> QWithAux m q (Maybe Name)
forall m (q :: * -> *).
(Quasi q, Monoid m) =>
Bool -> String -> QWithAux m q ()
forall m (q :: * -> *).
(Quasi q, Monoid m) =>
String -> QWithAux m q String
forall m (q :: * -> *).
(Quasi q, Monoid m) =>
String -> QWithAux m q Name
forall m (q :: * -> *).
(Quasi q, Monoid m) =>
String -> QWithAux m q ()
forall m (q :: * -> *).
(Quasi q, Monoid m) =>
[Dec] -> QWithAux m q ()
forall m (q :: * -> *).
(Quasi q, Monoid m) =>
Q () -> QWithAux m q ()
forall m (q :: * -> *).
(Quasi q, Monoid m) =>
Name -> QWithAux m q [Role]
forall m (q :: * -> *).
(Quasi q, Monoid m) =>
Name -> QWithAux m q [DecidedStrictness]
forall m (q :: * -> *).
(Quasi q, Monoid m) =>
Name -> QWithAux m q (Maybe Fixity)
forall m (q :: * -> *).
(Quasi q, Monoid m) =>
Name -> QWithAux m q Type
forall m (q :: * -> *).
(Quasi q, Monoid m) =>
Name -> QWithAux m q Info
forall m (q :: * -> *).
(Quasi q, Monoid m) =>
Name -> [Type] -> QWithAux m q [Dec]
forall m (q :: * -> *).
(Quasi q, Monoid m) =>
Extension -> QWithAux m q Bool
forall m (q :: * -> *).
(Quasi q, Monoid m) =>
ForeignSrcLang -> String -> QWithAux m q ()
forall m (q :: * -> *).
(Quasi q, Monoid m) =>
DocLoc -> QWithAux m q (Maybe String)
forall m (q :: * -> *).
(Quasi q, Monoid m) =>
DocLoc -> String -> QWithAux m q ()
forall m (q :: * -> *).
(Quasi q, Monoid m) =>
Module -> QWithAux m q ModuleInfo
forall m (q :: * -> *) a.
(Quasi q, Monoid m, Data a) =>
AnnLookup -> QWithAux m q [a]
forall m (q :: * -> *) a.
(Quasi q, Monoid m, Typeable a) =>
QWithAux m q (Maybe a)
forall m (q :: * -> *) a.
(Quasi q, Monoid m, Typeable a) =>
a -> QWithAux m q ()
forall m (q :: * -> *) a.
(Quasi q, Monoid m) =>
IO a -> QWithAux m q a
forall m (q :: * -> *) a.
(Quasi q, Monoid m) =>
QWithAux m q a -> QWithAux m q a -> QWithAux m q a
forall (m :: * -> *).
(MonadIO m, MonadFail m) =>
(String -> m Name)
-> (Bool -> String -> m ())
-> (forall a. m a -> m a -> m a)
-> (Bool -> String -> m (Maybe Name))
-> (Name -> m Info)
-> (Name -> m (Maybe Fixity))
-> (Name -> m Type)
-> (Name -> [Type] -> m [Dec])
-> (Name -> m [Role])
-> (forall a. Data a => AnnLookup -> m [a])
-> (Module -> m ModuleInfo)
-> (Name -> m [DecidedStrictness])
-> m Loc
-> (forall a. IO a -> m a)
-> m String
-> (String -> m ())
-> (String -> m String)
-> ([Dec] -> m ())
-> (ForeignSrcLang -> String -> m ())
-> (Q () -> m ())
-> (String -> m ())
-> (forall a. Typeable a => m (Maybe a))
-> (forall a. Typeable a => a -> m ())
-> (Extension -> m Bool)
-> m [Extension]
-> (DocLoc -> String -> m ())
-> (DocLoc -> m (Maybe String))
-> Quasi m
$cqNewName :: forall m (q :: * -> *).
(Quasi q, Monoid m) =>
String -> QWithAux m q Name
qNewName :: String -> QWithAux m q Name
$cqReport :: forall m (q :: * -> *).
(Quasi q, Monoid m) =>
Bool -> String -> QWithAux m q ()
qReport :: Bool -> String -> QWithAux m q ()
$cqRecover :: forall m (q :: * -> *) a.
(Quasi q, Monoid m) =>
QWithAux m q a -> QWithAux m q a -> QWithAux m q a
qRecover :: forall a. QWithAux m q a -> QWithAux m q a -> QWithAux m q a
$cqLookupName :: forall m (q :: * -> *).
(Quasi q, Monoid m) =>
Bool -> String -> QWithAux m q (Maybe Name)
qLookupName :: Bool -> String -> QWithAux m q (Maybe Name)
$cqReify :: forall m (q :: * -> *).
(Quasi q, Monoid m) =>
Name -> QWithAux m q Info
qReify :: Name -> QWithAux m q Info
$cqReifyFixity :: forall m (q :: * -> *).
(Quasi q, Monoid m) =>
Name -> QWithAux m q (Maybe Fixity)
qReifyFixity :: Name -> QWithAux m q (Maybe Fixity)
$cqReifyType :: forall m (q :: * -> *).
(Quasi q, Monoid m) =>
Name -> QWithAux m q Type
qReifyType :: Name -> QWithAux m q Type
$cqReifyInstances :: forall m (q :: * -> *).
(Quasi q, Monoid m) =>
Name -> [Type] -> QWithAux m q [Dec]
qReifyInstances :: Name -> [Type] -> QWithAux m q [Dec]
$cqReifyRoles :: forall m (q :: * -> *).
(Quasi q, Monoid m) =>
Name -> QWithAux m q [Role]
qReifyRoles :: Name -> QWithAux m q [Role]
$cqReifyAnnotations :: forall m (q :: * -> *) a.
(Quasi q, Monoid m, Data a) =>
AnnLookup -> QWithAux m q [a]
qReifyAnnotations :: forall a. Data a => AnnLookup -> QWithAux m q [a]
$cqReifyModule :: forall m (q :: * -> *).
(Quasi q, Monoid m) =>
Module -> QWithAux m q ModuleInfo
qReifyModule :: Module -> QWithAux m q ModuleInfo
$cqReifyConStrictness :: forall m (q :: * -> *).
(Quasi q, Monoid m) =>
Name -> QWithAux m q [DecidedStrictness]
qReifyConStrictness :: Name -> QWithAux m q [DecidedStrictness]
$cqLocation :: forall m (q :: * -> *). (Quasi q, Monoid m) => QWithAux m q Loc
qLocation :: QWithAux m q Loc
$cqRunIO :: forall m (q :: * -> *) a.
(Quasi q, Monoid m) =>
IO a -> QWithAux m q a
qRunIO :: forall a. IO a -> QWithAux m q a
$cqGetPackageRoot :: forall m (q :: * -> *). (Quasi q, Monoid m) => QWithAux m q String
qGetPackageRoot :: QWithAux m q String
$cqAddDependentFile :: forall m (q :: * -> *).
(Quasi q, Monoid m) =>
String -> QWithAux m q ()
qAddDependentFile :: String -> QWithAux m q ()
$cqAddTempFile :: forall m (q :: * -> *).
(Quasi q, Monoid m) =>
String -> QWithAux m q String
qAddTempFile :: String -> QWithAux m q String
$cqAddTopDecls :: forall m (q :: * -> *).
(Quasi q, Monoid m) =>
[Dec] -> QWithAux m q ()
qAddTopDecls :: [Dec] -> QWithAux m q ()
$cqAddForeignFilePath :: forall m (q :: * -> *).
(Quasi q, Monoid m) =>
ForeignSrcLang -> String -> QWithAux m q ()
qAddForeignFilePath :: ForeignSrcLang -> String -> QWithAux m q ()
$cqAddModFinalizer :: forall m (q :: * -> *).
(Quasi q, Monoid m) =>
Q () -> QWithAux m q ()
qAddModFinalizer :: Q () -> QWithAux m q ()
$cqAddCorePlugin :: forall m (q :: * -> *).
(Quasi q, Monoid m) =>
String -> QWithAux m q ()
qAddCorePlugin :: String -> QWithAux m q ()
$cqGetQ :: forall m (q :: * -> *) a.
(Quasi q, Monoid m, Typeable a) =>
QWithAux m q (Maybe a)
qGetQ :: forall a. Typeable a => QWithAux m q (Maybe a)
$cqPutQ :: forall m (q :: * -> *) a.
(Quasi q, Monoid m, Typeable a) =>
a -> QWithAux m q ()
qPutQ :: forall a. Typeable a => a -> QWithAux m q ()
$cqIsExtEnabled :: forall m (q :: * -> *).
(Quasi q, Monoid m) =>
Extension -> QWithAux m q Bool
qIsExtEnabled :: Extension -> QWithAux m q Bool
$cqExtsEnabled :: forall m (q :: * -> *).
(Quasi q, Monoid m) =>
QWithAux m q [Extension]
qExtsEnabled :: QWithAux m q [Extension]
$cqPutDoc :: forall m (q :: * -> *).
(Quasi q, Monoid m) =>
DocLoc -> String -> QWithAux m q ()
qPutDoc :: DocLoc -> String -> QWithAux m q ()
$cqGetDoc :: forall m (q :: * -> *).
(Quasi q, Monoid m) =>
DocLoc -> QWithAux m q (Maybe String)
qGetDoc :: DocLoc -> QWithAux m q (Maybe String)
Quasi, MonadFail (QWithAux m q)
Quasi (QWithAux m q)
QWithAux m q [Dec]
(Quasi (QWithAux m q), MonadFail (QWithAux m q)) =>
QWithAux m q [Dec] -> DsMonad (QWithAux m q)
forall m (q :: * -> *).
(DsMonad q, Monoid m) =>
MonadFail (QWithAux m q)
forall m (q :: * -> *).
(DsMonad q, Monoid m) =>
Quasi (QWithAux m q)
forall m (q :: * -> *). (DsMonad q, Monoid m) => QWithAux m q [Dec]
forall (m :: * -> *).
(Quasi m, MonadFail m) =>
m [Dec] -> DsMonad m
$clocalDeclarations :: forall m (q :: * -> *). (DsMonad q, Monoid m) => QWithAux m q [Dec]
localDeclarations :: QWithAux m q [Dec]
DsMonad )

-- run a computation with an auxiliary monoid, discarding the monoid result
evalWithoutAux :: Quasi q => QWithAux m q a -> q a
evalWithoutAux :: forall (q :: * -> *) m a. Quasi q => QWithAux m q a -> q a
evalWithoutAux = ((a, m) -> a) -> q (a, m) -> q a
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (a, m) -> a
forall a b. (a, b) -> a
fst (q (a, m) -> q a)
-> (QWithAux m q a -> q (a, m)) -> QWithAux m q a -> q a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WriterT m q a -> q (a, m)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (WriterT m q a -> q (a, m))
-> (QWithAux m q a -> WriterT m q a) -> QWithAux m q a -> q (a, m)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QWithAux m q a -> WriterT m q a
forall m (q :: * -> *) a. QWithAux m q a -> WriterT m q a
runQWA

-- run a computation with an auxiliary monoid, returning only the monoid result
evalForAux :: Quasi q => QWithAux m q a -> q m
evalForAux :: forall (q :: * -> *) m a. Quasi q => QWithAux m q a -> q m
evalForAux = WriterT m q a -> q m
forall (m :: * -> *) w a. Monad m => WriterT w m a -> m w
execWriterT (WriterT m q a -> q m)
-> (QWithAux m q a -> WriterT m q a) -> QWithAux m q a -> q m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QWithAux m q a -> WriterT m q a
forall m (q :: * -> *) a. QWithAux m q a -> WriterT m q a
runQWA

-- run a computation with an auxiliary monoid, return both the result
-- of the computation and the monoid result
evalForPair :: QWithAux m q a -> q (a, m)
evalForPair :: forall m (q :: * -> *) a. QWithAux m q a -> q (a, m)
evalForPair = WriterT m q a -> q (a, m)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (WriterT m q a -> q (a, m))
-> (QWithAux m q a -> WriterT m q a) -> QWithAux m q a -> q (a, m)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QWithAux m q a -> WriterT m q a
forall m (q :: * -> *) a. QWithAux m q a -> WriterT m q a
runQWA

-- in a computation with an auxiliary map, add a binding to the map
addBinding :: (Quasi q, Ord k) => k -> v -> QWithAux (Map.Map k v) q ()
addBinding :: forall (q :: * -> *) k v.
(Quasi q, Ord k) =>
k -> v -> QWithAux (Map k v) q ()
addBinding k
k v
v = Map k v -> QWithAux (Map k v) q ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (k -> v -> Map k v
forall k a. k -> a -> Map k a
Map.singleton k
k v
v)

-- in a computation with an auxiliar list, add an element to the list
addElement :: Quasi q => elt -> QWithAux [elt] q ()
addElement :: forall (q :: * -> *) elt. Quasi q => elt -> QWithAux [elt] q ()
addElement elt
elt = [elt] -> QWithAux [elt] q ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [elt
elt]

-- | Call 'lookupTypeNameWithLocals' first to ensure we have a 'Name' in the
-- type namespace, then call 'dsReify'.

-- See also Note [Using dsReifyTypeNameInfo when promoting instances]
-- in Data.Singletons.TH.Promote.
dsReifyTypeNameInfo :: DsMonad q => Name -> q (Maybe DInfo)
dsReifyTypeNameInfo :: forall (q :: * -> *). DsMonad q => Name -> q (Maybe DInfo)
dsReifyTypeNameInfo Name
ty_name = do
  mb_name <- String -> q (Maybe Name)
forall (q :: * -> *). DsMonad q => String -> q (Maybe Name)
lookupTypeNameWithLocals (Name -> String
nameBase Name
ty_name)
  case mb_name of
    Just Name
n  -> Name -> q (Maybe DInfo)
forall (q :: * -> *). DsMonad q => Name -> q (Maybe DInfo)
dsReify Name
n
    Maybe Name
Nothing -> Maybe DInfo -> q (Maybe DInfo)
forall a. a -> q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe DInfo
forall a. Maybe a
Nothing

-- lift concatMap into a monad
-- could this be more efficient?
concatMapM :: (Monad monad, Monoid monoid, Traversable t)
           => (a -> monad monoid) -> t a -> monad monoid
concatMapM :: forall (monad :: * -> *) monoid (t :: * -> *) a.
(Monad monad, Monoid monoid, Traversable t) =>
(a -> monad monoid) -> t a -> monad monoid
concatMapM a -> monad monoid
fn t a
list = do
  bss <- (a -> monad monoid) -> t a -> monad (t monoid)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> t a -> m (t b)
mapM a -> monad monoid
fn t a
list
  return $ fold bss

-- like GHC's
mapMaybeM :: Monad m => (a -> m (Maybe b)) -> [a] -> m [b]
mapMaybeM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m (Maybe b)) -> [a] -> m [b]
mapMaybeM a -> m (Maybe b)
_ [] = [b] -> m [b]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return []
mapMaybeM a -> m (Maybe b)
f (a
x:[a]
xs) = do
  y <- a -> m (Maybe b)
f a
x
  ys <- mapMaybeM f xs
  return $ case y of
    Maybe b
Nothing -> [b]
ys
    Just b
z  -> b
z b -> [b] -> [b]
forall a. a -> [a] -> [a]
: [b]
ys

-- make a one-element list
listify :: a -> [a]
listify :: forall a. a -> [a]
listify = (a -> [a] -> [a]
forall a. a -> [a] -> [a]
:[])

fstOf3 :: (a,b,c) -> a
fstOf3 :: forall a b c. (a, b, c) -> a
fstOf3 (a
a,b
_,c
_) = a
a

liftFst :: (a -> b) -> (a, c) -> (b, c)
liftFst :: forall a b c. (a -> b) -> (a, c) -> (b, c)
liftFst a -> b
f (a
a, c
c) = (a -> b
f a
a, c
c)

liftSnd :: (a -> b) -> (c, a) -> (c, b)
liftSnd :: forall a b c. (a -> b) -> (c, a) -> (c, b)
liftSnd a -> b
f (c
c, a
a) = (c
c, a -> b
f a
a)

snocView :: [a] -> ([a], a)
snocView :: forall a. [a] -> ([a], a)
snocView [] = String -> ([a], a)
forall a. HasCallStack => String -> a
error String
"snocView nil"
snocView [a
x] = ([], a
x)
snocView (a
x : [a]
xs) = ([a] -> [a]) -> ([a], a) -> ([a], a)
forall a b c. (a -> b) -> (a, c) -> (b, c)
liftFst (a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:) ([a] -> ([a], a)
forall a. [a] -> ([a], a)
snocView [a]
xs)

partitionWith :: (a -> Either b c) -> [a] -> ([b], [c])
partitionWith :: forall a b c. (a -> Either b c) -> [a] -> ([b], [c])
partitionWith a -> Either b c
f = [b] -> [c] -> [a] -> ([b], [c])
go [] []
  where go :: [b] -> [c] -> [a] -> ([b], [c])
go [b]
bs [c]
cs []     = ([b] -> [b]
forall a. [a] -> [a]
reverse [b]
bs, [c] -> [c]
forall a. [a] -> [a]
reverse [c]
cs)
        go [b]
bs [c]
cs (a
a:[a]
as) =
          case a -> Either b c
f a
a of
            Left b
b  -> [b] -> [c] -> [a] -> ([b], [c])
go (b
bb -> [b] -> [b]
forall a. a -> [a] -> [a]
:[b]
bs) [c]
cs [a]
as
            Right c
c -> [b] -> [c] -> [a] -> ([b], [c])
go [b]
bs (c
cc -> [c] -> [c]
forall a. a -> [a] -> [a]
:[c]
cs) [a]
as

partitionWithM :: Monad m => (a -> m (Either b c)) -> [a] -> m ([b], [c])
partitionWithM :: forall (m :: * -> *) a b c.
Monad m =>
(a -> m (Either b c)) -> [a] -> m ([b], [c])
partitionWithM a -> m (Either b c)
f = [b] -> [c] -> [a] -> m ([b], [c])
go [] []
  where go :: [b] -> [c] -> [a] -> m ([b], [c])
go [b]
bs [c]
cs []     = ([b], [c]) -> m ([b], [c])
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([b] -> [b]
forall a. [a] -> [a]
reverse [b]
bs, [c] -> [c]
forall a. [a] -> [a]
reverse [c]
cs)
        go [b]
bs [c]
cs (a
a:[a]
as) = do
          fa <- a -> m (Either b c)
f a
a
          case fa of
            Left b
b  -> [b] -> [c] -> [a] -> m ([b], [c])
go (b
bb -> [b] -> [b]
forall a. a -> [a] -> [a]
:[b]
bs) [c]
cs [a]
as
            Right c
c -> [b] -> [c] -> [a] -> m ([b], [c])
go [b]
bs (c
cc -> [c] -> [c]
forall a. a -> [a] -> [a]
:[c]
cs) [a]
as

partitionLetDecs :: [DDec] -> ([DLetDec], [DDec])
partitionLetDecs :: [DDec] -> ([DLetDec], [DDec])
partitionLetDecs = (DDec -> Either DLetDec DDec) -> [DDec] -> ([DLetDec], [DDec])
forall a b c. (a -> Either b c) -> [a] -> ([b], [c])
partitionWith (\case DLetDec DLetDec
ld -> DLetDec -> Either DLetDec DDec
forall a b. a -> Either a b
Left DLetDec
ld
                                        DDec
dec        -> DDec -> Either DLetDec DDec
forall a b. b -> Either a b
Right DDec
dec)

{-# INLINEABLE zipWith3M #-}
zipWith3M :: Monad m => (a -> b -> m c) -> [a] -> [b] -> m [c]
zipWith3M :: forall (m :: * -> *) a b c.
Monad m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWith3M a -> b -> m c
f (a
a:[a]
as) (b
b:[b]
bs) = (:) (c -> [c] -> [c]) -> m c -> m ([c] -> [c])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> b -> m c
f a
a b
b m ([c] -> [c]) -> m [c] -> m [c]
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (a -> b -> m c) -> [a] -> [b] -> m [c]
forall (m :: * -> *) a b c.
Monad m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWith3M a -> b -> m c
f [a]
as [b]
bs
zipWith3M a -> b -> m c
_ [a]
_ [b]
_ = [c] -> m [c]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return []

mapAndUnzip3M :: Monad m => (a -> m (b,c,d)) -> [a] -> m ([b],[c],[d])
mapAndUnzip3M :: forall (m :: * -> *) a b c d.
Monad m =>
(a -> m (b, c, d)) -> [a] -> m ([b], [c], [d])
mapAndUnzip3M a -> m (b, c, d)
_ []     = ([b], [c], [d]) -> m ([b], [c], [d])
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([],[],[])
mapAndUnzip3M a -> m (b, c, d)
f (a
x:[a]
xs) = do
    (r1,  r2,  r3)  <- a -> m (b, c, d)
f a
x
    (rs1, rs2, rs3) <- mapAndUnzip3M f xs
    return (r1:rs1, r2:rs2, r3:rs3)

-- is it a letter or underscore?
isHsLetter :: Char -> Bool
isHsLetter :: Char -> Bool
isHsLetter Char
c = Char -> Bool
isLetter Char
c Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'_'