{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TemplateHaskellQuotes #-}
{-# LANGUAGE Unsafe #-}
{-|
Module:      Data.Eliminator.TH
Copyright:   (C) 2017 Ryan Scott
License:     BSD-style (see the file LICENSE)
Maintainer:  Ryan Scott
Stability:   Experimental
Portability: GHC

Generate dependently typed elimination functions using Template Haskell.
-}
module Data.Eliminator.TH (
    -- * Eliminator generation
    -- ** Term-level eliminators
    -- $term-conventions
    deriveElim
  , deriveElimNamed
    -- ** Type-level eliminators
    -- $type-conventions
  , deriveTypeElim
  , deriveTypeElimNamed
  ) where

import           Control.Applicative
import           Control.Monad

import           Data.Char (isLetter, isUpper, toUpper)
import           Data.Foldable
import qualified Data.Kind as Kind (Type)
import           Data.Maybe
import           Data.Proxy
import           Data.Singletons.TH.Options

import           Language.Haskell.TH
import           Language.Haskell.TH.Datatype
import           Language.Haskell.TH.Datatype.TyVarBndr
import           Language.Haskell.TH.Desugar hiding (NewOrData(..))

import           Prelude.Singletons

{- $term-conventions
'deriveElim' and 'deriveElimNamed' provide a way to automate the creation of
eliminator functions, which are mostly boilerplate. Here is a complete example
showing how one might use 'deriveElim':

@
$('singletons' [d| data MyList a = MyNil | MyCons a (MyList a) |])
$('deriveElim' ''MyList)
@

This will produce an eliminator function that looks roughly like the following:

@
elimMyList :: forall (a :: 'Type') (p :: MyList a '~>' 'Type') (l :: MyList a).
              'Sing' l
           -> 'Apply' p MyNil
           -> (forall (x :: a). 'Sing' x
                -> forall (xs :: MyList a). 'Sing' xs -> 'Apply' p xs
                -> 'Apply' p (MyCons x xs))
           -> 'Apply' p l
elimMyList SMyNil pMyNil _ = pMyNil
elimMyList (SMyCons (x' :: 'Sing' x) (xs' :: 'Sing' xs)) pMyNil pMyCons
  = pMyCons x' xs' (elimMyList \@a \@p \@xs pMyNil pMyCons)
@

There are some important things to note here:

* Because these eliminators use 'Sing' under the hood, in order for
  'deriveElim' to work, the 'Sing' instance for the data type given as an
  argument must be in scope. Moreover, 'deriveElim' assumes the naming
  conventions for singled constructors used by the @singletons@ library.
  (This is why the 'singletons' function is used in the example above).

* There is a convention for the order in which the arguments appear.
  The quantified type variables appear in this order:

    1. First, the type variables of the data type itself (@a@, in the above example).

    2. Second, a predicate type variable of kind @\<Datatype\> '~>' 'Type'@
       (@p@, in the above example).

    3. Finally, a type variable of kind @\<Datatype\>@ (@l@, in the above example).

  The function arguments appear in this order:

    1. First, a 'Sing' argument (@'Sing' l@, in the above example).

    2. Next, there are arguments that correspond to each constructor. More on this
       in a second.

  The return type is the predicate type variable applied to the data type
  (@'Apply' p (MyCons x xs)@, the above example).

  The type of each constructor argument also follows certain conventions:

    1. For each field, there will be a rank-2 type variable whose kind matches
       the type of the field, followed by a matching 'Sing' type. For instance,
       in the above example, @forall (x :: a). 'Sing' x@ corresponds to the
       first field of @MyCons@.

    2. In addition, if the field is a recursive occurrence of the data type,
       an additional argument will follow the 'Sing' type. This is best
       explained using the above example. In the @MyCons@ constructor, the second
       field (of type @MyCons a@) is a recursive occurrence of @MyCons@, so
       that corresponds to the type
       @forall (xs :: MyList a). 'Sing' xs -> 'Apply' p xs@, where @'Apply' p xs@
       is only present due to the recursion.

    3. Finally, the return type will be the predicate type variable applied
       to a saturated occurrence of the data constructor
       (@'Apply' p (MyCons x xs)@, in the above example).

* You'll need to enable lots of GHC extensions in order for the code generated
  by 'deriveElim' to typecheck. You'll need at least the following:

    * @AllowAmbiguousTypes@

    * @DataKinds@

    * @GADTs@

    * @PolyKinds@

    * @RankNTypes@

    * @ScopedTypeVariables@

    * @TemplateHaskell@

    * @TypeApplications@

* 'deriveElim' doesn't support every possible data type at the moment.
  It is known not to work for the following:

    * Data types defined using @GADTs@ or @ExistentialQuantification@

    * Data family instances

    * Data types which use polymorphic recursion
      (e.g., @data Foo a = Foo (Foo a)@)
-}

-- | @'deriveElim' dataName@ generates a top-level elimination function for the
-- datatype @dataName@. The eliminator will follow these naming conventions:
--
-- * If the datatype has an alphanumeric name, its eliminator will have that name
--   with @elim@ prepended.
--
-- * If the datatype has a symbolic name, its eliminator will have that name
--   with @~>@ prepended.
deriveElim :: Name -> Q [Dec]
deriveElim :: Name -> Q [Dec]
deriveElim Name
dataName = String -> Name -> Q [Dec]
deriveElimNamed (Name -> String
eliminatorName Name
dataName) Name
dataName

-- | @'deriveElimNamed' funName dataName@ generates a top-level elimination
-- function named @funName@ for the datatype @dataName@.
deriveElimNamed :: String -> Name -> Q [Dec]
deriveElimNamed :: String -> Name -> Q [Dec]
deriveElimNamed = Proxy 'IsTerm -> String -> Name -> Q [Dec]
forall (t :: TermOrType) (proxy :: TermOrType -> *).
Eliminator t =>
proxy t -> String -> Name -> Q [Dec]
deriveElimNamed' (forall {k} (t :: k). Proxy t
forall (t :: TermOrType). Proxy t
Proxy @IsTerm)

{- $type-conventions
'deriveTypeElim' and 'deriveTypeElimNamed' are like 'deriveElim' and
'deriveElimNamed' except that they create /type/-level eliminators instead of
term-level ones. Here is an example showing how one might use
'deriveTypeElim':

@
data MyList a = MyNil | MyCons a (MyList a)
$('deriveTypeElim' ''MyList)
@

This will produce an eliminator function that looks roughly like the following:

@
type ElimMyList :: forall (a :: 'Type').
                   forall (p :: MyList a '~>' 'Type') (l :: MyList a)
                -> 'Apply' p MyNil
                -> (forall (x :: a) (xs :: MyList a)
                     -> 'Apply' p xs '~>' 'Apply' p (MyCons x xs))
                -> 'Apply' p l
type family ElimMyList p l pMyNil pMyCons where
  forall (a :: 'Type')
         (p :: MyList a ~> 'Type')
         (pMyNil :: 'Apply' p MyNil)
         (pMyCons :: forall (x :: a) (xs :: MyList a)
                      -> 'Apply' p xs '~>' 'Apply' p (MyCons x xs)).
    ElimMyList @a p MyNil pMyNil pMyCons =
      pMyNil
  forall (a :: 'Type')
         (p :: MyList a ~> 'Type')
         (_pMyNil :: 'Apply' p MyNil)
         (pMyCons :: forall (x :: a) (xs :: MyList a)
                      -> 'Apply' p xs '~>' 'Apply' p (MyCons x xs))
         x' xs'.
    ElimMyList @a p (MyCons x' xs') pMyNil pMyCons =
      'Apply' (pMyCons x' xs') (ElimMyList @a p xs' pMyNil pMyCons)
@

Note the following differences from a term-level eliminator that 'deriveElim'
would generate:

* Type-level eliminators do not use 'Sing'. Instead, they use visible dependent
  quantification. That is, instead of generating
  @forall (x :: a). Sing x -> ...@ (as a term-level eliminator would do), a
  type-level eliminator would use @forall (x :: a) -> ...@.

* Term-level eliminators quantify @p@ with an invisible @forall@, whereas
  type-level eliminators quantify @p@ with a visible @forall@. (Really, @p@
  ought to be quantified visibly in both forms of eliminator, but GHC does not
  yet support visible dependent quantification at the term level.)

* Type-level eliminators use ('~>') in certain places where (@->@) would appear
  in term-level eliminators. For instance, note the use of
  @'Apply' p xs '~>' 'Apply' p (MyCons x xs)@ in @ElimMyList@ above. This is
  done to make it easier to use type-level eliminators with defunctionalization
  symbols (which aren't necessary for term-level eliminators).

  This comes with a notable drawback: type-level eliminators cannot support
  data constructors where recursive occurrences of the data type appear in a
  position other than the last field of a constructor. In other words,
  'deriveTypeElim' works on the @MyList@ example above, but not this variant:

  @
  data SnocList a = SnocNil | SnocCons (SnocList a) a
  @

  This is because @$('deriveTypeElim' ''SnocList)@ would generate an eliminator
  with the following kind:

  @
  type ElimSnocList :: forall (a :: 'Type').
                       forall (p :: SnocList a '~>' 'Type') (l :: SnocList a)
                    -> 'Apply' p SnocNil
                    -> (forall (xs :: SnocList a) -> 'Apply' p xs
                          '~>' (forall (x :: a) -> 'Apply' p (SnocCons x xs)))
                    -> 'Apply' p l
  @

  Unfortunately, the kind
  @'Apply' p xs '~>' (forall (x :: a) -> 'Apply' p (SnocCons x xs))@ is
  impredicative.

* In addition to the language extensions that 'deriveElim' requires, you'll need
  to enable these extensions in order to use 'deriveTypeElim':

    * @StandaloneKindSignatures@

    * @UndecidableInstances@
-}

-- | @'deriveTypeElim' dataName@ generates a type-level eliminator for the
-- datatype @dataName@. The eliminator will follow these naming conventions:
--
-- * If the datatype has an alphanumeric name, its eliminator will have that name
--   with @Elim@ prepended.
--
-- * If the datatype has a symbolic name, its eliminator will have that name
--   with @~>@ prepended.
deriveTypeElim :: Name -> Q [Dec]
deriveTypeElim :: Name -> Q [Dec]
deriveTypeElim Name
dataName = String -> Name -> Q [Dec]
deriveTypeElimNamed (String -> String
upcase (Name -> String
eliminatorName Name
dataName)) Name
dataName

-- | @'deriveTypeElimNamed' funName dataName@ generates a type-level eliminator
-- named @funName@ for the datatype @dataName@.
deriveTypeElimNamed :: String -> Name -> Q [Dec]
deriveTypeElimNamed :: String -> Name -> Q [Dec]
deriveTypeElimNamed = Proxy 'IsType -> String -> Name -> Q [Dec]
forall (t :: TermOrType) (proxy :: TermOrType -> *).
Eliminator t =>
proxy t -> String -> Name -> Q [Dec]
deriveElimNamed' (forall {k} (t :: k). Proxy t
forall (t :: TermOrType). Proxy t
Proxy @IsType)

-- The workhorse for deriveElim(Named). This generates either a term- or
-- type-level eliminator, depending on which Eliminator instance is used.
deriveElimNamed' ::
     Eliminator t
  => proxy t
  -> String  -- The name of the eliminator function
  -> Name    -- The name of the data type
  -> Q [Dec] -- The eliminator's type signature and body
deriveElimNamed' :: forall (t :: TermOrType) (proxy :: TermOrType -> *).
Eliminator t =>
proxy t -> String -> Name -> Q [Dec]
deriveElimNamed' proxy t
prox String
funName Name
dataName = do
  info :: DatatypeInfo
info@(DatatypeInfo { datatypeVars :: DatatypeInfo -> [TyVarBndrUnit]
datatypeVars      = [TyVarBndrUnit]
dataVarBndrs
                     , datatypeInstTypes :: DatatypeInfo -> [Type]
datatypeInstTypes = [Type]
instTys
                     , datatypeVariant :: DatatypeInfo -> DatatypeVariant
datatypeVariant   = DatatypeVariant
variant
                     , datatypeCons :: DatatypeInfo -> [ConstructorInfo]
datatypeCons      = [ConstructorInfo]
cons
                     }) <- Name -> Q DatatypeInfo
reifyDatatype Name
dataName
  let noDataFamilies :: Q a
noDataFamilies =
        String -> Q a
forall a. String -> Q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Eliminators for data family instances are currently not supported"
  case DatatypeVariant
variant of
    DatatypeVariant
DataInstance    -> Q ()
forall {a}. Q a
noDataFamilies
    DatatypeVariant
NewtypeInstance -> Q ()
forall {a}. Q a
noDataFamilies
    DatatypeVariant
Datatype        -> () -> Q ()
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    DatatypeVariant
Newtype         -> () -> Q ()
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  Name
predVar <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"p"
  Name
singVar <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"s"
  let elimName :: Name
elimName = String -> Name
mkName String
funName
      promDataKind :: Type
promDataKind = DatatypeInfo -> Type
datatypeType DatatypeInfo
info
      predVarBndr :: TyVarBndrUnit
predVarBndr = Name -> Type -> TyVarBndrUnit
kindedTV Name
predVar (Type -> Name -> Type -> Type
InfixT Type
promDataKind ''(~>) (Name -> Type
ConT ''Kind.Type))
      singVarBndr :: TyVarBndrUnit
singVarBndr = Name -> Type -> TyVarBndrUnit
kindedTV Name
singVar Type
promDataKind
  [Type]
caseTypes <- (ConstructorInfo -> Q Type) -> [ConstructorInfo] -> Q [Type]
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) -> [a] -> f [b]
traverse (proxy t -> Name -> Name -> ConstructorInfo -> Q Type
forall (t :: TermOrType) (proxy :: TermOrType -> *).
Eliminator t =>
proxy t -> Name -> Name -> ConstructorInfo -> Q Type
caseType proxy t
prox Name
dataName Name
predVar) [ConstructorInfo]
cons
  Bool -> Q () -> Q ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Int] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (DatatypeInfo -> [Int]
findParams DatatypeInfo
info) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
instTys) (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$
    String -> Q ()
forall a. String -> Q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Eliminators for polymorphically recursive data types are currently not supported"
  let returnType :: Type
returnType  = Name -> Type -> Type
predType Name
predVar (Name -> Type
VarT Name
singVar)
      elimType :: Type
elimType    = proxy t
-> [TyVarBndrUnit]
-> TyVarBndrUnit
-> TyVarBndrUnit
-> [Type]
-> Type
-> Type
forall (t :: TermOrType) (proxy :: TermOrType -> *).
Eliminator t =>
proxy t
-> [TyVarBndrUnit]
-> TyVarBndrUnit
-> TyVarBndrUnit
-> [Type]
-> Type
-> Type
forall (proxy :: TermOrType -> *).
proxy t
-> [TyVarBndrUnit]
-> TyVarBndrUnit
-> TyVarBndrUnit
-> [Type]
-> Type
-> Type
elimTypeSig proxy t
prox [TyVarBndrUnit]
dataVarBndrs TyVarBndrUnit
predVarBndr TyVarBndrUnit
singVarBndr
                                [Type]
caseTypes Type
returnType
  Dec
elimEqns <- proxy t
-> Name
-> Name
-> [TyVarBndrUnit]
-> TyVarBndrUnit
-> TyVarBndrUnit
-> [Type]
-> [ConstructorInfo]
-> Q Dec
forall (t :: TermOrType) (proxy :: TermOrType -> *).
Eliminator t =>
proxy t
-> Name
-> Name
-> [TyVarBndrUnit]
-> TyVarBndrUnit
-> TyVarBndrUnit
-> [Type]
-> [ConstructorInfo]
-> Q Dec
forall (proxy :: TermOrType -> *).
proxy t
-> Name
-> Name
-> [TyVarBndrUnit]
-> TyVarBndrUnit
-> TyVarBndrUnit
-> [Type]
-> [ConstructorInfo]
-> Q Dec
qElimEqns proxy t
prox (String -> Name
mkName String
funName) Name
dataName
                        [TyVarBndrUnit]
dataVarBndrs TyVarBndrUnit
predVarBndr TyVarBndrUnit
singVarBndr
                        [Type]
caseTypes [ConstructorInfo]
cons
  [Dec] -> Q [Dec]
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [proxy t -> Name -> Type -> Dec
forall (t :: TermOrType) (proxy :: TermOrType -> *).
Eliminator t =>
proxy t -> Name -> Type -> Dec
forall (proxy :: TermOrType -> *). proxy t -> Name -> Type -> Dec
elimSigD proxy t
prox Name
elimName Type
elimType, Dec
elimEqns]

-- Generate the type for a "case alternative" in an eliminator function's type
-- signature, which is done on a constructor-by-constructor basis.
caseType ::
     Eliminator t
  => proxy t
  -> Name            -- The name of the data type
  -> Name            -- The predicate type variable
  -> ConstructorInfo -- The data constructor
  -> Q Type          -- The full case type
caseType :: forall (t :: TermOrType) (proxy :: TermOrType -> *).
Eliminator t =>
proxy t -> Name -> Name -> ConstructorInfo -> Q Type
caseType proxy t
prox Name
dataName Name
predVar
         (ConstructorInfo { constructorName :: ConstructorInfo -> Name
constructorName    = Name
conName
                          , constructorVars :: ConstructorInfo -> [TyVarBndrUnit]
constructorVars    = [TyVarBndrUnit]
conVars
                          , constructorContext :: ConstructorInfo -> [Type]
constructorContext = [Type]
conContext
                          , constructorFields :: ConstructorInfo -> [Type]
constructorFields  = [Type]
fieldTypes })
  = do Bool -> Q () -> Q ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([TyVarBndrUnit] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyVarBndrUnit]
conVars Bool -> Bool -> Bool
&& [Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
conContext) (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$
         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] -> String
unlines
           [ String
"Eliminators for GADTs or datatypes with existentially quantified"
           , String
"data constructors currently not supported"
           ]
       [Name]
vars <- String -> Int -> Q [Name]
newNameList String
"f" (Int -> Q [Name]) -> Int -> Q [Name]
forall a b. (a -> b) -> a -> b
$ [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
fieldTypes
       let returnType :: Type
returnType = Name -> Type -> Type
predType Name
predVar
                                 ((Type -> Type -> Type) -> Type -> [Type] -> Type
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Type -> Type -> Type
AppT (Name -> Type
ConT Name
conName) ((Name -> Type) -> [Name] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Type
VarT [Name]
vars))
       Type -> Q Type
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> Q Type) -> Type -> Q Type
forall a b. (a -> b) -> a -> b
$ ((Name, Type) -> Type -> Type) -> Type -> [(Name, Type)] -> Type
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr' (\(Name
var, Type
varType) Type
t ->
                        proxy t -> Name -> Name -> Name -> Type -> Type -> Type
