{-# 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
      Class
appCls  <- Name -> TcPluginM Class
tcLookupClass Name
applicativeClassName
      Class
funcCls <- Name -> TcPluginM Class
tcLookupClass Name
functorClassName
      Class
foldCls <- Name -> TcPluginM Class
tcLookupClass Name
foldableClassName
      let fixed :: [Type]
fixed = HasDebugCallStack => Type -> [Type]
Type -> [Type]
tyConAppArgs Type
realF
          dcons :: [DataCon]
dcons = TyCon -> [DataCon]
tyConDataCons TyCon
fTc
          traverseSel :: Id
traverseSel = String -> Class -> Id
classMethod String
"traverse" Class
travCls
          pureSel :: Id
pureSel     = String -> Class -> Id
classMethod String
"pure" Class
appCls
          apSel :: Id
apSel       = String -> Class -> Id
classMethod String
"<*>"  Class
appCls
          coAt :: Type -> Coercion
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
      Id
fTv <- Type -> String -> TcPluginM Id
freshTyVarK (HasDebugCallStack => Type -> Type -> Type
Type -> Type -> Type
mkVisFunTyMany Type
liftedTypeKind Type
liftedTypeKind) String
"f"  -- f :: Type -> Type
      Id
aTv <- String -> TcPluginM Id
freshTyVar String
"a" ; Id
bTv <- String -> TcPluginM Id
freshTyVar String
"b"
      let fTy :: Type
fTy = Id -> Type
mkTyVarTy Id
fTv ; aTy :: Type
aTy = Id -> Type
mkTyVarTy Id
aTv ; bTy :: Type
bTy = Id -> Type
mkTyVarTy Id
bTv
          fOf :: Type -> Type
fOf Type
t  = Type -> Type -> Type
mkAppTy Type
fTy Type
t
          innerA :: Type
innerA = TyCon -> [Type] -> Type
mkTyConApp TyCon
fTc ([Type]
fixed [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type
aTy])
          gTy :: Type
gTy    = HasDebugCallStack => Type -> Type -> Type
Type -> Type -> Type
mkVisFunTyMany Type
aTy (Type -> Type
fOf Type
bTy)              -- a -> f b
          stbTy :: Type
stbTy  = Type -> Type -> Type
mkAppTy Type
wrappedTy Type
bTy                     -- Stock1 F b
      Id
dApp <- Type -> String -> TcPluginM Id
freshId (Class -> [Type] -> Type
mkClassPred Class
appCls [Type
fTy]) String
"dApp"
      Id
gId  <- Type -> String -> TcPluginM Id
freshId Type
gTy String
"g"
      Id
xId  <- Type -> String -> TcPluginM Id
freshId (Type -> Type -> Type
mkAppTy Type
wrappedTy Type
aTy) String
"x"
      Id
cb   <- Type -> String -> TcPluginM Id
freshId Type
innerA String
"cb"
      let pureE :: Type -> Arg b -> Arg b
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 -> Type -> Arg b -> Arg b -> Arg b
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 -> Type
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 -> Expr Id -> TcPluginM (Maybe (Expr Id, [Ct]))
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
                [Id]
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
                [Maybe (Expr Id, [Ct])]
rs <- (Type -> Expr Id -> TcPluginM (Maybe (Expr Id, [Ct])))
-> [Type] -> [Expr Id] -> TcPluginM [Maybe (Expr Id, [Ct])]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Type -> Expr Id -> TcPluginM (Maybe (Expr Id, [Ct]))
traverseField [Type]
args ((Id -> Expr Id) -> [Id] -> [Expr Id]
forall a b. (a -> b) -> [a] -> [b]
map Id -> Expr Id
forall b. Id -> Expr b
Var [Id]
xs)
                case [Maybe (Expr Id, [Ct])] -> Maybe [(Expr Id, [Ct])]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence [Maybe (Expr Id, [Ct])]
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
                    [Id]
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
                    Id
cb <- Type -> String -> TcPluginM Id
freshId Type
ft String
"cb"
                    let mkTup :: Expr Id
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
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)
                    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 -> Id -> Type -> [Alt Id] -> Expr Id
forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Case Expr Id
xe Id
cb (Type -> Type
fOf Type
subTup) [AltCon -> [Id] -> Expr Id -> Alt Id
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt (DataCon -> AltCon
DataAlt DataCon
dc) [Id]
xs Expr Id
built]
                               , ((Expr Id, [Ct]) -> [Ct]) -> [(Expr Id, [Ct])] -> [Ct]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Expr Id, [Ct]) -> [Ct]
forall a b. (a, b) -> b
snd [(Expr Id, [Ct])]
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 CtEvidence
ev <- CtLoc -> Type -> TcPluginM CtEvidence
newWanted CtLoc
loc (Class -> [Type] -> Type
mkClassPred Class
travCls [Type
h])
                          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
mkApps (Id -> Expr Id
forall b. Id -> Expr b
Var Id
traverseSel)
                                 [Type -> Expr Id
forall b. Type -> Expr b
Type Type
h, 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
xe]
                                 , [CtEvidence -> Ct
mkNonCanonical CtEvidence
ev] ))
                  else do Id
y     <- Type -> String -> TcPluginM Id
freshId Type
larg String
"y"
                          Maybe (Expr Id, [Ct])
inner <- Type -> Expr Id -> TcPluginM (Maybe (Expr Id, [Ct]))
traverseField Type
larg (Id -> Expr Id
forall b. Id -> Expr b
Var Id
y)
                          case Maybe (Expr Id, [Ct])
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
                              CtEvidence
