{-# LANGUAGE CPP #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE LambdaCase #-}
{-# OPTIONS_GHC -Wno-x-partial -Wno-incomplete-uni-patterns -Wno-unused-imports #-}
-- | @Traversable (Stock1 F)@, synthesized directly (DeriveTraversable-style
-- Core), NOT by coercion.  @traverse@'s result @f (t b)@ places the wrapper
-- under an /abstract/ applicative @f@ (nominal role), so DerivingVia cannot
-- coerce @Traversable (Stock1 F)@ onto @F@ — but the instance itself is
-- perfectly definable and usable at the wrapper.  Put it on your own type with
-- the one-liner (which works with @Override1@ too):
--
-- > instance Traversable F where
-- >   traverse g = fmap unStock1 . traverse g . Stock1
module Stock.Traversable (synthTraversable) where

import GHC.Plugins hiding (TcPlugin)
import GHC.Tc.Plugin
import GHC.Tc.Types.Constraint
#if MIN_VERSION_ghc(9,12,0)
import GHC.Tc.Types.CtLoc (CtLoc)
#else
import GHC.Tc.Types.Constraint (CtLoc)
#endif
import GHC.Tc.Types.Evidence
import GHC.Core.Class (Class)
import GHC.Core.Predicate (mkClassPred)
import GHC.Core.Multiplicity (scaledThing)
import GHC.Core.TyCo.Compare (eqType)
import GHC.Core.TyCo.Subst (substTyWith)
import GHC.Core.TyCo.Rep (UnivCoProvenance(PluginProv))
import GHC.Builtin.Names (applicativeClassName, functorClassName, foldableClassName)
import Control.Monad (forM, zipWithM)
import Data.List (zipWith4)
import Stock.Derive (classMethod)
import Stock.Internal
import Stock.Functor (synthFunctor, synthFoldable)

-- | Synthesize @Traversable (Stock1 F)@: per constructor, @pure mkCon \<*\> f1
-- \<*\> … \<*\> fn@ where the parameter field uses the supplied @g@, a constant
-- uses @pure@, and a sub-functor @H a@ field uses @traverse \@H g@ (an
-- @Override1@-reshaped functor traverses through the modifier, re-wrapped with
-- @pure coerce \<*\> _@ — never a cast under the abstract @f@).  @Functor@ and
-- @Foldable@ superclasses come from their own synthesizers.
synthTraversable :: GenEnv -> Class -> CtLoc -> Type -> Type
                 -> TcPluginM (Maybe (EvTerm, [Ct]))
synthTraversable :: GenEnv
-> Class
-> CtLoc
-> Type
-> Type
-> TcPluginM (Maybe (EvTerm, [Ct]))
synthTraversable GenEnv
gen Class
travCls CtLoc
loc Type
wrappedTy Type
f =
  case GenEnv -> Maybe TyCon
geStock1 GenEnv
gen of
    Just TyCon
st1Tc
      | let (Type
realF, Maybe [Type]
mMods) = GenEnv -> Type -> (Type, Maybe [Type])
peelOverride1 GenEnv
gen Type
f
      , Just TyCon
fTc <- Type -> Maybe TyCon
tyConAppTyCon_maybe Type
realF -> do
      appCls  <- Name -> TcPluginM Class
tcLookupClass Name
applicativeClassName
      funcCls <- tcLookupClass functorClassName
      foldCls <- tcLookupClass foldableClassName
      let fixed = HasCallStack => Type -> [Type]
Type -> [Type]
tyConAppArgs Type
realF
          dcons = TyCon -> [DataCon]
tyConDataCons TyCon
fTc
          traverseSel = String -> Class -> Id
classMethod String
"traverse" Class
travCls
          pureSel     = String -> Class -> Id
classMethod String
"pure" Class
appCls
          apSel       = String -> Class -> Id
classMethod String
"<*>"  Class
appCls
          coAt Type
t      = GenEnv -> TyCon -> Type -> Type -> Type -> Type -> Coercion
coDown1 GenEnv
gen TyCon
st1Tc Type
wrappedTy Type
f Type
realF Type
t   -- Stock1 (Override1? F) t ~R F t
      fTv <- freshTyVarK (mkVisFunTyMany liftedTypeKind liftedTypeKind) "f"  -- f :: Type -> Type
      aTv <- freshTyVar "a" ; bTv <- freshTyVar "b"
      let fTy = Id -> Type
mkTyVarTy Id
fTv ; aTy = Id -> Type
mkTyVarTy Id
aTv ; bTy = Id -> Type
mkTyVarTy Id
bTv
          fOf Type
t  = Type -> Type -> Type
mkAppTy Type
fTy Type
t
          innerA = TyCon -> [Type] -> Type
mkTyConApp TyCon
fTc ([Type]
fixed [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type
aTy])
          gTy    = HasDebugCallStack => Type -> Type -> Type
Type -> Type -> Type
mkVisFunTyMany Type
aTy (Type -> Type
fOf Type
bTy)              -- a -> f b
          stbTy  = Type -> Type -> Type
mkAppTy Type
wrappedTy Type
bTy                     -- Stock1 F b
      dApp <- freshId (mkClassPred appCls [fTy]) "dApp"
      gId  <- freshId gTy "g"
      xId  <- freshId (mkAppTy wrappedTy aTy) "x"
      cb   <- freshId innerA "cb"
      let pureE Type
ty Arg b
e        = Arg b -> [Arg b] -> Arg b
forall b. Expr b -> [Expr b] -> Expr b
mkApps (Id -> Arg b
forall b. Id -> Expr b
Var Id
pureSel) [Type -> Arg b
forall b. Type -> Expr b
Type Type
fTy, Id -> Arg b
forall b. Id -> Expr b
Var Id
dApp, Type -> Arg b
forall b. Type -> Expr b
Type Type
ty, Arg b
e]
          apE Type
tyA Type
tyB Arg b
ac Arg b
fe = Arg b -> [Arg b] -> Arg b
forall b. Expr b -> [Expr b] -> Expr b
mkApps (Id -> Arg b
forall b. Id -> Expr b
Var Id
apSel)   [Type -> Arg b
forall b. Type -> Expr b
Type Type
fTy, Id -> Arg b
forall b. Id -> Expr b
Var Id
dApp, Type -> Arg b
forall b. Type -> Expr b
Type Type
tyA, Type -> Arg b
forall b. Type -> Expr b
Type Type
tyB, Arg b
ac, Arg b
fe]
          subB Type
t = [Id] -> [Type] -> Type -> Type
HasDebugCallStack => [Id] -> [Type] -> Type -> Type
substTyWith [Id
aTv] [Type
bTy] Type
t                  -- t[a := b]
          -- GHC's @ft_*@ traversal of a field: a constant ⇒ @pure x@; the
          -- parameter ⇒ @g x@; a tuple ⇒ @pure (,..) \<*\> t1 \<*\> …@ (every
          -- component); a covariant @H larg@ ⇒ @traverse \@H@ (nested @[[a]]@ ⇒
          -- @traverse (traverse g)@); a function field rejected.  Result is
          -- @f (subB ft)@.
          traverseField Type
ft Expr Id
xe
            | Bool -> Bool
not (Id
aTv Id -> VarSet -> Bool
`elemVarSet` Type -> VarSet
tyCoVarsOfType Type
ft) = Maybe (Expr Id, [Ct]) -> TcPluginM (Maybe (Expr Id, [Ct]))
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Expr Id, [Ct]) -> Maybe (Expr Id, [Ct])
forall a. a -> Maybe a
Just (Type -> Expr Id -> Expr Id
forall {b}. Type -> Arg b -> Arg b
pureE Type
ft Expr Id
xe, []))
            | Type
