    {- Data/Singletons/Promote/Eq.hs

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

    This module defines the functions that generate type-level equality type
    family instances.
    -}

    module Data.Singletons.Promote.Eq where

    import Language.Haskell.TH.Syntax
    import Language.Haskell.TH.Desugar
    import Data.Singletons.Names
    import Data.Singletons.Util
    import Control.Monad

    -- produce a closed type family helper and the instance
    -- for (==) over the given list of ctors
    mkEqTypeInstance :: Quasi q => DKind -> [DCon] -> q [DDec]
    mkEqTypeInstance :: DKind -> [DCon] -> q [DDec]
    mkEqTypeInstance kind :: DKind
    kind cons :: [DCon]
    cons = do
      Name
    helperName <- String -> q Name
    forall (q :: * -> *). Quasi q => String -> q Name
    newUniqueName "Equals"
      Name
    aName <- String -> q Name
    forall (q :: * -> *). Quasi q => String -> q Name
    qNewName "a"
      Name
    bName <- String -> q Name
    forall (q :: * -> *). Quasi q => String -> q Name
    qNewName "b"
      [DTySynEqn]
    true_branches <- (DCon -> q DTySynEqn) -> [DCon] -> q [DTySynEqn]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (Name -> DCon -> q DTySynEqn
    forall (q :: * -> *). Quasi q => Name -> DCon -> q DTySynEqn
    mk_branch Name
    helperName) [DCon]
    cons
      let null_branch :: DTySynEqn
    null_branch  = Name -> Name -> DTySynEqn
    catch_all_case Name
    helperName Name
    trueName
          false_branch :: DTySynEqn
    false_branch = Name -> Name -> DTySynEqn
    catch_all_case Name
    helperName Name
    falseName
          branches :: [DTySynEqn]
    branches | [DCon] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [DCon]
    cons = [DTySynEqn
    null_branch]
                   | Bool
    otherwise = [DTySynEqn]
    true_branches [DTySynEqn] -> [DTySynEqn] -> [DTySynEqn]
    forall a. [a] -> [a] -> [a]
    ++ [DTySynEqn
    false_branch]
          closedFam :: DDec
    closedFam = DTypeFamilyHead -> [DTySynEqn] -> DDec
    DClosedTypeFamilyD (Name
    -> [DTyVarBndr]
    -> DFamilyResultSig
    -> Maybe InjectivityAnn
    -> DTypeFamilyHead
    DTypeFamilyHead Name
    helperName
                                                            -- We opt to give explicit kinds for the tyvars
                                                            -- in the helper type family.
                                                            -- See Note [Promoted class method kinds]
                                                            -- in Data.Singletons.Promote.
                                                          [ Name -> DKind -> DTyVarBndr
    DKindedTV Name
    aName DKind
    kind
                                                          , Name -> DKind -> DTyVarBndr
    DKindedTV Name
    bName DKind
    kind ]
                                                          (DKind -> DFamilyResultSig
    DKindSig DKind
    boolKi)
                                                          Maybe InjectivityAnn
    forall a. Maybe a
    Nothing)
                                         [DTySynEqn]
    branches
          eqInst :: DDec
    eqInst = DTySynEqn -> DDec
    DTySynInstD (DTySynEqn -> DDec) -> DTySynEqn -> DDec
    forall a b. (a -> b) -> a -> b
    $
                   Maybe [DTyVarBndr] -> DKind -> DKind -> DTySynEqn
    DTySynEqn Maybe [DTyVarBndr]
    forall a. Maybe a
    Nothing
                             (Name -> DKind
    DConT Name
    tyEqName DKind -> DKind -> DKind
    `DAppT` Name -> DKind
    DVarT Name
    aName DKind -> DKind -> DKind
    `DAppT` Name -> DKind
    DVarT Name
    bName)
                             (DKind -> [DKind] -> DKind
    foldType (Name -> DKind
    DConT Name
    helperName) [Name -> DKind
    DVarT Name
    aName, Name -> DKind
    DVarT Name
    bName])
          inst :: DDec
    inst = Maybe Overlap
    -> Maybe [DTyVarBndr] -> [DKind] -> DKind -> [DDec] -> DDec
    DInstanceD Maybe Overlap
    forall a. Maybe a
    Nothing Maybe [DTyVarBndr]
    forall a. Maybe a
    Nothing [] ((Name -> DKind
    DConT (Name -> DKind) -> Name -> DKind
    forall a b. (a -> b) -> a -> b
    $ Name -> Name
    promoteClassName Name
    eqName) DKind -> DKind -> DKind
    `DAppT`
                                                DKind
    kind) [DDec
    eqInst]

      [DDec] -> q [DDec]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [DDec
    closedFam, DDec
    inst]

      where mk_branch :: Quasi q => Name -> DCon -> q DTySynEqn
            mk_branch :: Name -> DCon -> q DTySynEqn
    mk_branch helper_name :: Name
    helper_name con :: DCon
    con = do
              let (name :: Name
    name, numArgs :: Int
    numArgs) = DCon -> (Name, Int)
    extractNameArgs DCon
    con
              [Name]
    lnames <- Int -> q Name -> q [Name]
    forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
    replicateM Int
    numArgs (String -> q Name
    forall (q :: * -> *). Quasi q => String -> q Name
    qNewName "a")
              [Name]
    rnames <- Int -> q Name -> q [Name]
    forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
    replicateM Int
    numArgs (String -> q Name
    forall (q :: * -> *). Quasi q => String -> q Name
    qNewName "b")
              let lvars :: [DKind]
    lvars = (Name -> DKind) -> [Name] -> [DKind]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> DKind
    DVarT [Name]
    lnames
                  rvars :: [DKind]
    rvars = (Name -> DKind) -> [Name] -> [DKind]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> DKind
    DVarT [Name]
    rnames
                  ltype :: DKind
    ltype = DKind -> [DKind] -> DKind
    foldType (Name -> DKind
    DConT Name
    name) [DKind]
    lvars
                  rtype :: DKind
    rtype = DKind -> [DKind] -> DKind
    foldType (Name -> DKind
    DConT Name
    name) [DKind]
    rvars
                  results :: [DKind]
    results = (DKind -> DKind -> DKind) -> [DKind] -> [DKind] -> [DKind]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (\l :: DKind
    l r :: DKind
    r -> DKind -> [DKind] -> DKind
    foldType (Name -> DKind
    DConT Name
    tyEqName) [DKind
    l, DKind
    r]) [DKind]
    lvars [DKind]
    rvars
                  result :: DKind
    result = [DKind] -> DKind
    tyAll [DKind]
    results
              DTySynEqn -> q DTySynEqn
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DTySynEqn -> q DTySynEqn) -> DTySynEqn -> q DTySynEqn
    forall a b. (a -> b) -> a -> b
    $ Maybe [DTyVarBndr] -> DKind -> DKind -> DTySynEqn
    DTySynEqn Maybe [DTyVarBndr]
    forall a. Maybe a
    Nothing
                                 (Name -> DKind
    DConT Name
    helper_name DKind -> DKind -> DKind
    `DAppT` DKind
    ltype DKind -> DKind -> DKind
    `DAppT` DKind
    rtype)
                                 DKind
    result

            catch_all_case :: Name -> Name -> DTySynEqn
            catch_all_case :: Name -> Name -> DTySynEqn
    catch_all_case helper_name :: Name
    helper_name returned_val_name :: Name
    returned_val_name =
              Maybe [DTyVarBndr] -> DKind -> DKind -> DTySynEqn
    DTySynEqn Maybe [DTyVarBndr]
    forall a. Maybe a
    Nothing
                        (Name -> DKind
    DConT Name
    helper_name
                           DKind -> DKind -> DKind
    `DAppT` DKind -> DKind -> DKind
    DSigT DKind
    DWildCardT DKind
    kind
                           DKind -> DKind -> DKind
    `DAppT` DKind -> DKind -> DKind
    DSigT DKind
    DWildCardT DKind
    kind)
                        (Name -> DKind
    promoteValRhs Name
    returned_val_name)

            tyAll :: [DType] -> DType -- "all" at the type level
            tyAll :: [DKind] -> DKind
    tyAll [] = (Name -> DKind
    promoteValRhs Name
    trueName)
            tyAll [one :: DKind
    one] = DKind
    one
            tyAll (h :: DKind
    h:t :: [DKind]
    t) = DKind -> [DKind] -> DKind
    foldType (Name -> DKind
    DConT (Name -> DKind) -> Name -> DKind
    forall a b. (a -> b) -> a -> b
    $ Name -> Name
    promoteValNameLhs Name
    andName) [DKind
    h, ([DKind] -> DKind
    tyAll [DKind]
    t)]
               -- I could use the Apply nonsense here, but there's no reason to