    {- 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 kind cons = do
      helperName <- newUniqueName "Equals"
      aName <- qNewName "a"
      bName <- qNewName "b"
      true_branches <- mapM mk_branch cons
      let null_branch  = catch_all_case trueName
          false_branch = catch_all_case falseName
          branches | null cons = [null_branch]
                   | otherwise = true_branches ++ [false_branch]
          closedFam = DClosedTypeFamilyD (DTypeFamilyHead 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.
                                                          [ DKindedTV aName kind
                                                          , DKindedTV bName kind ]
                                                          (DKindSig boolKi)
                                                          Nothing)
                                         branches
          eqInst = DTySynInstD tyEqName (DTySynEqn [DVarT aName, DVarT bName]
                                                 (foldType (DConT helperName)
                                                           [DVarT aName, DVarT bName]))
          inst = DInstanceD Nothing [] ((DConT $ promoteClassName eqName) `DAppT`
                                        kind) [eqInst]

      return [closedFam, inst]

      where mk_branch :: Quasi q => DCon -> q DTySynEqn
            mk_branch con = do
              let (name, numArgs) = extractNameArgs con
              lnames <- replicateM numArgs (qNewName "a")
              rnames <- replicateM numArgs (qNewName "b")
              let lvars = map DVarT lnames
                  rvars = map DVarT rnames
                  ltype = foldType (DConT name) lvars
                  rtype = foldType (DConT name) rvars
                  results = zipWith (\l r -> foldType (DConT tyEqName) [l, r]) lvars rvars
                  result = tyAll results
              return $ DTySynEqn [ltype, rtype] result

            catch_all_case :: Name -> DTySynEqn
            catch_all_case returned_val_name =
              DTySynEqn [DSigT DWildCardT kind, DSigT DWildCardT kind]
                        (promoteValRhs returned_val_name)

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