forall (t :: TermOrType) (proxy :: TermOrType -> *).
Eliminator t =>
proxy t -> Name -> Name -> Name -> Type -> Type -> Type
forall (proxy :: TermOrType -> *).
proxy t -> Name -> Name -> Name -> Type -> Type -> Type
prependElimCaseTypeVar proxy t
prox Name
dataName Name
predVar Name
var Type
varType Type
t)
                     Type
returnType
                     ([Name] -> [Type] -> [(Name, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
vars [Type]
fieldTypes)

-- Generate a single clause for a term-level eliminator's @go@ function.
goCaseClause ::
     Name            -- The name of the @go@ function
  -> Name            -- The name of the data type
  -> Name            -- The name of the "case alternative" to apply on the right-hand side
  -> ConstructorInfo -- The data constructor
  -> Q Clause        -- The generated function clause
goCaseClause :: Name -> Name -> Name -> ConstructorInfo -> Q Clause
goCaseClause Name
goName Name
dataName Name
usedCaseVar
    (ConstructorInfo { constructorName :: ConstructorInfo -> Name
constructorName   = Name
conName
                     , constructorFields :: ConstructorInfo -> [Type]
constructorFields = [Type]
fieldTypes })
  = do let numFields :: Int
numFields = [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
fieldTypes
       [Name]
singVars    <- String -> Int -> Q [Name]
newNameList String
"s"   Int
numFields
       [Name]
singVarSigs <- String -> Int -> Q [Name]
newNameList String
"sTy" Int
numFields
       let singConName :: Name
singConName = Options -> Name -> Name
singledDataConName Options
defaultOptions Name
conName
           mkSingVarPat :: Name -> Name -> Pat
mkSingVarPat Name
var Name
varSig = Pat -> Type -> Pat
SigP (Name -> Pat
VarP Name
var) (Name -> Type
singType Name
varSig)
           singVarPats :: [Pat]
singVarPats = (Name -> Name -> Pat) -> [Name] -> [Name] -> [Pat]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Name -> Name -> Pat
mkSingVarPat [Name]
singVars [Name]
singVarSigs

           mbInductiveArg :: Name -> Name -> Type -> Maybe Exp
mbInductiveArg Name
singVar Name
singVarSig Type
varType =
             let inductiveArg :: Exp
inductiveArg = Name -> Exp
VarE Name
goName Exp -> Type -> Exp
`AppTypeE` Name -> Type
VarT Name
singVarSig
                                            Exp -> Exp -> Exp
`AppE`     Name -> Exp
VarE Name
singVar
             in Name -> Type -> ([TypeArg] -> Exp) -> Maybe Exp
forall a. Name -> Type -> ([TypeArg] -> a) -> Maybe a
mbInductiveCase Name
dataName Type
varType (([TypeArg] -> Exp) -> Maybe Exp)
-> ([TypeArg] -> Exp) -> Maybe Exp
forall a b. (a -> b) -> a -> b
$ Exp -> [TypeArg] -> Exp
forall a b. a -> b -> a
const Exp
inductiveArg
           mkArg :: Exp -> (Name, Name, Type) -> Exp
mkArg Exp
f (Name
singVar, Name
singVarSig, Type
varType) =
             Exp -> [Exp] -> Exp
foldAppE Exp
f ([Exp] -> Exp) -> [Exp] -> Exp
forall a b. (a -> b) -> a -> b
$ Name -> Exp
VarE Name
singVar
                        Exp -> [Exp] -> [Exp]
forall a. a -> [a] -> [a]
: Maybe Exp -> [Exp]
forall a. Maybe a -> [a]
maybeToList (Name -> Name -> Type -> Maybe Exp
mbInductiveArg Name
singVar Name
singVarSig Type
varType)
           rhs :: Exp
rhs = (Exp -> (Name, Name, Type) -> Exp)
-> Exp -> [(Name, Name, Type)] -> Exp
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Exp -> (Name, Name, Type) -> Exp
mkArg (Name -> Exp
VarE Name
usedCaseVar) ([(Name, Name, Type)] -> Exp) -> [(Name, Name, Type)] -> Exp
forall a b. (a -> b) -> a -> b
$
                        [Name] -> [Name] -> [Type] -> [(Name, Name, Type)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [Name]
singVars [Name]
singVarSigs [Type]
fieldTypes
       Clause -> Q Clause
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Clause -> Q Clause) -> Clause -> Q Clause
forall a b. (a -> b) -> a -> b
$ [Pat] -> Body -> [Dec] -> Clause
Clause [Name -> [Type] -> [Pat] -> Pat
ConP Name
singConName [] [Pat]
singVarPats]
                     (Exp -> Body
NormalB Exp
rhs)
                     []

-- Generate a single equation for a type-level eliminator.
--
-- This code is fairly similar in structure to caseClause, but different
-- enough in subtle ways that I did not attempt to de-duplicate this code as
-- a method of the Eliminator class.
caseTySynEqn ::
     Name            -- The name of the eliminator function
  -> Name            -- The name of the data type
  -> [TyVarBndrUnit] -- The type variables bound by the data type
  -> TyVarBndrUnit   -- The predicate type variable
  -> Int             -- The index of this constructor (0-indexed)
  -> [Type]          -- The types of each "case alternative" in the eliminator
                     -- function's type signature
  -> ConstructorInfo -- The data constructor
  -> Q TySynEqn      -- The generated type family equation
caseTySynEqn :: Name
-> Name
-> [TyVarBndrUnit]
-> TyVarBndrUnit
-> Int
-> [Type]
-> ConstructorInfo
-> Q TySynEqn
caseTySynEqn Name
elimName Name
dataName [TyVarBndrUnit]
dataVarBndrs TyVarBndrUnit
predVarBndr Int
conIndex [Type]
caseTypes
    (ConstructorInfo { constructorName :: ConstructorInfo -> Name
constructorName   = Name
conName
                     , constructorFields :: ConstructorInfo -> [Type]
constructorFields = [Type]
fieldTypes })
  = do let dataVarNames :: [Name]
dataVarNames = (TyVarBndrUnit -> Name) -> [TyVarBndrUnit] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map TyVarBndrUnit -> Name
forall flag. TyVarBndr_ flag -> Name
tvName [TyVarBndrUnit]
dataVarBndrs
           predVarName :: Name
predVarName  = TyVarBndrUnit -> Name
forall flag. TyVarBndr_ flag -> Name
tvName TyVarBndrUnit
predVarBndr
           numFields :: Int
numFields    = [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
fieldTypes
       [Name]
singVars     <- String -> Int -> Q [Name]
newNameList String
"s" Int
numFields
       Name
usedCaseVar  <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"useThis"
       [TyVarBndrUnit]
caseVarBndrs <- ((Int -> Type -> Q TyVarBndrUnit) -> [Type] -> Q [TyVarBndrUnit])
-> [Type] -> (Int -> Type -> Q TyVarBndrUnit) -> Q [TyVarBndrUnit]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Int -> Type -> Q TyVarBndrUnit) -> [Type] -> Q [TyVarBndrUnit]
forall (f :: * -> *) a b.
Applicative f =>
(Int -> a -> f b) -> [a] -> f [b]
itraverse [Type]
caseTypes ((Int -> Type -> Q TyVarBndrUnit) -> Q [TyVarBndrUnit])
-> (Int -> Type -> Q TyVarBndrUnit) -> Q [TyVarBndrUnit]
forall a b. (a -> b) -> a -> b
$ \Int
i Type
caseTy ->
                         let mkVarName :: Q Name
mkVarName
                               | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
conIndex = Name -> Q Name
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Name
usedCaseVar
                               | Bool
otherwise     = String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName (String
"_p" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i)
                         in (Name -> Type -> TyVarBndrUnit)
-> Q Name -> Q Type -> Q TyVarBndrUnit
forall a b c. (a -> b -> c) -> Q a -> Q b -> Q c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Name -> Type -> TyVarBndrUnit
kindedTV Q Name
mkVarName (Type -> Q Type
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
caseTy)
       let caseVarNames :: [Name]
caseVarNames = (TyVarBndrUnit -> Name) -> [TyVarBndrUnit] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map TyVarBndrUnit -> Name
forall flag. TyVarBndr_ flag -> Name
tvName [TyVarBndrUnit]
caseVarBndrs
           prefix :: Type
prefix       = Type -> [Type] -> Type
foldAppKindT (Name -> Type
ConT Name
elimName) ([Type] -> Type) -> [Type] -> Type
forall a b. (a -> b) -> a -> b
$ (Name -> Type) -> [Name] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Type
VarT [Name]
dataVarNames
           mbInductiveArg :: Name -> Type -> Maybe Type
mbInductiveArg Name
singVar Type
varType =
             let inductiveArg :: Type
inductiveArg = Type -> [Type] -> Type
foldAppT Type
prefix ([Type] -> Type) -> [Type] -> Type
forall a b. (a -> b) -> a -> b
$ Name -> Type
VarT Name
predVarName
                                                Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: Name -> Type
VarT Name
singVar
                                                Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: (Name -> Type) -> [Name] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Type
VarT [Name]
caseVarNames
             in Name -> Type -> ([TypeArg] -> Type) -> Maybe Type
forall a. Name -> Type -> ([TypeArg] -> a) -> Maybe a
mbInductiveCase Name
dataName Type
varType (([TypeArg] -> Type) -> Maybe Type)
-> ([TypeArg] -> Type) -> Maybe Type
forall a b. (a -> b) -> a -> b
$ Type -> [TypeArg] -> Type
forall a b. a -> b -> a
const Type
inductiveArg
           mkArg :: Type -> (Name, Type) -> Type
mkArg Type
f (Name
singVar, Type
varType) =
             Type -> [Type] -> Type
foldAppDefunT (Type
f Type -> Type -> Type
`AppT` Name -> Type
VarT Name
singVar)
                         ([Type] -> Type) -> [Type] -> Type
forall a b. (a -> b) -> a -> b
$ Maybe Type -> [Type]
forall a. Maybe a -> [a]
maybeToList (Name -> Type -> Maybe Type
mbInductiveArg Name
singVar Type
varType)
           bndrs :: [TyVarBndrUnit]
bndrs = [TyVarBndrUnit]
dataVarBndrs [TyVarBndrUnit] -> [TyVarBndrUnit] -> [TyVarBndrUnit]
forall a. [a] -> [a] -> [a]
++ TyVarBndrUnit
predVarBndr TyVarBndrUnit -> [TyVarBndrUnit] -> [TyVarBndrUnit]
forall a. a -> [a] -> [a]
: [TyVarBndrUnit]
caseVarBndrs [TyVarBndrUnit] -> [TyVarBndrUnit] -> [TyVarBndrUnit]
forall a. [a] -> [a] -> [a]
++ (Name -> TyVarBndrUnit) -> [Name] -> [TyVarBndrUnit]
forall a b. (a -> b) -> [a] -> [b]
map Name -> TyVarBndrUnit
plainTV [Name]
singVars
           lhs :: Type
lhs   = Type -> [Type] -> Type
foldAppT Type
prefix ([Type] -> Type) -> [Type] -> Type
forall a b. (a -> b) -> a -> b
$ Name -> Type
VarT Name
predVarName
                                   Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: Type -> [Type] -> Type
foldAppT (Name -> Type
ConT Name
conName) ((Name -> Type) -> [Name] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Type
VarT [Name]
singVars)
                                   Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: (Name -> Type) -> [Name] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Type
VarT [Name]
caseVarNames
           rhs :: Type
rhs   = (Type -> (Name, Type) -> Type) -> Type -> [(Name, Type)] -> Type
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Type -> (Name, Type) -> Type
mkArg (Name -> Type
VarT Name
usedCaseVar) ([(Name, Type)] -> Type) -> [(Name, Type)] -> Type
forall a b. (a -> b) -> a -> b
$ [Name] -> [Type] -> [(Name, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
singVars [Type]
fieldTypes
       TySynEqn -> Q TySynEqn
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TySynEqn -> Q TySynEqn) -> TySynEqn -> Q TySynEqn
forall a b. (a -> b) -> a -> b
$ Maybe [TyVarBndrUnit] -> Type -> Type -> TySynEqn
TySynEqn ([TyVarBndrUnit] -> Maybe [TyVarBndrUnit]
forall a. a -> Maybe a
Just [TyVarBndrUnit]
bndrs) Type
lhs Type
rhs

-- Are we dealing with a term or a type?
data TermOrType
  = IsTerm
  | IsType

-- A class that abstracts out certain common operations that one must perform
-- for both term- and type-level eliminators.
class Eliminator (t :: TermOrType) where
  -- Create the Dec for an eliminator function's type signature.
  elimSigD ::
       proxy t
    -> Name -- The name of the eliminator function
    -> Type -- The type of the eliminator function
    -> Dec  -- The type signature Dec (SigD or KiSigD)

  -- Create an eliminator function's type.
  elimTypeSig ::
       proxy t
    -> [TyVarBndrUnit] -- The type variables bound by the data type
    -> TyVarBndrUnit   -- The predicate type variable
    -> TyVarBndrUnit   -- The type variable whose kind is that of the data type itself
    -> [Type]          -- The types of each "case alternative" in the eliminator
                       -- function's type signature
    -> Type            -- The eliminator function's return type
    -> Type            -- The full type

  -- Take a data constructor's field type and prepend it to a "case
  -- alternative" in an eliminator function's type signature.
  prependElimCaseTypeVar ::
       proxy t
    -> Name -- The name of the data type
    -> Name -- The predicate type variable
    -> Name -- A fresh type variable name
    -> Kind -- The field type
    -> Type -- The rest of the "case alternative" type
    -> Type -- The "case alternative" type after prepending

  -- Generate the clauses/equations for the body of the eliminator function.
  qElimEqns ::
       proxy t
    -> Name              -- The name of the eliminator function
    -> Name              -- The name of the data type
    -> [TyVarBndrUnit]   -- The type variables bound by the data type
    -> TyVarBndrUnit     -- The predicate type variable
    -> TyVarBndrUnit     -- The type variable whose kind is that of the data type itself
    -> [Type]            -- The types of each "case alternative" in the eliminator
                         -- function's type signature
    -> [ConstructorInfo] -- The data constructors
    -> Q Dec             -- The Dec containing the clauses/equations

instance Eliminator IsTerm where
  elimSigD :: forall (proxy :: TermOrType -> *).
proxy 'IsTerm -> Name -> Type -> Dec
elimSigD proxy 'IsTerm
_ = Name -> Type -> Dec
SigD

  elimTypeSig :: forall (proxy :: TermOrType -> *).
proxy 'IsTerm
-> [TyVarBndrUnit]
-> TyVarBndrUnit
-> TyVarBndrUnit
-> [Type]
-> Type
-> Type
elimTypeSig proxy 'IsTerm
_ [TyVarBndrUnit]
dataVarBndrs TyVarBndrUnit
predVarBndr TyVarBndrUnit
singVarBndr [Type]
caseTypes Type
returnType =
    [TyVarBndr Specificity] -> [Type] -> Type -> Type
ForallT (Specificity -> [TyVarBndrUnit] -> [TyVarBndr Specificity]
forall newFlag oldFlag.
newFlag -> [TyVarBndr_ oldFlag] -> [TyVarBndr_ newFlag]
changeTVFlags Specificity
SpecifiedSpec ([TyVarBndrUnit] -> [TyVarBndr Specificity])
-> [TyVarBndrUnit] -> [TyVarBndr Specificity]
forall a b. (a -> b) -> a -> b
$
             [TyVarBndrUnit]
dataVarBndrs [TyVarBndrUnit] -> [TyVarBndrUnit] -> [TyVarBndrUnit]
forall a. [a] -> [a] -> [a]
++ [TyVarBndrUnit
predVarBndr, TyVarBndrUnit
singVarBndr]) [] (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
    [Type] -> Type -> Type
ravel (Name -> Type
singType (TyVarBndrUnit -> Name
forall flag. TyVarBndr_ flag -> Name
tvName TyVarBndrUnit
singVarBndr)Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
caseTypes) Type
returnType

  prependElimCaseTypeVar :: forall (proxy :: TermOrType -> *).
proxy 'IsTerm -> Name -> Name -> Name -> Type -> Type -> Type
prependElimCaseTypeVar proxy 'IsTerm
_ Name
dataName Name
predVar Name
var Type
varType Type
t =
    [TyVarBndr Specificity] -> [Type] -> Type -> Type
ForallT [Name -> Type -> TyVarBndr Specificity
kindedTVSpecified Name
var Type
varType] [] (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
    [Type] -> Type -> Type
ravel (Name -> Type
singType Name
varType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:Maybe Type -> [Type]
forall a. Maybe a -> [a]
maybeToList (Name -> Name -> Name -> Type -> Maybe Type
mbInductiveType Name
dataName Name
predVar Name
var Type
varType)) Type
t

  -- A unique characteristic of term-level eliminators is that we manually
  -- apply the static argument transformation, e.g.,
  --
  --   elimT :: forall a (p :: T a ~> Type) (t :: T a).
  --            Sing t
  --         -> (forall (x :: a) (xs :: T a).
  --               Sing x -> Sing xs -> Apply p xs -> Apply p (MkT x xs))
  --         -> Apply p t
  --   elimT st k = go @s k
  --     where
  --       go :: forall (t' :: T a).
  --             Sing t' -> Apply p t'
  --       go (SMkT (sx :: Sing x) (sxs :: Sing xs)) =
  --         k sx sxs (go @xs sxs)
  --
  -- This reduces the likelihood of recursive calls falling afoul of GHC's
  -- ambiguity check.
  qElimEqns :: forall (proxy :: TermOrType -> *).
proxy 'IsTerm
-> Name
-> Name
-> [TyVarBndrUnit]
-> TyVarBndrUnit
-> TyVarBndrUnit
-> [Type]
-> [ConstructorInfo]
-> Q Dec
qElimEqns proxy 'IsTerm
_ Name
elimName Name
dataName [TyVarBndrUnit]
_dataVarBndrs TyVarBndrUnit
predVarBndr TyVarBndrUnit
singVarBndr [Type]
_caseTypes [ConstructorInfo]
cons = do
    Name
singTermVar <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"s"
    [Name]
caseVars    <- String -> Int -> Q [Name]
newNameList String
"p" (Int -> Q [Name]) -> Int -> Q [Name]
forall a b. (a -> b) -> a -> b
$ [ConstructorInfo] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ConstructorInfo]
cons
    Name
goName      <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"go"
    let singTypeVar :: Name
singTypeVar = TyVarBndrUnit -> Name
forall flag. TyVarBndr_ flag -> Name
tvName TyVarBndrUnit
singVarBndr
    Name
goSingTypeVar <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName (String -> Q Name) -> String -> Q Name
forall a b. (a -> b) -> a -> b
$ Name -> String
nameBase Name
singTypeVar
    let elimRHS :: Exp
elimRHS       = Name -> Exp
VarE Name
goName Exp -> Type -> Exp
`AppTypeE` Name -> Type
VarT Name
singTypeVar Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
singTermVar
        goSingVarBndr :: TyVarBndrUnit
goSingVarBndr = (Name -> Name) -> TyVarBndrUnit -> TyVarBndrUnit
forall flag. (Name -> Name) -> TyVarBndr_ flag -> TyVarBndr_ flag
mapTVName (Name -> Name -> Name
forall a b. a -> b -> a
const Name
goSingTypeVar) TyVarBndrUnit
singVarBndr
        goReturnType :: Type
goReturnType  = Name -> Type -> Type
predType (TyVarBndrUnit -> Name
forall flag. TyVarBndr_ flag -> Name
tvName TyVarBndrUnit
predVarBndr) (Name -> Type
VarT Name
goSingTypeVar)
        goType :: Type
goType = [TyVarBndr Specificity] -> [Type] -> Type -> Type
ForallT (Specificity -> [TyVarBndrUnit] -> [TyVarBndr Specificity]
forall newFlag oldFlag.
newFlag -> [TyVarBndr_ oldFlag] -> [TyVarBndr_ newFlag]
changeTVFlags Specificity
SpecifiedSpec [TyVarBndrUnit
goSingVarBndr]) [] (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
                 Type
ArrowT Type -> Type -> Type
`AppT` Name -> Type
singType Name
goSingTypeVar Type -> Type -> Type
`AppT` Type
goReturnType
    [Clause]
goClauses
      <- if [ConstructorInfo] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ConstructorInfo]
cons
         then [Clause] -> Q [Clause]
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [[Pat] -> Body -> [Dec] -> Clause
Clause [Name -> Pat
VarP Name
singTermVar] (Exp -> Body
NormalB (Exp -> [Match] -> Exp
CaseE (Name -> Exp
VarE Name
singTermVar) [])) []]
         else (Name -> ConstructorInfo -> Q Clause)
-> [Name] -> [ConstructorInfo] -> Q [Clause]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (Name -> Name -> Name -> ConstructorInfo -> Q Clause
goCaseClause Name
goName Name
dataName) [Name]
caseVars [ConstructorInfo]
cons
    Dec -> Q Dec
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Dec -> Q Dec) -> Dec -> Q Dec
forall a b. (a -> b) -> a -> b
$ Name -> [Clause] -> Dec
FunD Name
elimName [ [Pat] -> Body -> [Dec] -> Clause
Clause ((Name -> Pat) -> [Name] -> [Pat]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Pat
VarP (Name
singTermVarName -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:[Name]
caseVars)) (Exp -> Body
NormalB Exp
elimRHS)
                                  [Name -> Type -> Dec
SigD Name
goName Type
goType, Name -> [Clause] -> Dec
FunD Name
goName [Clause]
goClauses] ]

instance Eliminator IsType where
  elimSigD :: forall (proxy :: TermOrType -> *).
proxy 'IsType -> Name -> Type -> Dec
elimSigD proxy 'IsType
_ = Name -> Type -> Dec
KiSigD

  elimTypeSig :: forall (proxy :: TermOrType -> *).
proxy 'IsType
-> [TyVarBndrUnit]
-> TyVarBndrUnit
-> TyVarBndrUnit
-> [Type]
-> Type
-> Type
elimTypeSig proxy 'IsType
_ [TyVarBndrUnit]
dataVarBndrs TyVarBndrUnit
predVarBndr TyVarBndrUnit
singVarBndr [Type]
caseTypes Type
returnType =
    [TyVarBndr Specificity] -> [Type] -> Type -> Type
ForallT (Specificity -> [TyVarBndrUnit] -> [TyVarBndr Specificity]
forall newFlag oldFlag.
newFlag -> [TyVarBndr_ oldFlag] -> [TyVarBndr_ newFlag]
changeTVFlags Specificity
SpecifiedSpec [TyVarBndrUnit]
dataVarBndrs) [] (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
    [TyVarBndrUnit] -> Type -> Type
ForallVisT [TyVarBndrUnit
predVarBndr, TyVarBndrUnit
singVarBndr] (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
    [Type] -> Type -> Type
ravel [Type]
caseTypes Type
returnType

  prependElimCaseTypeVar :: forall (proxy :: TermOrType -> *).
proxy 'IsType -> Name -> Name -> Name -> Type -> Type -> Type
prependElimCaseTypeVar proxy 'IsType
_ Name
dataName Name
predVar Name
var Type
varType Type
t =
    [TyVarBndrUnit] -> Type -> Type
ForallVisT [Name -> Type -> TyVarBndrUnit
kindedTV Name
var Type
varType] (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
    [Type] -> Type -> Type
ravelDefun (Maybe Type -> [Type]
forall a. Maybe a -> [a]
maybeToList (Name -> Name -> Name -> Type -> Maybe Type
mbInductiveType Name
dataName Name
predVar Name
var Type
varType)) Type
t

  qElimEqns :: forall (proxy :: TermOrType -> *).
proxy 'IsType
-> Name
-> Name
-> [TyVarBndrUnit]
-> TyVarBndrUnit
-> TyVarBndrUnit
-> [Type]
-> [ConstructorInfo]
-> Q Dec
qElimEqns proxy 'IsType
_ Name
elimName Name
dataName [TyVarBndrUnit]
dataVarBndrs TyVarBndrUnit
predVarBndr TyVarBndrUnit
singVarBndr [Type]
caseTypes [ConstructorInfo]
cons = do
    [TyVarBndrUnit]
caseVarBndrs <- Int -> Q TyVarBndrUnit -> Q [TyVarBndrUnit]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM ([Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
caseTypes) (Name -> TyVarBndrUnit
plainTV (Name -> TyVarBndrUnit) -> Q Name -> Q TyVarBndrUnit
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"p")
    let predVar :: Name
predVar   = TyVarBndrUnit -> Name
forall flag. TyVarBndr_ flag -> Name
tvName TyVarBndrUnit
predVarBndr
        singVar :: Name
singVar   = TyVarBndrUnit -> Name
forall flag. TyVarBndr_ flag -> Name
tvName TyVarBndrUnit
singVarBndr
        tyFamHead :: TypeFamilyHead
tyFamHead = Name
-> [TyVarBndrUnit]
-> FamilyResultSig
-> Maybe InjectivityAnn
-> TypeFamilyHead
TypeFamilyHead Name
elimName
                      (Name -> TyVarBndrUnit
plainTV Name
predVarTyVarBndrUnit -> [TyVarBndrUnit] -> [TyVarBndrUnit]
forall a. a -> [a] -> [a]
:Name -> TyVarBndrUnit
plainTV Name
singVarTyVarBndrUnit -> [TyVarBndrUnit] -> [TyVarBndrUnit]
forall a. a -> [a] -> [a]
:[TyVarBndrUnit]
caseVarBndrs)
                      FamilyResultSig
NoSig Maybe InjectivityAnn
forall a. Maybe a
Nothing
    [TySynEqn]
caseEqns <- (Int -> ConstructorInfo -> Q TySynEqn)
-> [ConstructorInfo] -> Q [TySynEqn]
forall (f :: * -> *) a b.
Applicative f =>
(Int -> a -> f b) -> [a] -> f [b]
itraverse (\Int
i -> Name
-> Name
-> [TyVarBndrUnit]
-> TyVarBndrUnit
-> Int
-> [Type]
-> ConstructorInfo
-> Q TySynEqn
caseTySynEqn Name
elimName Name
dataName
                                 [TyVarBndrUnit]
dataVarBndrs TyVarBndrUnit
predVarBndr Int
i [Type]
caseTypes) [ConstructorInfo]
cons
    Dec -> Q Dec
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Dec -> Q Dec) -> Dec -> Q Dec
forall a b. (a -> b) -> a -> b
$ TypeFamilyHead -> [TySynEqn] -> Dec
ClosedTypeFamilyD TypeFamilyHead
tyFamHead [TySynEqn]
caseEqns

mbInductiveType :: Name -> Name -> Name -> Kind -> Maybe Type
mbInductiveType :: Name -> Name -> Name -> Type -> Maybe Type
mbInductiveType Name
dataName Name
predVar Name
var Type
varType =
  Name -> Type -> ([TypeArg] -> Type) -> Maybe Type
forall a. Name -> Type -> ([TypeArg] -> a) -> Maybe a
mbInductiveCase Name
dataName Type
varType (([TypeArg] -> Type) -> Maybe Type)
-> ([TypeArg] -> Type) -> Maybe Type
forall a b. (a -> b) -> a -> b
$ Type -> [TypeArg] -> Type
forall a b. a -> b -> a
const (Type -> [TypeArg] -> Type) -> Type -> [TypeArg] -> Type
forall a b. (a -> b) -> a -> b
$ Name -> Type -> Type
predType Name
predVar (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Name -> Type
VarT Name
var

mbInductiveCase :: Name -> Type -> ([TypeArg] -> a) -> Maybe a
mbInductiveCase :: forall a. Name -> Type -> ([TypeArg] -> a) -> Maybe a
mbInductiveCase Name
dataName Type
varType [TypeArg] -> a
inductiveArg
  = case Type -> (Type, [TypeArg])
unfoldType Type
varType of
      (Type
headTy, [TypeArg]
argTys)
          -- Annoying special case for lists
        | Type
ListT <- Type
headTy
        , Name
dataName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''[]
       -> a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe a
forall a b. (a -> b) -> a -> b
$ [TypeArg] -> a
inductiveArg [TypeArg]
argTys

        | ConT Name
n <- Type
headTy
        , Name
dataName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n
       -> a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe a
forall a b. (a -> b) -> a -> b
$ [TypeArg] -> a
inductiveArg [TypeArg]
argTys

        | Bool
otherwise
       -> Maybe a
forall a. Maybe a
Nothing

-- | Construct a type of the form @'Sing' x@ given @x@.
singType :: Name -> Type
singType :: Name -> Type
singType Name
x = Name -> Type
ConT ''Sing Type -> Type -> Type
`AppT` Name -> Type
VarT Name
x

-- | Construct a type of the form @'Apply' p ty@ given @p@ and @ty@.
predType :: Name -> Type -> Type
predType :: Name -> Type -> Type
predType Name
p Type
ty = Name -> Type
ConT ''Apply Type -> Type -> Type
`AppT` Name -> Type
VarT Name
p Type -> Type -> Type
`AppT` Type
ty

-- | Generate a list of fresh names with a common prefix, and numbered suffixes.
newNameList :: String -> Int -> Q [Name]
newNameList :: String -> Int -> Q [Name]
newNameList String
prefix Int
n = Int -> (Int -> Q Name) -> Q [Name]
forall (f :: * -> *) a.
Applicative f =>
Int -> (Int -> f a) -> f [a]
ireplicateA Int
n ((Int -> Q Name) -> Q [Name]) -> (Int -> Q Name) -> Q [Name]
forall a b. (a -> b) -> a -> b
$ String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName (String -> Q Name) -> (Int -> String) -> Int -> Q Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String
prefix ++) (String -> String) -> (Int -> String) -> Int -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String
forall a. Show a => a -> String
show

-- Compute an eliminator function's name from the data type name.
eliminatorName :: Name -> String
eliminatorName :: Name -> String
eliminatorName Name
n
  | Char
first:String
_ <- String
nStr
  , Char -> Bool
isUpper Char
first
  = String
"elim" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nStr

  | Bool
otherwise
  = String
"~>" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nStr
  where
    nStr :: String
nStr = Name -> String
nameBase Name
n

-- Construct a function type, separating the arguments with ->
ravel :: [Type] -> Type -> Type
ravel :: [Type] -> Type -> Type
ravel [Type]
args Type
res = [Type] -> Type
go [Type]
args
  where
    go :: [Type] -> Type
go []    = Type
res
    go (Type
h:[Type]
t) = Type -> Type -> Type
AppT (Type -> Type -> Type
AppT Type
ArrowT Type
h) ([Type] -> Type
go [Type]
t)

-- Construct a function type, separating the arguments with ~>
ravelDefun :: [Type] -> Type -> Type
ravelDefun :: [Type] -> Type -> Type
ravelDefun [Type]
args Type
res = [Type] -> Type
go [Type]
args
  where
    go :: [Type] -> Type
go []    = Type
res
    go (Type
h:[Type]
t) = Type -> Type -> Type
AppT (Type -> Type -> Type
AppT (Name -> Type
ConT ''(~>)) Type
h) ([Type] -> Type
go [Type]
t)

-- Apply an expression to a list of expressions using ordinary function applications.
foldAppE :: Exp -> [Exp] -> Exp
foldAppE :: Exp -> [Exp] -> Exp
foldAppE = (Exp -> Exp -> Exp) -> Exp -> [Exp] -> Exp
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Exp -> Exp -> Exp
AppE

-- Apply a type to a list of types using ordinary function applications.
foldAppT :: Type -> [Type] -> Type
foldAppT :: Type -> [Type] -> Type
foldAppT = (Type -> Type -> Type) -> Type -> [Type] -> Type
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Type -> Type -> Type
AppT

-- Apply a type to a list of types using defunctionalized applications
-- (i.e., using Apply from singletons).
foldAppDefunT :: Type -> [Type] -> Type
foldAppDefunT :: Type -> [Type] -> Type
foldAppDefunT = (Type -> Type -> Type) -> Type -> [Type] -> Type
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\Type
x Type
y -> Name -> Type
ConT ''Apply Type -> Type -> Type
`AppT` Type
x Type -> Type -> Type
`AppT` Type
y)

-- Apply a type to a list of types using visible kind applications.
foldAppKindT :: Type -> [Type] -> Type
foldAppKindT :: Type -> [Type] -> Type
foldAppKindT = (Type -> Type -> Type) -> Type -> [Type] -> Type
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Type -> Type -> Type
AppKindT

itraverse :: Applicative f => (Int -> a -> f b) -> [a] -> f [b]
itraverse :: forall (f :: * -> *) a b.
Applicative f =>
(Int -> a -> f b) -> [a] -> f [b]
itraverse Int -> a -> f b
f [a]
xs0 = [a] -> Int -> f [b]
go [a]
xs0 Int
0 where
  go :: [a] -> Int -> f [b]
go [] Int
_ = [b] -> f [b]
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
  go (a
x:[a]
xs) Int
n = (:) (b -> [b] -> [b]) -> f b -> f ([b] -> [b])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> a -> f b
f Int
n a
x f ([b] -> [b]) -> f [b] -> f [b]
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ([a] -> Int -> f [b]
go [a]
xs (Int -> f [b]) -> Int -> f [b]
forall a b. (a -> b) -> a -> b
$! (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1))

ireplicateA :: Applicative f => Int -> (Int -> f a) -> f [a]
ireplicateA :: forall (f :: * -> *) a.
Applicative f =>
Int -> (Int -> f a) -> f [a]
ireplicateA Int
cnt0 Int -> f a
f =
    Int -> Int -> f [a]
forall {t}. (Ord t, Num t) => t -> Int -> f [a]
loop Int
cnt0 Int
0
  where
    loop :: t -> Int -> f [a]
loop t
cnt Int
n
        | t
cnt t -> t -> Bool
forall a. Ord a => a -> a -> Bool
<= t
0  = [a] -> f [a]
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
        | Bool
otherwise = (a -> [a] -> [a]) -> f a -> f [a] -> f [a]
forall a b c. (a -> b -> c) -> f a -> f b -> f c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (:) (Int -> f a
f Int
n) (t -> Int -> f [a]
loop (t
cnt t -> t -> t
forall a. Num a => a -> a -> a
- t
1) (Int -> f [a]) -> Int -> f [a]
forall a b. (a -> b) -> a -> b
$! (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1))

-- | Find the data type constructor arguments that are parameters.
--
-- Parameters are names which are unchanged across the structure.
-- They appear at least once in every constructor type, always appear
-- in the same argument position(s), and nothing else ever appears in those
-- argument positions.
--
-- This was adapted from a similar algorithm used in Idris
-- (https://github.com/idris-lang/Idris-dev/blob/a13caeb4e50d0c096d34506f2ebf6b9d140a07aa/src/Idris/Elab/Utils.hs#L401-L468),
-- licensed under the BSD-3-Clause license.
findParams :: DatatypeInfo -> [Int]
findParams :: DatatypeInfo -> [Int]
findParams (DatatypeInfo { datatypeName :: DatatypeInfo -> Name
datatypeName      = Name
dataName
                         , datatypeInstTypes :: DatatypeInfo -> [Type]
datatypeInstTypes = [Type]
instTys
                         , datatypeCons :: DatatypeInfo -> [ConstructorInfo]
datatypeCons      = [ConstructorInfo]
cons
                         }) =
  let allapps :: [[[Maybe Name]]]
allapps = (ConstructorInfo -> [[Maybe Name]])
-> [ConstructorInfo] -> [[[Maybe Name]]]
forall a b. (a -> b) -> [a] -> [b]
map ConstructorInfo -> [[Maybe Name]]
getDataApp [ConstructorInfo]
cons
        -- do each constructor separately, then merge the results (names
        -- may change between constructors)
      conParams :: [[Int]]
conParams = ([[Maybe Name]] -> [Int]) -> [[[Maybe Name]]] -> [[Int]]
forall a b. (a -> b) -> [a] -> [b]
map [[Maybe Name]] -> [Int]
forall name. Eq name => [[Maybe name]] -> [Int]
paramPos [[[Maybe Name]]]
allapps
  in [[Int]] -> [Int]
forall pos. Eq pos => [[pos]] -> [pos]
inAll [[Int]]
conParams
  where
    inAll :: Eq pos => [[pos]] -> [pos]
    inAll :: forall pos. Eq pos => [[pos]] -> [pos]
inAll [] = []
    inAll ([pos]
x : [[pos]]
xs) = (pos -> Bool) -> [pos] -> [pos]
forall a. (a -> Bool) -> [a] -> [a]
filter (\pos
p -> ([pos] -> Bool) -> [[pos]] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\[pos]
ps -> pos
p pos -> [pos] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [pos]
ps) [[pos]]
xs) [pos]
x

    paramPos :: Eq name => [[Maybe name]] -> [Int]
    paramPos :: forall name. Eq name => [[Maybe name]] -> [Int]
paramPos [] = []
    paramPos ([Maybe name]
args : [[Maybe name]]
rest)
          = [(Int, Maybe name)] -> [Int]
forall pos name. [(pos, Maybe name)] -> [pos]
dropNothing ([(Int, Maybe name)] -> [Int]) -> [(Int, Maybe name)] -> [Int]
forall a b. (a -> b) -> a -> b
$ [(Int, Maybe name)] -> [[Maybe name]] -> [(Int, Maybe name)]
forall name pos.
Eq name =>
[(pos, Maybe name)] -> [[Maybe name]] -> [(pos, Maybe name)]
keepSame ([Int] -> [Maybe name] -> [(Int, Maybe name)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [Maybe name]
args) [[Maybe name]]
rest

    dropNothing :: [(pos, Maybe name)] -> [pos]
    dropNothing :: forall pos name. [(pos, Maybe name)] -> [pos]
dropNothing [] = []
    dropNothing ((pos
_, Maybe name
Nothing) : [(pos, Maybe name)]
ts) = [(pos, Maybe name)] -> [pos]
forall pos name. [(pos, Maybe name)] -> [pos]
dropNothing [(pos, Maybe name)]
ts
    dropNothing ((pos
x, Maybe name
_) : [(pos, Maybe name)]
ts) = pos
x pos -> [pos] -> [pos]
forall a. a -> [a] -> [a]
: [(pos, Maybe name)] -> [pos]
forall pos name. [(pos, Maybe name)] -> [pos]
dropNothing [(pos, Maybe name)]
ts

    keepSame :: Eq name =>
                [(pos, Maybe name)] -> [[Maybe name]] ->
                [(pos, Maybe name)]
    keepSame :: forall name pos.
Eq name =>
[(pos, Maybe name)] -> [[Maybe name]] -> [(pos, Maybe name)]
keepSame [(pos, Maybe name)]
as [] = [(pos, Maybe name)]
as
    keepSame [(pos, Maybe name)]
as ([Maybe name]
args : [[Maybe name]]
rest) = [(pos, Maybe name)] -> [[Maybe name]] -> [(pos, Maybe name)]
forall name pos.
Eq name =>
[(pos, Maybe name)] -> [[Maybe name]] -> [(pos, Maybe name)]
keepSame ([(pos, Maybe name)] -> [Maybe name] -> [(pos, Maybe name)]
forall name pos.
Eq name =>
[(pos, Maybe name)] -> [Maybe name] -> [(pos, Maybe name)]
update [(pos, Maybe name)]
as [Maybe name]
args) [[Maybe name]]
rest

    update :: Eq name => [(pos, Maybe name)] -> [Maybe name] -> [(pos, Maybe name)]
    update :: forall name pos.
Eq name =>
[(pos, Maybe name)] -> [Maybe name] -> [(pos, Maybe name)]
update [] [Maybe name]
_ = []
    update [(pos, Maybe name)]
_ [] = []
    update ((pos
n, Just name
x) : [(pos, Maybe name)]
as) (Just name
x' : [Maybe name]
args)
        | name
x name -> name -> Bool
forall a. Eq a => a -> a -> Bool
== name
x' = (pos
n, name -> Maybe name
forall a. a -> Maybe a
Just name
x) (pos, Maybe name) -> [(pos, Maybe name)] -> [(pos, Maybe name)]
forall a. a -> [a] -> [a]
: [(pos, Maybe name)] -> [Maybe name] -> [(pos, Maybe name)]
forall name pos.
Eq name =>
[(pos, Maybe name)] -> [Maybe name] -> [(pos, Maybe name)]
update [(pos, Maybe name)]
as [Maybe name]
args
    update ((pos
n, Maybe name
_) : [(pos, Maybe name)]
as) (Maybe name
_ : [Maybe name]
args) = (pos
n, Maybe name
forall a. Maybe a
Nothing) (pos, Maybe name) -> [(pos, Maybe name)] -> [(pos, Maybe name)]
forall a. a -> [a] -> [a]
: [(pos, Maybe name)] -> [Maybe name] -> [(pos, Maybe name)]
forall name pos.
Eq name =>
[(pos, Maybe name)] -> [Maybe name] -> [(pos, Maybe name)]
update [(pos, Maybe name)]
as [Maybe name]
args

    getDataApp :: ConstructorInfo -> [[Maybe Name]]
    getDataApp :: ConstructorInfo -> [[Maybe Name]]
getDataApp (ConstructorInfo { constructorFields :: ConstructorInfo -> [Type]
constructorFields  = [Type]
fields }) =
      (Type -> [[Maybe Name]]) -> [Type] -> [[Maybe Name]]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Type -> [[Maybe Name]]
getThem ([Type] -> [[Maybe Name]]) -> [Type] -> [[Maybe Name]]
forall a b. (a -> b) -> a -> b
$
      [Type]
fields [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [ Type -> [TypeArg] -> Type
applyType (Name -> Type
ConT Name
dataName) ([TypeArg] -> Type) -> [TypeArg] -> Type
forall a b. (a -> b) -> a -> b
$ (Type -> TypeArg) -> [Type] -> [TypeArg]
forall a b. (a -> b) -> [a] -> [b]
map Type -> TypeArg
TANormal
                                            ([Type] -> [TypeArg]) -> [Type] -> [TypeArg]
forall a b. (a -> b) -> a -> b
$ (Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Type
unSigType [Type]
instTys
                ]
      where
        getThem :: Type -> [[Maybe Name]]
        getThem :: Type -> [[Maybe Name]]
getThem Type
ty = Maybe [Maybe Name] -> [[Maybe Name]]
forall a. Maybe a -> [a]
maybeToList (Maybe [Maybe Name] -> [[Maybe Name]])
-> Maybe [Maybe Name] -> [[Maybe Name]]
forall a b. (a -> b) -> a -> b
$ Name -> Type -> ([TypeArg] -> [Maybe Name]) -> Maybe [Maybe Name]
forall a. Name -> Type -> ([TypeArg] -> a) -> Maybe a
mbInductiveCase Name
dataName Type
ty [TypeArg] -> [Maybe Name]
inductiveArg

        inductiveArg :: [TypeArg] -> [Maybe Name]
        inductiveArg :: [TypeArg] -> [Maybe Name]
inductiveArg [TypeArg]
argTys =
          let visArgTys :: [Type]
visArgTys = [TypeArg] -> [Type]
filterTANormals [TypeArg]
argTys
          in [Type] -> [Type] -> [Maybe Name]
mParam [Type]
visArgTys [Type]
visArgTys

    -- keep the arguments which are single names, which appear
    -- in the return type, counting only the first time they appear in
    -- the return type as the parameter position
    mParam :: [Type] -> [Type] -> [Maybe Name]
    mParam :: [Type] -> [Type] -> [Maybe Name]
mParam [Type]
_    [] = []
    mParam [Type]
args (VarT Name
n:[Type]
rest)
      | Bool -> Name -> [Type] -> Bool
paramIn Bool
False Name
n [Type]
args
      = Name -> Maybe Name
forall a. a -> Maybe a
Just Name
n Maybe Name -> [Maybe Name] -> [Maybe Name]
forall a. a -> [a] -> [a]
: [Type] -> [Type] -> [Maybe Name]
mParam ((Type -> Bool) -> [Type] -> [Type]
forall a. (a -> Bool) -> [a] -> [a]
filter (Name -> Type -> Bool
noN Name
n) [Type]
args) [Type]
rest
    mParam [Type]
args (Type
_:[Type]
rest) = Maybe Name
forall a. Maybe a
Nothing Maybe Name -> [Maybe Name] -> [Maybe Name]
forall a. a -> [a] -> [a]
: [Type] -> [Type] -> [Maybe Name]
mParam [Type]
args [Type]
rest

    paramIn :: Bool -> Name -> [Type] -> Bool
    paramIn :: Bool -> Name -> [Type] -> Bool
paramIn Bool
ok Name
_ []          = Bool
ok
    paramIn Bool
ok Name
n (VarT Name
t:[Type]
ts) = Bool -> Name -> [Type] -> Bool
paramIn (Bool
ok Bool -> Bool -> Bool
|| Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
t) Name
n [Type]
ts
    paramIn Bool
ok Name
n (Type
t:[Type]
ts)
      | Name
n Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Type -> [Name]
forall a. TypeSubstitution a => a -> [Name]
freeVariables Type
t = Bool
False -- not a single name
      | Bool
otherwise                = Bool -> Name -> [Type] -> Bool
paramIn Bool
ok Name
n [Type]
ts

    -- If the name appears again later, don't count that appearance
    -- as a parameter position
    noN :: Name -> Type -> Bool
    noN :: Name -> Type -> Bool
noN Name
n (VarT Name
t) = Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/= Name
t
    noN Name
_ Type
_        = Bool
False

-----
-- Taken directly from th-desugar
-----

-- | Remove all of the explicit kind signatures from a 'Type'.
unSigType :: Type -> Type
unSigType :: Type -> Type
unSigType (SigT Type
t Type
_)            = Type
t
unSigType (AppT Type
f Type
x)            = Type -> Type -> Type
AppT (Type -> Type
unSigType Type
f) (Type -> Type
unSigType Type
x)
unSigType (ForallT [TyVarBndr Specificity]
tvbs [Type]
ctxt Type
t) = [TyVarBndr Specificity] -> [Type] -> Type -> Type
ForallT [TyVarBndr Specificity]
tvbs ((Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Type
unSigType [Type]
ctxt) (Type -> Type
unSigType Type
t)
unSigType (InfixT Type
t1 Name
n Type
t2)      = Type -> Name -> Type -> Type
InfixT (Type -> Type
unSigType Type
t1) Name
n (Type -> Type
unSigType Type
t2)
unSigType (UInfixT Type
t1 Name
n Type
t2)     = Type -> Name -> Type -> Type
UInfixT (Type -> Type
unSigType Type
t1) Name
n (Type -> Type
unSigType Type
t2)
unSigType (ParensT Type
t)           = Type -> Type
ParensT (Type -> Type
unSigType Type
t)
unSigType (AppKindT Type
t Type
k)        = Type -> Type -> Type
AppKindT (Type -> Type
unSigType Type
t) (Type -> Type
unSigType Type
k)
unSigType (ImplicitParamT String
n Type
t)  = String -> Type -> Type
ImplicitParamT String
n (Type -> Type
unSigType Type
t)
unSigType Type
t                     = Type
t

-----
-- Taken directly from singletons
-----

-- Make an identifier uppercase. If the identifier is infix, this acts as the
-- identity function.
upcase :: String -> String
upcase :: String -> String
upcase String
str
  | Char -> Bool
isHsLetter Char
first
  = Char -> Char
toUpper Char
first Char -> String -> String
forall a. a -> [a] -> [a]
: String -> String
forall a. HasCallStack => [a] -> [a]
tail String
str

  | Bool
otherwise
  = String
str
  where
    first :: Char
first = String -> Char
forall a. HasCallStack => [a] -> a
head String
str

-- 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
'_'