ft Type -> Type -> Bool
`eqType` Type
aTy                          = Maybe (Expr Id, [Ct]) -> TcPluginM (Maybe (Expr Id, [Ct]))
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Expr Id, [Ct]) -> Maybe (Expr Id, [Ct])
forall a. a -> Maybe a
Just (Expr Id -> Expr Id -> Expr Id
forall b. Expr b -> Expr b -> Expr b
App (Id -> Expr Id
forall b. Id -> Expr b
Var Id
gId) Expr Id
xe, []))
            | Just (FunTyFlag, Type, Type, Type)
_ <- Type -> Maybe (FunTyFlag, Type, Type, Type)
splitFunTy_maybe Type
ft            = Maybe (Expr Id, [Ct]) -> TcPluginM (Maybe (Expr Id, [Ct]))
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Expr Id, [Ct])
forall a. Maybe a
Nothing
            | Just (TyCon
tc, [Type]
args) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ft
            , TyCon -> Bool
isTupleTyCon TyCon
tc, [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
args Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
2 = do
                xs <- (Type -> TcPluginM Id) -> [Type] -> TcPluginM [Id]
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) -> [a] -> m [b]
mapM (Type -> String -> TcPluginM Id
`freshId` String
"u") [Type]
args
                rs <- zipWithM traverseField args (map Var xs)
                case sequence rs of
                  Maybe [(Expr Id, [Ct])]