ev <- CtLoc -> Type -> TcPluginM CtEvidence
newWanted CtLoc
loc (Class -> [Type] -> Type
mkClassPred Class
travCls [Type
h])
                              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
mkApps (Id -> Expr Id
forall b. Id -> Expr b
Var Id
traverseSel)
                                     [Type -> Expr Id
forall b. Type -> Expr b
Type Type
h, 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
larg, Type -> Expr Id
forall b. Type -> Expr b
Type (Type -> Type
subB Type
larg)
                                     , Id -> Expr Id
forall b. Id -> Expr b
Var Id
dApp, Id -> Expr Id -> Expr Id
forall b. b -> Expr b -> Expr b
Lam Id
y Expr Id
e, Expr Id
xe]
                                     , CtEvidence -> Ct
mkNonCanonical CtEvidence
ev Ct -> [Ct] -> [Ct]
forall a. a -> [a] -> [a]
: [Ct]
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 -> Id -> Type -> Type -> TcPluginM (Maybe (Expr Id, [Ct]))
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@
              CtEvidence
ev <- CtLoc -> Type -> TcPluginM CtEvidence
newWanted CtLoc
loc (Class -> [Type] -> Type
mkClassPred Class
travCls [Type
m])
              let coS :: Coercion
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 :: Coercion
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
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)
              Id
mb <- Type -> String -> TcPluginM Id
freshId (Type -> Type -> Type
mkAppTy Type
m Type
bTy) String
"mb"
              let coerceFn :: Expr Id
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
              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 -> Type -> Expr Id -> Expr Id -> Expr Id
forall {b}. Type -> Type -> Arg b -> Arg b -> Arg b
apE (Type -> Type -> Type
mkAppTy Type
m Type
bTy) Type
rvFt
                             (Type -> Expr Id -> Expr Id
forall {b}. Type -> Arg b -> Arg b
pureE (HasDebugCallStack => Type -> Type -> Type
Type -> Type -> Type
mkVisFunTyMany (Type -> Type -> Type
mkAppTy Type
m Type
bTy) Type
rvFt) Expr Id
coerceFn) Expr Id
trav
                         , [CtEvidence -> Ct
mkNonCanonical CtEvidence
ev] ))
            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)
      [Maybe (Alt Id, [Ct])]
malts <- [DataCon]
-> (DataCon -> TcPluginM (Maybe (Alt Id, [Ct])))
-> TcPluginM [Maybe (Alt Id, [Ct])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [DataCon]
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]))
        [Id]
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
        [Maybe (Expr Id, [Ct])]
mfes <- [TcPluginM (Maybe (Expr Id, [Ct]))]
-> TcPluginM [Maybe (Expr Id, [Ct])]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence ((Int -> Id -> Type -> Type -> TcPluginM (Maybe (Expr Id, [Ct])))
-> [Int]
-> [Id]
-> [Type]
-> [Type]
-> [TcPluginM (Maybe (Expr Id, [Ct]))]
forall a b c d e.
(a -> b -> c -> d -> e) -> [a] -> [b] -> [c] -> [d] -> [e]
zipWith4 Int -> Id -> Type -> Type -> TcPluginM (Maybe (Expr Id, [Ct]))
fieldOf [Int
0 :: Int ..] [Id]
xs [Type]
fts [Type]
rvFts)
        case [Maybe (Expr Id, [Ct])] -> Maybe [(Expr Id, [Ct])]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence [Maybe (Expr Id, [Ct])]
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
            [Id]
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 :: Expr Id
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]
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
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)
            Maybe (Alt Id, [Ct]) -> TcPluginM (Maybe (Alt Id, [Ct]))
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Alt Id, [Ct]) -> Maybe (Alt Id, [Ct])
forall a. a -> Maybe a
Just (AltCon -> [Id] -> Expr Id -> Alt Id
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt (DataCon -> AltCon
DataAlt DataCon
dc) [Id]
xs Expr Id
body, [[Ct]] -> [Ct]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Ct]]
wss))
      case [Maybe (Alt Id, [Ct])] -> Maybe [(Alt Id, [Ct])]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence [Maybe (Alt Id, [Ct])]
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)
          Maybe (EvTerm, [Ct])
mFunc <- GenEnv
-> Class
-> CtLoc
-> Type
-> Type
-> TcPluginM (Maybe (EvTerm, [Ct]))
synthFunctor  GenEnv
gen Class
funcCls CtLoc
loc Type
wrappedTy Type
f
          Maybe (EvTerm, [Ct])
mFold <- GenEnv
-> Class
-> CtLoc
-> Type
-> Type
-> TcPluginM (Maybe (EvTerm, [Ct]))
synthFoldable GenEnv
gen Class
foldCls CtLoc
loc Type
wrappedTy Type
f
          case (Maybe (EvTerm, [Ct])
mFunc, Maybe (EvTerm, [Ct])
mFold) of
            (Just (EvTerm
fEv, [Ct]
fWs), Just (EvTerm
foEv, [Ct]
foWs)) -> do
              Expr Id
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)]
              Maybe (EvTerm, [Ct]) -> TcPluginM (Maybe (EvTerm, [Ct]))
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((EvTerm, [Ct]) -> Maybe (EvTerm, [Ct])
forall a. a -> Maybe a
Just (Expr Id -> EvTerm
EvExpr Expr Id
dict, [Ct]
fWs [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
foWs [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [[Ct]] -> [Ct]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Ct]]
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