Nothing    -> Maybe (Expr Id, [Ct]) -> TcPluginM (Maybe (Expr Id, [Ct]))
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Expr Id, [Ct])
forall a. Maybe a
Nothing
                  Just [(Expr Id, [Ct])]
travs -> do
                    let subArgs :: [Type]
subArgs = (Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Type
subB [Type]
args
                        dc :: DataCon
dc      = Boxity -> Int -> DataCon
tupleDataCon Boxity
Boxed ([Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
args)
                        subTup :: Type
subTup  = Type -> Type
subB Type
ft
                        rs' :: [Type]
rs'     = (Type -> Type -> Type) -> Type -> [Type] -> [Type]
forall a b. (a -> b -> b) -> b -> [a] -> [b]
scanr HasDebugCallStack => Type -> Type -> Type
Type -> Type -> Type
mkVisFunTyMany Type
subTup [Type]
subArgs
                    ys <- (Type -> TcPluginM Id) -> [Type] -> TcPluginM [Id]
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) -> [a] -> m [b]
mapM (Type -> String -> TcPluginM Id
`freshId` String
"v") [Type]
subArgs
                    cb <- freshId ft "cb"
                    let mkTup = [Id] -> Expr Id -> Expr Id
forall b. [b] -> Expr b -> Expr b
mkLams [Id]
ys (DataCon -> [Expr Id] -> Expr Id
mkCoreConApps DataCon
dc ((Type -> Expr Id) -> [Type] -> [Expr Id]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Expr Id
forall b. Type -> Expr b
Type [Type]
subArgs [Expr Id] -> [Expr Id] -> [Expr Id]
forall a. [a] -> [a] -> [a]
++ (Id -> Expr Id) -> [Id] -> [Expr Id]
forall a b. (a -> b) -> [a] -> [b]
map Id -> Expr Id
forall b. Id -> Expr b
Var [Id]
ys))
                        built = (Expr Id -> (Int, Expr Id, Type) -> Expr Id)
-> Expr Id -> [(Int, Expr Id, Type)] -> Expr Id
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\Expr Id
ac (Int
k, Expr Id
te, Type
sa) -> Type -> Type -> Expr Id -> Expr Id -> Expr Id
forall {b}. Type -> Type -> Arg b -> Arg b -> Arg b
apE Type
sa ([Type]
rs' [Type] -> Int -> Type
forall a. HasCallStack => [a] -> Int -> a
!! (Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)) Expr Id
ac Expr Id
te)
                                      (Type -> Expr Id -> Expr Id
forall {b}. Type -> Arg b -> Arg b
pureE ([Type] -> Type
forall a. HasCallStack => [a] -> a
head [Type]
rs') Expr Id
mkTup)
                                      ([Int] -> [Expr Id] -> [Type] -> [(Int, Expr Id, Type)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [Int
0 :: Int ..] (((Expr Id, [Ct]) -> Expr Id) -> [(Expr Id, [Ct])] -> [Expr Id]
forall a b. (a -> b) -> [a] -> [b]
map (Expr Id, [Ct]) -> Expr Id
forall a b. (a, b) -> a
fst [(Expr Id, [Ct])]
travs) [Type]
subArgs)
                    pure (Just ( Case xe cb (fOf subTup) [Alt (DataAlt dc) xs built]
                               , concatMap snd travs ))
            | Just (Type
h, Type
larg) <- Type -> Maybe (Type, Type)
splitAppTy_maybe Type
ft
            , Bool -> Bool
not (Id
aTv Id -> VarSet -> Bool
`elemVarSet` Type -> VarSet
tyCoVarsOfType Type
h) =
                if Type
larg Type -> Type -> Bool
`eqType` Type
aTy
                  then do ev <- CtLoc -> Type -> TcPluginM CtEvidence
newWanted CtLoc
loc (Class -> [Type] -> Type
mkClassPred Class
travCls [Type
h])
                          pure (Just ( mkApps (Var traverseSel)
                                 [Type h, ctEvExpr ev, Type fTy, Type aTy, Type bTy, Var dApp, Var gId, xe]
                                 , [mkNonCanonical ev] ))
                  else do y     <- Type -> String -> TcPluginM Id
freshId Type
larg String
"y"
                          inner <- traverseField larg (Var y)
                          case inner of
                            Maybe (Expr Id, [Ct])
Nothing     -> Maybe (Expr Id, [Ct]) -> TcPluginM (Maybe (Expr Id, [Ct]))
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Expr Id, [Ct])
forall a. Maybe a
Nothing
                            Just (Expr Id
e, [Ct]
w) -> do
                              ev <- CtLoc -> Type -> TcPluginM CtEvidence
newWanted CtLoc
loc (Class -> [Type] -> Type
mkClassPred Class
travCls [Type
h])
                              pure (Just ( mkApps (Var traverseSel)
                                     [Type h, ctEvExpr ev, Type fTy, Type larg, Type (subB larg)
                                     , Var dApp, Lam y e, xe]
                                     , mkNonCanonical ev : w ))
            | Bool
otherwise = Maybe (Expr Id, [Ct]) -> TcPluginM (Maybe (Expr Id, [Ct]))
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Expr Id, [Ct])
forall a. Maybe a
Nothing
          -- one field's effect @f rvFt@; Override1 reshapes the (one-level)
          -- functor @h a -> m a@, otherwise the full structural walk.
          fieldOf Int
i Id
x Type
ftA Type
rvFt = case GenEnv -> Maybe [Type] -> Int -> Maybe Type
override1Mod GenEnv
gen Maybe [Type]
mMods Int
i of
            Just Type
m -> do        -- Override1: traverse through @m@, re-wrap @m b -> h b@
              ev <- CtLoc -> Type -> TcPluginM CtEvidence
newWanted CtLoc
loc (Class -> [Type] -> Type
mkClassPred Class
travCls [Type
m])
              -- validate at the closed type @()@ (see Stock.Functor) so the
              -- evidence stays free of the method-local @aTv@.
              vw <- newWanted loc (mkStockReprEq (substTyWith [aTv] [unitTy] ftA)
                                                 (mkAppTy m unitTy))
              let coS  = UnivCoProvenance -> Role -> Type -> Type -> Coercion
mkStockCo (String -> UnivCoProvenance
PluginProv String
"stock") Role
Representational Type
ftA (Type -> Type -> Type
mkAppTy Type
m Type
aTy)
                  coRb = UnivCoProvenance -> Role -> Type -> Type -> Coercion
mkStockCo (String -> UnivCoProvenance
PluginProv String
"stock") Role
Representational (Type -> Type -> Type
mkAppTy Type
m Type
bTy) Type
rvFt
                  trav = Expr Id -> [Expr Id] -> Expr Id
forall b. Expr b -> [Expr b] -> Expr b
mkApps (Id -> Expr Id
forall b. Id -> Expr b
Var Id
traverseSel)
                           [Type -> Expr Id
forall b. Type -> Expr b
Type Type
m, HasDebugCallStack => CtEvidence -> Expr Id
CtEvidence -> Expr Id
ctEvExpr CtEvidence
ev, Type -> Expr Id
forall b. Type -> Expr b
Type Type
fTy, Type -> Expr Id
forall b. Type -> Expr b
Type Type
aTy, Type -> Expr Id
forall b. Type -> Expr b
Type Type
bTy
                           , Id -> Expr Id
forall b. Id -> Expr b
Var Id
dApp, Id -> Expr Id
forall b. Id -> Expr b
Var Id
gId, Expr Id -> Coercion -> Expr Id
forall b. Expr b -> Coercion -> Expr b
Cast (Id -> Expr Id
forall b. Id -> Expr b
Var Id
x) Coercion
coS]          -- :: f (m b)
              mb <- freshId (mkAppTy m bTy) "mb"
              let coerceFn = Id -> Expr Id -> Expr Id
forall b. b -> Expr b -> Expr b
Lam Id
mb (Expr Id -> Coercion -> Expr Id
forall b. Expr b -> Coercion -> Expr b
Cast (Id -> Expr Id
forall b. Id -> Expr b
Var Id
mb) Coercion
coRb)                   -- m b -> h b
              pure (Just ( apE (mkAppTy m bTy) rvFt
                             (pureE (mkVisFunTyMany (mkAppTy m bTy) rvFt) coerceFn) trav
                         , [mkNonCanonical ev, mkNonCanonical vw] ))
            Maybe Type
Nothing -> Type -> Expr Id -> TcPluginM (Maybe (Expr Id, [Ct]))
traverseField Type
ftA (Id -> Expr Id
forall b. Id -> Expr b
Var Id
x)
      malts <- forM dcons \DataCon
dc -> do
        let fts :: [Type]
fts   = (Scaled Type -> Type) -> [Scaled Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Scaled Type -> Type
forall a. Scaled a -> a
scaledThing (DataCon -> [Type] -> [Scaled Type]
dataConInstOrigArgTys DataCon
dc ([Type]
fixed [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type
aTy]))
            rvFts :: [Type]
rvFts = (Scaled Type -> Type) -> [Scaled Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Scaled Type -> Type
forall a. Scaled a -> a
scaledThing (DataCon -> [Type] -> [Scaled Type]
dataConInstOrigArgTys DataCon
dc ([Type]
fixed [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type
bTy]))
        xs   <- (Int -> Type -> TcPluginM Id) -> [Int] -> [Type] -> TcPluginM [Id]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (\Int
n Type
ft -> Type -> String -> TcPluginM Id
freshId Type
ft (String
"x" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n)) [Int
0 :: Int ..] [Type]
fts
        mfes <- sequence (zipWith4 fieldOf [0 :: Int ..] xs fts rvFts)
        case sequence mfes of
          Maybe [(Expr Id, [Ct])]
Nothing  -> Maybe (Alt Id, [Ct]) -> TcPluginM (Maybe (Alt Id, [Ct]))
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Alt Id, [Ct])
forall a. Maybe a
Nothing
          Just [(Expr Id, [Ct])]
fes -> do
            let ([Expr Id]
fieldExprs, [[Ct]]
wss) = [(Expr Id, [Ct])] -> ([Expr Id], [[Ct]])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Expr Id, [Ct])]
fes
            ys <- (Int -> Type -> TcPluginM Id) -> [Int] -> [Type] -> TcPluginM [Id]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (\Int
n Type
ft -> Type -> String -> TcPluginM Id
freshId Type
ft (String
"y" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n)) [Int
0 :: Int ..] [Type]
rvFts
            let mkCon = [Id] -> Expr Id -> Expr Id
forall b. [b] -> Expr b -> Expr b
mkLams [Id]
ys (Expr Id -> Coercion -> Expr Id
forall b. Expr b -> Coercion -> Expr b
Cast (DataCon -> [Expr Id] -> Expr Id
mkCoreConApps DataCon
dc ((Type -> Expr Id) -> [Type] -> [Expr Id]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Expr Id
forall b. Type -> Expr b
Type ([Type]
fixed [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type
bTy]) [Expr Id] -> [Expr Id] -> [Expr Id]
forall a. [a] -> [a] -> [a]
++ (Id -> Expr Id) -> [Id] -> [Expr Id]
forall a b. (a -> b) -> [a] -> [b]
map Id -> Expr Id
forall b. Id -> Expr b
Var [Id]
ys))
                                        (Coercion -> Coercion
mkSymCo (Type -> Coercion
coAt Type
bTy)))                -- rvFt.. -> Stock1 F b
                rs    = (Type -> Type -> Type) -> Type -> [Type] -> [Type]
forall a b. (a -> b -> b) -> b -> [a] -> [b]
scanr HasDebugCallStack => Type -> Type -> Type
Type -> Type -> Type
mkVisFunTyMany Type
stbTy [Type]
rvFts                     -- R_0 … R_n(=Stock1 F b)
                body  = (Expr Id -> (Int, Expr Id, Type) -> Expr Id)
-> Expr Id -> [(Int, Expr Id, Type)] -> Expr Id
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\Expr Id
ac (Int
k, Expr Id
fe, Type
rvFt) -> Type -> Type -> Expr Id -> Expr Id -> Expr Id
forall {b}. Type -> Type -> Arg b -> Arg b -> Arg b
apE Type
rvFt ([Type]
rs [Type] -> Int -> Type
forall a. HasCallStack => [a] -> Int -> a
!! (Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)) Expr Id
ac Expr Id
fe)
                              (Type -> Expr Id -> Expr Id
forall {b}. Type -> Arg b -> Arg b
pureE ([Type] -> Type
forall a. HasCallStack => [a] -> a
head [Type]
rs) Expr Id
mkCon)
                              ([Int] -> [Expr Id] -> [Type] -> [(Int, Expr Id, Type)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [Int
0 :: Int ..] [Expr Id]
fieldExprs [Type]
rvFts)
            pure (Just (Alt (DataAlt dc) xs body, concat wss))
      case sequence malts of
        Maybe [(Alt Id, [Ct])]
Nothing     -> Maybe (EvTerm, [Ct]) -> TcPluginM (Maybe (EvTerm, [Ct]))
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (EvTerm, [Ct])
forall a. Maybe a
Nothing
        Just [(Alt Id, [Ct])]
altWss -> do
          let ([Alt Id]
alts, [[Ct]]
wss) = [(Alt Id, [Ct])] -> ([Alt Id], [[Ct]])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Alt Id, [Ct])]
altWss
              traverseImpl :: Expr Id
traverseImpl = [Id] -> Expr Id -> Expr Id
forall b. [b] -> Expr b -> Expr b
mkLams [Id
fTv, Id
aTv, Id
bTv, Id
dApp, Id
gId, Id
xId]
                (TyCon -> [Type] -> Expr Id -> Id -> Type -> [Alt Id] -> Expr Id
destructInner TyCon
fTc ([Type]
fixed [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type
aTy]) (Expr Id -> Coercion -> Expr Id
forall b. Expr b -> Coercion -> Expr b
Cast (Id -> Expr Id
forall b. Id -> Expr b
Var Id
xId) (Type -> Coercion
coAt Type
aTy)) Id
cb (Type -> Type
fOf Type
stbTy) [Alt Id]
alts)
          mFunc <- GenEnv
-> Class
-> CtLoc
-> Type
-> Type
-> TcPluginM (Maybe (EvTerm, [Ct]))
synthFunctor  GenEnv
gen Class
funcCls CtLoc
loc Type
wrappedTy Type
f
          mFold <- synthFoldable gen foldCls loc wrappedTy f
          case (mFunc, mFold) of
            (Just (EvTerm
fEv, [Ct]
fWs), Just (EvTerm
foEv, [Ct]
foWs)) -> do
              dict <- Class
-> Type -> [Expr Id] -> [(Int, Expr Id)] -> TcPluginM (Expr Id)
recDictWith Class
travCls Type
wrappedTy [EvTerm -> Expr Id
unwrapEv EvTerm
fEv, EvTerm -> Expr Id
unwrapEv EvTerm
foEv] [(Int
0, Expr Id
traverseImpl)]
              pure (Just (EvExpr dict, fWs ++ foWs ++ concat wss))
            (Maybe (EvTerm, [Ct]), Maybe (EvTerm, [Ct]))
_ -> Maybe (EvTerm, [Ct]) -> TcPluginM (Maybe (EvTerm, [Ct]))
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (EvTerm, [Ct])
forall a. Maybe a
Nothing
    Maybe TyCon
_ -> Maybe (EvTerm, [Ct]) -> TcPluginM (Maybe (EvTerm, [Ct]))
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (EvTerm, [Ct])
forall a. Maybe a
Nothing