{-# LANGUAGE CPP #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE DerivingVia #-}
{-# OPTIONS_GHC -Wno-x-partial -Wno-incomplete-uni-patterns -Wno-unused-imports #-}
-- | @Generic@ \/ @Generic1@ synthesizers: @Rep@ as a balanced @:+:@ \/ @:*:@ tree.
module Stock.Generic where
-- Most names below (data-con/type builders, coercion builders, occ-name
-- helpers, …) are re-exported by 'GHC.Plugins', so we only import explicitly
-- the ones it does not provide.
import GHC.Plugins hiding (TcPlugin)
import GHC.Tc.Plugin
import GHC.Tc.Types
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.Tc.Utils.Monad (addErrTc)
import GHC.Tc.Errors.Types (mkTcRnUnknownMessage)
import GHC.Types.Error (mkPlainError, noHints)
import GHC.Core.Class (Class, className, classMethods, classOpItems, classTyCon)
import GHC.Core.Predicate (classifyPredType, Pred(ClassPred), mkClassPred)
import GHC.Builtin.Types.Prim (intPrimTy)
import GHC.Builtin.PrimOps (PrimOp(TagToEnumOp))
import GHC.Builtin.PrimOps.Ids (primOpId)
import GHC.Builtin.Names ( eqClassName, ordClassName, appendName
                         , enumClassName, mapName, numClassName
                         , enumFromToName, enumFromThenToName
                         , eqStringName
                         , genClassName, repTyConName, u1TyConName, k1TyConName
                         , prodTyConName, sumTyConName
                         , monoidClassName, foldableClassName, functorClassName
                         , semigroupClassName )
import Stock.Compat ( gHC_INTERNAL_SHOW, gHC_INTERNAL_READ
                    , gHC_INTERNAL_LIST, gHC_INTERNAL_GENERICS )
import GHC.Core.Reduction (mkReduction)
import GHC.Core.TyCo.Rep (UnivCoProvenance(PluginProv))
import GHC.Rename.Fixity (lookupFixityRn)
import GHC.Types.Fixity (Fixity(..), defaultFixity)
import GHC.Core.TyCo.Compare (eqType)
import GHC.Core.Multiplicity (scaledThing)
import GHC.Core.SimpleOpt (defaultSimpleOpts)
import GHC.Core.Unfold.Make (mkInlineUnfoldingWithArity)
import GHC.Core.InstEnv (classInstances, is_dfun, is_tys)
import GHC.Runtime.Loader (getValueSafely)
import Stock.Derive
import Data.Maybe (catMaybes, fromJust, isJust, fromMaybe)
import qualified Data.Monoid as Mon (Alt(..))  -- 'Alt' clashes with GHC.Core's case-alt 'Alt'
import Stock.Trans (MaybeT(..))
import Control.Monad (forM, zipWithM, unless, guard)
import Data.IORef (IORef, newIORef, readIORef, modifyIORef')
import Stock.Internal

-- | Field types with @Override1@ modifiers applied: an @h a@ field whose config
-- names a modifier @m@ becomes @m a@ (so its @Rep1@ leaf is @Rec1 m@); all other
-- fields are unchanged.  Used by /both/ 'rewriteRep1' (the @Rep1@ type) and
-- 'synthGeneric1' (the @from1@\/@to1@ values), keeping them in lock-step.
reshape1Ftys :: GenEnv -> Maybe [Type] -> TyVar -> Type -> [Type] -> [Type]
reshape1Ftys :: GenEnv -> Maybe [Type] -> TyVar -> Type -> [Type] -> [Type]
reshape1Ftys GenEnv
gen Maybe [Type]
mMods TyVar
atv Type
aTy [Type]
fts =
  [ case (TyVar -> Type -> Type -> Maybe FieldKind
classifyField TyVar
atv Type
aTy Type
ft, GenEnv -> Maybe [Type] -> Int -> Maybe Type
override1Mod GenEnv
gen Maybe [Type]
mMods Int
i) of
      (Just (FApp Type
_), Just Type
m) -> Type -> Type -> Type
mkAppTy Type
m Type
aTy   -- @h a@ field → @m a@
      (Maybe FieldKind, Maybe Type)
_                       -> Type
ft
  | (Int
i, Type
ft) <- [Int] -> [Type] -> [(Int, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 :: Int ..] [Type]
fts ]

rewriteRep :: GenEnv -> RewriteEnv -> [Ct] -> [Type] -> TcPluginM TcPluginRewriteResult
rewriteRep :: GenEnv
-> RewriteEnv -> [Ct] -> [Type] -> TcPluginM TcPluginRewriteResult
rewriteRep GenEnv
gen RewriteEnv
_env [Ct]
_given [Type
arg]
  -- @Rep (Stock (Override T cfg))@: the leaves carry the /modifier/ types, so
  -- @Generically (Stock (Override T cfg))@ derives over the overridden fields.
  -- (Checked first; the plain branch would otherwise treat @Override@ as a data
  -- type.)  @synthGeneric@'s @from@\/@to@ coerce to match.
  | Just (Type
realInner, [(DataCon, [Type])]
cons) <- GenEnv -> Type -> Maybe (Type, [(DataCon, [Type])])
overrideFieldTypes GenEnv
gen Type
arg = do
      fixOf <- MetaEnv -> [DataCon] -> TcPluginM (DataCon -> Type)
mkFixOf (GenEnv -> MetaEnv
geMeta GenEnv
gen) (((DataCon, [Type]) -> DataCon) -> [(DataCon, [Type])] -> [DataCon]
forall a b. (a -> b) -> [a] -> [b]
map (DataCon, [Type]) -> DataCon
forall a b. (a, b) -> a
fst [(DataCon, [Type])]
cons)
      let struct = GenEnv -> (DataCon -> Type) -> Type -> [(DataCon, [Type])] -> Type
repMetaFts GenEnv
gen DataCon -> Type
fixOf Type
realInner [(DataCon, [Type])]
cons
          lhs    = TyCon -> [Type] -> Type
mkTyConApp (GenEnv -> TyCon
geRepTc GenEnv
gen) [Type
arg]
          co     = UnivCoProvenance -> Role -> Type -> Type -> Coercion
mkStockCo (String -> UnivCoProvenance
PluginProv String
"stock") Role
Nominal Type
lhs Type
struct
      pure (TcPluginRewriteTo (mkReduction co struct) [])
  | Just Repr
repr <- Maybe TyCon -> Type -> Maybe Repr
mkRepr (GenEnv -> Maybe TyCon
geStock GenEnv
gen) Type
arg, Bool -> Bool
not ([ConInfo] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Repr -> [ConInfo]
rCons Repr
repr)) = do
      fixOf <- MetaEnv -> [DataCon] -> TcPluginM (DataCon -> Type)
mkFixOf (GenEnv -> MetaEnv
geMeta GenEnv
gen) ((ConInfo -> DataCon) -> [ConInfo] -> [DataCon]
forall a b. (a -> b) -> [a] -> [b]
map ConInfo -> DataCon
ciCon (Repr -> [ConInfo]
rCons Repr
repr))
      let struct = GenEnv -> (DataCon -> Type) -> Type -> [DataCon] -> Type
repMeta GenEnv
gen DataCon -> Type
fixOf (Repr -> Type
rInner Repr
repr) ((ConInfo -> DataCon) -> [ConInfo] -> [DataCon]
forall a b. (a -> b) -> [a] -> [b]
map ConInfo -> DataCon
ciCon (Repr -> [ConInfo]
rCons Repr
repr))
          lhs    = TyCon -> [Type] -> Type
mkTyConApp (GenEnv -> TyCon
geRepTc GenEnv
gen) [Type
arg]
          co     = UnivCoProvenance -> Role -> Type -> Type -> Coercion
mkStockCo (String -> UnivCoProvenance
PluginProv String
"stock") Role
Nominal Type
lhs Type
struct
      pure (TcPluginRewriteTo (mkReduction co struct) [])
rewriteRep GenEnv
_ RewriteEnv
_ [Ct]
_ [Type]
_ = TcPluginRewriteResult -> TcPluginM TcPluginRewriteResult
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TcPluginRewriteResult
TcPluginNoRewrite

-- | Rewrite @Rep1 (Stock1 F)@ to the parameter-aware structure (@Par1@\/@Rec1@\/
-- @Rec0@ leaves under the @M1@ metadata).  No rewrite if any field is an
-- unsupported shape (composition etc.).
rewriteRep1 :: GenEnv -> RewriteEnv -> [Ct] -> [Type] -> TcPluginM TcPluginRewriteResult
rewriteRep1 :: GenEnv
-> RewriteEnv -> [Ct] -> [Type] -> TcPluginM TcPluginRewriteResult
rewriteRep1 GenEnv
gen RewriteEnv
_env [Ct]
_given [Type]
args
  | (Type
arg : [Type]
_)  <- [Type] -> [Type]
forall a. [a] -> [a]
reverse [Type]
args             -- @Rep1@ is poly-kinded: drop the kind arg
  , Just TyCon
st1Tc <- GenEnv -> Maybe TyCon
geStock1 GenEnv
gen
  , Just TyCon
stTc  <- Type -> Maybe TyCon
tyConAppTyCon_maybe Type
arg, TyCon
stTc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
st1Tc
  , (Type
_ : Type
f : [Type]
_) <- HasCallStack => Type -> [Type]
Type -> [Type]
tyConAppArgs Type
arg
    -- @f@ may be @Override1 cfg realF@: peel it, then reshape @h a@ fields to
    -- @m a@ so the @Rep1@ leaves use the modifier (in lock-step with 'synthGeneric1').
  , 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
      a0 <- String -> TcPluginM TyVar
freshTyVar String
"a"
      let aT0   = TyVar -> Type
mkTyVarTy TyVar
a0
          fixed = HasCallStack => Type -> [Type]
Type -> [Type]
tyConAppArgs Type
realF
          dcons = TyCon -> [DataCon]
tyConDataCons TyCon
fTc
          innerF = TyCon -> [Type] -> Type
mkTyConApp TyCon
fTc ([Type]
fixed [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type
aT0])
          ftysOf DataCon
dc = GenEnv -> Maybe [Type] -> TyVar -> Type -> [Type] -> [Type]
reshape1Ftys GenEnv
gen Maybe [Type]
mMods TyVar
a0 Type
aT0
                        ((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
aT0])))
          ok = (DataCon -> Bool) -> [DataCon] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Maybe Type -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Type -> Bool) -> (Type -> Maybe Type) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenEnv -> TyVar -> Type -> Maybe Type
rep1Field GenEnv
gen TyVar
a0) ([Type] -> Bool) -> (DataCon -> [Type]) -> DataCon -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCon -> [Type]
ftysOf) [DataCon]
dcons
      if not ok then pure TcPluginNoRewrite else do
        fixOf <- mkFixOf (geMeta gen) dcons
        let struct = GenEnv
-> (DataCon -> Type)
-> (Type -> Type)
-> Type
-> [(DataCon, [Type])]
-> Type
repMetaWith GenEnv
gen DataCon -> Type
fixOf (Maybe Type -> Type
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Type -> Type) -> (Type -> Maybe Type) -> Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenEnv -> TyVar -> Type -> Maybe Type
rep1Field GenEnv
gen TyVar
a0) Type
innerF
                       [ (DataCon
dc, DataCon -> [Type]
ftysOf DataCon
dc) | DataCon
dc <- [DataCon]
dcons ]
            lhs    = TyCon -> [Type] -> Type
mkTyConApp (Gen1Env -> TyCon
g1RepTc (GenEnv -> Gen1Env
geGen1 GenEnv
gen)) [Type]
args
            co     = UnivCoProvenance -> Role -> Type -> Type -> Coercion
mkStockCo (String -> UnivCoProvenance
PluginProv String
"stock") Role
Nominal Type
lhs Type
struct
        pure (TcPluginRewriteTo (mkReduction co struct) [])
rewriteRep1 GenEnv
_ RewriteEnv
_ [Ct]
_ [Type]
_ = TcPluginRewriteResult -> TcPluginM TcPluginRewriteResult
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TcPluginRewriteResult
TcPluginNoRewrite

-- | The structural @Rep@ for a whole datatype: a single constructor is just its
-- product 'repStruct'; several constructors form a /balanced/ @:+:@ tree of
-- their product structs (mirroring GHC's @foldBal@).
-- @cons@ carries each constructor's /modifier/ field types ('ciFields') and the
-- per-cell coercions ('ciFieldCos', @realFieldType ~R modifierType@; 'Refl'
-- without an @Override@).  The @Rep@ leaves use the modifier types (matching
-- 'rewriteRep'); @from@ coerces the real field /into/ the leaf, @to@ coerces
-- /back/ before rebuilding.  Refl everywhere ⇒ byte-identical Core to plain.
synthGeneric :: GenEnv -> Type -> Type -> Coercion -> [ConInfo] -> TcPluginM EvTerm
synthGeneric :: GenEnv -> Type -> Type -> Coercion -> [ConInfo] -> TcPluginM EvTerm
synthGeneric GenEnv
gen Type
wrappedTy Type
innerTy Coercion
co [ConInfo]
cons = do
  fixOf <- MetaEnv -> [DataCon] -> TcPluginM (DataCon -> Type)
mkFixOf (GenEnv -> MetaEnv
geMeta GenEnv
gen) ((ConInfo -> DataCon) -> [ConInfo] -> [DataCon]
forall a b. (a -> b) -> [a] -> [b]
map ConInfo -> DataCon
ciCon [ConInfo]
cons)
  let genCls = GenEnv -> Class
geGen GenEnv
gen
      k1Tc   = GenEnv -> TyCon
geK1Tc GenEnv
gen
      prodTc = GenEnv -> TyCon
geProdTc GenEnv
gen ; prodDc = GenEnv -> DataCon
geProdDc GenEnv
gen
      sumTc  = GenEnv -> TyCon
geSumTc GenEnv
gen
      [l1Dc, r1Dc] = tyConDataCons sumTc
      u1Dc   = [DataCon] -> DataCon
forall a. HasCallStack => [a] -> a
head (TyCon -> [DataCon]
tyConDataCons (GenEnv -> TyCon
geU1Tc GenEnv
gen))
      rTy    = GenEnv -> Type
geRTy GenEnv
gen
      kTy    = Type
liftedTypeKind
      dcons    = (ConInfo -> DataCon) -> [ConInfo] -> [DataCon]
forall a b. (a -> b) -> [a] -> [b]
map ConInfo -> DataCon
ciCon [ConInfo]
cons
      modFtss  = (ConInfo -> [Type]) -> [ConInfo] -> [[Type]]
forall a b. (a -> b) -> [a] -> [b]
map ConInfo -> [Type]
ciFields [ConInfo]
cons                    -- Rep leaves (modifier types)
      cosss    = (ConInfo -> [Coercion]) -> [ConInfo] -> [[Coercion]]
forall a b. (a -> b) -> [a] -> [b]
map ConInfo -> [Coercion]
ciFieldCos [ConInfo]
cons                  -- realFt ~R modFt per field
      realFtss = (DataCon -> [Type]) -> [DataCon] -> [[Type]]
forall a b. (a -> b) -> [a] -> [b]
map (Type -> DataCon -> [Type]
fieldTysAt Type
innerTy) [DataCon]
dcons        -- bound (pattern) types
      mfcss    = ([Type] -> [Coercion] -> [(Type, Coercion)])
-> [[Type]] -> [[Coercion]] -> [[(Type, Coercion)]]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith [Type] -> [Coercion] -> [(Type, Coercion)]
forall a b. [a] -> [b] -> [(a, b)]
zip [[Type]]
modFtss [[Coercion]]
cosss             -- per con: [(modFt, fco)]
      structMeta = GenEnv -> (DataCon -> Type) -> Type -> [(DataCon, [Type])] -> Type
repMetaFts GenEnv
gen DataCon -> Type
fixOf Type
innerTy ([DataCon] -> [[Type]] -> [(DataCon, [Type])]
forall a b. [a] -> [b] -> [(a, b)]
zip [DataCon]
dcons [[Type]]
modFtss)   -- faithful (rewrite-target) Rep
      structBare = GenEnv -> [[Type]] -> Type
repData GenEnv
gen [[Type]]
modFtss                          -- the un-M1 value structure
      lhs    = TyCon -> [Type] -> Type
mkTyConApp (GenEnv -> TyCon
geRepTc GenEnv
gen) [Type
wrappedTy]
      coRep  = UnivCoProvenance -> Role -> Type -> Type -> Coercion
mkStockCo (String -> UnivCoProvenance
PluginProv String
"stock") Role
Nominal Type
lhs Type
structMeta
      -- the M1 layers are newtypes, so structMeta ~R structBare (asserted, true)
      coStrip = UnivCoProvenance -> Role -> Type -> Type -> Coercion
mkStockCo (String -> UnivCoProvenance
PluginProv String
"stock") Role
Representational Type
structMeta Type
structBare

  ux <- unsafeTcPluginTcM getUniqueM
  let xtv = Name -> Type -> TyVar
mkTyVar (Unique -> OccName -> Name
mkSystemName Unique
ux (String -> OccName
mkTyVarOcc String
"x")) Type
liftedTypeKind
      xty = TyVar -> Type
mkTyVarTy TyVar
xtv
      prodTy Type
f Type
g = TyCon -> [Type] -> Type
mkTyConApp TyCon
prodTc [Type
kTy, Type
f, Type
g]
      sumTy  Type
f Type
g = TyCon -> [Type] -> Type
mkTyConApp TyCon
sumTc  [Type
kTy, Type
f, Type
g]
      -- Rep x ~R structMeta x ~R structBare x  (and back)
      castDn = HasDebugCallStack => Coercion -> Coercion
Coercion -> Coercion
mkSubCo (Coercion -> Coercion -> Coercion
mkAppCo Coercion
coRep (Type -> Coercion
mkNomReflCo Type
xty))             -- Rep x ~R structMeta x
                 Coercion -> Coercion -> Coercion
`mkTransCo` Coercion -> Coercion -> Coercion
mkAppCo Coercion
coStrip (Type -> Coercion
mkNomReflCo Type
xty)       -- structMeta x ~R structBare x
      castUp = Coercion -> Coercion
mkSymCo Coercion
castDn                                        -- structBare x ~R Rep x
      k1Co Type
ft     = Role -> CoAxiom Unbranched -> [Type] -> [Coercion] -> Coercion
mkUnbranchedAxInstCo Role
Representational
                      (TyCon -> CoAxiom Unbranched
newTyConCo TyCon
k1Tc) [Type
kTy, Type
rTy, Type
ft, Type
xty] []   -- K1 R ft x ~R ft
      -- from: real field value (fi :: realFt) coerced to its modifier type, into K1 modFt
      k1ValOv Coercion
fco Type
mft TyVar
fi = Expr TyVar -> Coercion -> Expr TyVar
forall b. Expr b -> Coercion -> Expr b
Cast (Expr TyVar -> Coercion -> Expr TyVar
castInto (TyVar -> Expr TyVar
forall b. TyVar -> Expr b
Var TyVar
fi) Coercion
fco) (Coercion -> Coercion
mkSymCo (Type -> Coercion
k1Co Type
mft))
      -- to: a K1 modFt projection back to the real field type
      unK1Ov  Coercion
fco Type
mft Expr TyVar
scr = Expr TyVar -> Coercion -> Expr TyVar
castInto (Expr TyVar -> Coercion -> Expr TyVar
forall b. Expr b -> Coercion -> Expr b
Cast Expr TyVar
scr (Type -> Coercion
k1Co Type
mft)) (Coercion -> Coercion
mkSymCo Coercion
fco)
      -- balanced product VALUE (+ its type), mirroring 'repStruct'/'foldBal'
      buildV [(Expr TyVar
v, Type
t)] = (Expr TyVar
v, Type
t)
      buildV [(Expr TyVar, Type)]
vs = let ([(Expr TyVar, Type)]
l, [(Expr TyVar, Type)]
r)  = Int
-> [(Expr TyVar, Type)]
-> ([(Expr TyVar, Type)], [(Expr TyVar, Type)])
forall a. Int -> [a] -> ([a], [a])
splitAt ([(Expr TyVar, Type)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Expr TyVar, Type)]
vs Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2) [(Expr TyVar, Type)]
vs
                      (Expr TyVar
lv, Type
lt) = [(Expr TyVar, Type)] -> (Expr TyVar, Type)
buildV [(Expr TyVar, Type)]
l ; (Expr TyVar
rv, Type
rt) = [(Expr TyVar, Type)] -> (Expr TyVar, Type)
buildV [(Expr TyVar, Type)]
r
                  in ( DataCon -> [Expr TyVar] -> Expr TyVar
mkCoreConApps DataCon
prodDc [Type -> Expr TyVar
forall b. Type -> Expr b
Type Type
kTy, Type -> Expr TyVar
forall b. Type -> Expr b
Type Type
lt, Type -> Expr TyVar
forall b. Type -> Expr b
Type Type
rt, Type -> Expr TyVar
forall b. Type -> Expr b
Type Type
xty, Expr TyVar
lv, Expr TyVar
rv]
                     , Type -> Type -> Type
prodTy Type
lt Type
rt )
      -- product value for one constructor's fields (per field: its (modFt, fco) + binder)
      prodValOf [(Type, Coercion)]
mfcs [TyVar]
fis
        | [(Type, Coercion)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Type, Coercion)]
mfcs = DataCon -> [Expr TyVar] -> Expr TyVar
mkCoreConApps DataCon
u1Dc [Type -> Expr TyVar
forall b. Type -> Expr b
Type Type
kTy, Type -> Expr TyVar
forall b. Type -> Expr b
Type Type
xty]
        | Bool
otherwise = (Expr TyVar, Type) -> Expr TyVar
forall a b. (a, b) -> a
fst ([(Expr TyVar, Type)] -> (Expr TyVar, Type)
buildV [ (Coercion -> Type -> TyVar -> Expr TyVar
k1ValOv Coercion
fco Type
mft TyVar
fi, TyCon -> [Type] -> Type
mkTyConApp TyCon
k1Tc [Type
kTy, Type
rTy, Type
mft])
                                  | ((Type
mft, Coercion
fco), TyVar
fi) <- [(Type, Coercion)] -> [TyVar] -> [((Type, Coercion), TyVar)]
forall a b. [a] -> [b] -> [(a, b)]
zip [(Type, Coercion)]
mfcs [TyVar]
fis ])
      -- balanced @:+:@ injectors (one per constructor) + the sum type
      injectors [[Type]
fts] = ([Expr TyVar -> Expr TyVar
forall a. a -> a
id], GenEnv -> [Type] -> Type
repStruct GenEnv
gen [Type]
fts)
      injectors [[Type]]
fss   =
        let ([[Type]]
l, [[Type]]
r)   = Int -> [[Type]] -> ([[Type]], [[Type]])
forall a. Int -> [a] -> ([a], [a])
splitAt ([[Type]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Type]]
fss Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2) [[Type]]
fss
            ([Expr TyVar -> Expr TyVar]
li, Type
lt) = [[Type]] -> ([Expr TyVar -> Expr TyVar], Type)
injectors [[Type]]
l ; ([Expr TyVar -> Expr TyVar]
ri, Type
rt) = [[Type]] -> ([Expr TyVar -> Expr TyVar], Type)
injectors [[Type]]
r
            wrapL :: Expr TyVar -> Expr TyVar
wrapL Expr TyVar
v  = DataCon -> [Expr TyVar] -> Expr TyVar
mkCoreConApps DataCon
l1Dc [Type -> Expr TyVar
forall b. Type -> Expr b
Type Type
kTy, Type -> Expr TyVar
forall b. Type -> Expr b
Type Type
lt, Type -> Expr TyVar
forall b. Type -> Expr b
Type Type
rt, Type -> Expr TyVar
forall b. Type -> Expr b
Type Type
xty, Expr TyVar
v]
            wrapR :: Expr TyVar -> Expr TyVar
wrapR Expr TyVar
v  = DataCon -> [Expr TyVar] -> Expr TyVar
mkCoreConApps DataCon
r1Dc [Type -> Expr TyVar
forall b. Type -> Expr b
Type Type
kTy, Type -> Expr TyVar
forall b. Type -> Expr b
Type Type
lt, Type -> Expr TyVar
forall b. Type -> Expr b
Type Type
rt, Type -> Expr TyVar
forall b. Type -> Expr b
Type Type
xty, Expr TyVar
v]
        in (((Expr TyVar -> Expr TyVar) -> Expr TyVar -> Expr TyVar)
-> [Expr TyVar -> Expr TyVar] -> [Expr TyVar -> Expr TyVar]
forall a b. (a -> b) -> [a] -> [b]
map (Expr TyVar -> Expr TyVar
wrapL (Expr TyVar -> Expr TyVar)
-> (Expr TyVar -> Expr TyVar) -> Expr TyVar -> Expr TyVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) [Expr TyVar -> Expr TyVar]
li [Expr TyVar -> Expr TyVar]
-> [Expr TyVar -> Expr TyVar] -> [Expr TyVar -> Expr TyVar]
forall a. [a] -> [a] -> [a]
++ ((Expr TyVar -> Expr TyVar) -> Expr TyVar -> Expr TyVar)
-> [Expr TyVar -> Expr TyVar] -> [Expr TyVar -> Expr TyVar]
forall a b. (a -> b) -> [a] -> [b]
map (Expr TyVar -> Expr TyVar
wrapR (Expr TyVar -> Expr TyVar)
-> (Expr TyVar -> Expr TyVar) -> Expr TyVar -> Expr TyVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) [Expr TyVar -> Expr TyVar]
ri, Type -> Type -> Type
sumTy Type
lt Type
rt)
      (injs, _) = injectors modFtss

  -- from = /\x. \v -> case (v |> co) of  Cᵢ f.. -> injᵢ <product> |> castUp
  vId <- freshId wrappedTy "v"
  cbV <- freshId innerTy "cb"
  fromAlts <- forM (zip dcons (zip3 realFtss mfcss injs)) \(DataCon
dc, ([Type]
realFts, [(Type, Coercion)]
mfcs, Expr TyVar -> Expr TyVar
inj)) -> do
    fis <- (Int -> Type -> TcPluginM TyVar)
-> [Int] -> [Type] -> TcPluginM [TyVar]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (\Int
n Type
ft -> Type -> String -> TcPluginM TyVar
freshId Type
ft (String
"f" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n)) [Int
0 :: Int ..] [Type]
realFts
    pure (Alt (DataAlt dc) fis (Cast (inj (prodValOf mfcs fis)) castUp))
  let fromImpl = TyVar -> Expr TyVar -> Expr TyVar
forall b. b -> Expr b -> Expr b
Lam TyVar
xtv (TyVar -> Expr TyVar -> Expr TyVar
forall b. b -> Expr b -> Expr b
Lam TyVar
vId
                   (Expr TyVar -> TyVar -> Type -> [Alt TyVar] -> Expr TyVar
forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Case (Expr TyVar -> Coercion -> Expr TyVar
forall b. Expr b -> Coercion -> Expr b
Cast (TyVar -> Expr TyVar
forall b. TyVar -> Expr b
Var TyVar
vId) Coercion
co) TyVar
cbV (Type -> Type -> Type
mkAppTy Type
lhs Type
xty) [Alt TyVar]
fromAlts))

  -- to = /\x. \r -> <project (r |> castDn) through :+: / :*:, rebuild Cᵢ>
  rId <- freshId (mkAppTy lhs xty) "r"
  let -- take apart a balanced :*: product (typed by the modifier types), returning the
      -- real-typed field exprs (each projected then coerced back) + a case-nesting wrapper
      destruct Expr TyVar
scr [(Type
mft, Coercion
fco)] = ([Expr TyVar], Expr TyVar -> Expr TyVar)
-> TcPluginM ([Expr TyVar], Expr TyVar -> Expr TyVar)
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Coercion -> Type -> Expr TyVar -> Expr TyVar
unK1Ov Coercion
fco Type
mft Expr TyVar
scr], Expr TyVar -> Expr TyVar
forall a. a -> a
id)
      destruct Expr TyVar
scr [(Type, Coercion)]
mfs = do
        let ([(Type, Coercion)]
lT, [(Type, Coercion)]
rT) = Int
-> [(Type, Coercion)] -> ([(Type, Coercion)], [(Type, Coercion)])
forall a. Int -> [a] -> ([a], [a])
splitAt ([(Type, Coercion)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Type, Coercion)]
mfs Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2) [(Type, Coercion)]
mfs
            lt :: Type
lt = GenEnv -> [Type] -> Type
repStruct GenEnv
gen (((Type, Coercion) -> Type) -> [(Type, Coercion)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Type, Coercion) -> Type
forall a b. (a, b) -> a
fst [(Type, Coercion)]
lT) ; rt :: Type
rt = GenEnv -> [Type] -> Type
repStruct GenEnv
gen (((Type, Coercion) -> Type) -> [(Type, Coercion)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Type, Coercion) -> Type
forall a b. (a, b) -> a
fst [(Type, Coercion)]
rT)
        lv <- Type -> String -> TcPluginM TyVar
freshId (Type -> Type -> Type
mkAppTy Type
lt Type
xty) String
"l"
        rv <- freshId (mkAppTy rt xty) "rr"
        cb <- freshId (mkAppTy (prodTy lt rt) xty) "pc"
        (lfs, lwrap) <- destruct (Var lv) lT
        (rfs, rwrap) <- destruct (Var rv) rT
        let wrap Expr TyVar
body = Expr TyVar -> TyVar -> Type -> [Alt TyVar] -> Expr TyVar
forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Case Expr TyVar
scr TyVar
cb Type
wrappedTy
                          [AltCon -> [TyVar] -> Expr TyVar -> Alt TyVar
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt (DataCon -> AltCon
DataAlt DataCon
prodDc) [TyVar
lv, TyVar
rv] (Expr TyVar -> Expr TyVar
lwrap (Expr TyVar -> Expr TyVar
rwrap Expr TyVar
body))]
        pure (lfs ++ rfs, wrap)
      -- rebuild one constructor from its product struct
      rebuildCon Expr TyVar
scr [(Type, Coercion)]
mfs DataCon
dc
        | [(Type, Coercion)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Type, Coercion)]
mfs  = Expr TyVar -> TcPluginM (Expr TyVar)
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr TyVar -> Coercion -> Expr TyVar
forall b. Expr b -> Coercion -> Expr b
Cast (Type -> DataCon -> [Expr TyVar] -> Expr TyVar
conAppAt Type
innerTy DataCon
dc []) (Coercion -> Coercion
mkSymCo Coercion
co))
        | Bool
otherwise = do (fields, wrap) <- Expr TyVar
-> [(Type, Coercion)]
-> TcPluginM ([Expr TyVar], Expr TyVar -> Expr TyVar)
destruct Expr TyVar
scr [(Type, Coercion)]
mfs
                         pure (wrap (Cast (conAppAt innerTy dc fields) (mkSymCo co)))
      -- project through the balanced :+: tree, rebuilding at each leaf
      destructSum Expr TyVar
scr [[(Type, Coercion)]
mfs] [DataCon
dc] = Expr TyVar
-> [(Type, Coercion)] -> DataCon -> TcPluginM (Expr TyVar)
rebuildCon Expr TyVar
scr [(Type, Coercion)]
mfs DataCon
dc
      destructSum Expr TyVar
scr [[(Type, Coercion)]]
mfss  [DataCon]
dcs  = do
        let h :: Int
h          = [[(Type, Coercion)]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[(Type, Coercion)]]
mfss Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2
            ([[(Type, Coercion)]]
lfs, [[(Type, Coercion)]]
rfs) = Int
-> [[(Type, Coercion)]]
-> ([[(Type, Coercion)]], [[(Type, Coercion)]])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
h [[(Type, Coercion)]]
mfss ; ([DataCon]
ldc, [DataCon]
rdc) = Int -> [DataCon] -> ([DataCon], [DataCon])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
h [DataCon]
dcs
            lt :: Type
lt = GenEnv -> [[Type]] -> Type
repData GenEnv
gen (([(Type, Coercion)] -> [Type]) -> [[(Type, Coercion)]] -> [[Type]]
forall a b. (a -> b) -> [a] -> [b]
map (((Type, Coercion) -> Type) -> [(Type, Coercion)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Type, Coercion) -> Type
forall a b. (a, b) -> a
fst) [[(Type, Coercion)]]
lfs) ; rt :: Type
rt = GenEnv -> [[Type]] -> Type
repData GenEnv
gen (([(Type, Coercion)] -> [Type]) -> [[(Type, Coercion)]] -> [[Type]]
forall a b. (a -> b) -> [a] -> [b]
map (((Type, Coercion) -> Type) -> [(Type, Coercion)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Type, Coercion) -> Type
forall a b. (a, b) -> a
fst) [[(Type, Coercion)]]
rfs)
        lv <- Type -> String -> TcPluginM TyVar
freshId (Type -> Type -> Type
mkAppTy Type
lt Type
xty) String
"sl"
        rv <- freshId (mkAppTy rt xty) "sr"
        cb <- freshId (mkAppTy (sumTy lt rt) xty) "sc"
        lbody <- destructSum (Var lv) lfs ldc
        rbody <- destructSum (Var rv) rfs rdc
        pure (Case scr cb wrappedTy
                [ Alt (DataAlt l1Dc) [lv] lbody, Alt (DataAlt r1Dc) [rv] rbody ])
  toBody <- destructSum (Cast (Var rId) castDn) mfcss dcons
  let toImpl = TyVar -> Expr TyVar -> Expr TyVar
forall b. b -> Expr b -> Expr b
Lam TyVar
xtv (TyVar -> Expr TyVar -> Expr TyVar
forall b. b -> Expr b -> Expr b
Lam TyVar
rId Expr TyVar
toBody)

  pure $ EvExpr $ mkClassDict genCls wrappedTy [fromImpl, toImpl]

-- | Synthesize @Generic1 (Stock1 F)@: like 'synthGeneric' but the field
-- representation is parameter-aware — the last type variable @a@ becomes
-- @Par1@, @g a@ becomes @Rec1 g@, a constant becomes @Rec0@ (see 'rep1Field').
-- @from1@\/@to1@ wrap\/unwrap each field through the corresponding newtype.
-- 'Nothing' for shapes 'rep1Field' rejects (e.g. composition @f (g a)@).
synthGeneric1 :: GenEnv -> Class -> CtLoc -> Type -> Type
              -> TcPluginM (Maybe (EvTerm, [Ct]))
synthGeneric1 :: GenEnv
-> Class
-> CtLoc
-> Type
-> Type
-> TcPluginM (Maybe (EvTerm, [Ct]))
synthGeneric1 GenEnv
gen Class
cls CtLoc
loc Type
wrappedTy Type
f =
  case (GenEnv -> Maybe TyCon
geStock1 GenEnv
gen, Type -> Maybe TyCon
tyConAppTyCon_maybe Type
realF) of
    (Just TyCon
st1Tc, Just TyCon
fTc) -> do
      functorCls <- Name -> TcPluginM Class
tcLookupClass Name
functorClassName
      let g1     = GenEnv -> Gen1Env
geGen1 GenEnv
gen
          fixed  = HasCallStack => Type -> [Type]
Type -> [Type]
tyConAppArgs Type
realF
          dcons  = TyCon -> [DataCon]
tyConDataCons TyCon
fTc
          k1Tc   = GenEnv -> TyCon
geK1Tc GenEnv
gen ; rTy = GenEnv -> Type
geRTy GenEnv
gen ; kTy = Type
liftedTypeKind
          par1Tc = Gen1Env -> TyCon
g1Par1Tc Gen1Env
g1 ; rec1Tc = Gen1Env -> TyCon
g1Rec1Tc Gen1Env
g1 ; compTc = Gen1Env -> TyCon
g1CompTc Gen1Env
g1
          fmapSel = String -> Class -> TyVar
classMethod String
"fmap" Class
functorCls
          prodTc = GenEnv -> TyCon
geProdTc GenEnv
gen ; prodDc = GenEnv -> DataCon
geProdDc GenEnv
gen
          sumTc  = GenEnv -> TyCon
geSumTc GenEnv
gen ; [l1Dc, r1Dc] = tyConDataCons sumTc
          u1Dc   = [DataCon] -> DataCon
forall a. HasCallStack => [a] -> a
head (TyCon -> [DataCon]
tyConDataCons (GenEnv -> TyCon
geU1Tc GenEnv
gen))
          coAt Type
t = GenEnv -> TyCon -> Type -> Type -> Type -> Type -> Coercion
coDown1 GenEnv
gen TyCon
st1Tc Type
wrappedTy Type
f Type
realF Type
t
      atv <- freshTyVar "a"
      let aTy    = TyVar -> Type
mkTyVarTy TyVar
atv
          innerA = TyCon -> [Type] -> Type
mkTyConApp TyCon
fTc ([Type]
fixed [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type
aTy])
          prodTy Type
a Type
b = TyCon -> [Type] -> Type
mkTyConApp TyCon
prodTc [Type
kTy, Type
a, Type
b]
          sumTy  Type
a Type
b = TyCon -> [Type] -> Type
mkTyConApp TyCon
sumTc  [Type
kTy, Type
a, Type
b]
          u1Ty   = TyCon -> [Type] -> Type
mkTyConApp (GenEnv -> TyCon
geU1Tc GenEnv
gen) [Type
kTy]
          par1Co   = Role -> CoAxiom Unbranched -> [Type] -> [Coercion] -> Coercion
mkUnbranchedAxInstCo Role
Representational (TyCon -> CoAxiom Unbranched
newTyConCo TyCon
par1Tc) [Type
aTy] []
          rec1Co Type
h = Role -> CoAxiom Unbranched -> [Type] -> [Coercion] -> Coercion
mkUnbranchedAxInstCo Role
Representational (TyCon -> CoAxiom Unbranched
newTyConCo TyCon
rec1Tc) [Type
kTy, Type
h, Type
aTy] []
          k1Co Type
t   = Role -> CoAxiom Unbranched -> [Type] -> [Coercion] -> Coercion
mkUnbranchedAxInstCo Role
Representational (TyCon -> CoAxiom Unbranched
newTyConCo TyCon
k1Tc) [Type
kTy, Type
rTy, Type
t, Type
aTy] []
          fieldsOf DataCon
dc = (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]))
          -- classify a field → (bare leaf type, wrap, unwrap, emitted wanteds).
          -- wrap\/unwrap are value transforms; composition emits a @Functor@
          -- wanted and uses @Comp1 . fmap innerWrap@ (matching GHC's DeriveGeneric1).
          classify1 Maybe Type
mMod Type
ft
            | Type
ft Type -> Type -> Bool
`eqType` Type
aTy =
                Maybe
  (Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar, [Ct])
-> TcPluginM
     (Maybe
        (Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar, [Ct]))
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar, [Ct])
-> Maybe
     (Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar, [Ct])
forall a. a -> Maybe a
Just (TyCon -> Type
mkTyConTy TyCon
par1Tc, \Expr TyVar
e -> Expr TyVar -> Coercion -> Expr TyVar
forall b. Expr b -> Coercion -> Expr b
Cast Expr TyVar
e (Coercion -> Coercion
mkSymCo Coercion
par1Co), \Expr TyVar
e -> Expr TyVar -> Coercion -> Expr TyVar
forall b. Expr b -> Coercion -> Expr b
Cast Expr TyVar
e Coercion
par1Co, []))
            | Bool -> Bool
not (TyVar
atv TyVar -> VarSet -> Bool
`elemVarSet` Type -> VarSet
tyCoVarsOfType Type
ft) =
                Maybe
  (Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar, [Ct])
-> TcPluginM
     (Maybe
        (Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar, [Ct]))
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar, [Ct])
-> Maybe
     (Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar, [Ct])
forall a. a -> Maybe a
Just (TyCon -> [Type] -> Type
mkTyConApp TyCon
k1Tc [Type
kTy, Type
rTy, Type
ft], \Expr TyVar
e -> Expr TyVar -> Coercion -> Expr TyVar
forall b. Expr b -> Coercion -> Expr b
Cast Expr TyVar
e (Coercion -> Coercion
mkSymCo (Type -> Coercion
k1Co Type
ft)), \Expr TyVar
e -> Expr TyVar -> Coercion -> Expr TyVar
forall b. Expr b -> Coercion -> Expr b
Cast Expr TyVar
e (Type -> Coercion
k1Co Type
ft), []))
            | Just (Type
h, Type
larg) <- Type -> Maybe (Type, Type)
splitAppTy_maybe Type
ft
            , Bool -> Bool
not (TyVar
atv TyVar -> VarSet -> Bool
`elemVarSet` Type -> VarSet
tyCoVarsOfType Type
h) =
                if Type
larg Type -> Type -> Bool
`eqType` Type
aTy
                  -- @h a@ leaf, reshaped to @Rec1 m@ under @Override1@: wrap coerces
                  -- the field value @h a ~R m a@ then into @Rec1 m a@; unwrap reverses.
                  then let m :: Type
m  = Type -> Maybe Type -> Type
forall a. a -> Maybe a -> a
fromMaybe Type
h Maybe Type
mMod
                           co :: Coercion
co = Type -> Type -> Type -> Coercion
reshapeCo Type
h Type
m Type
aTy
                       in Maybe
  (Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar, [Ct])
-> TcPluginM
     (Maybe
        (Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar, [Ct]))
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar, [Ct])
-> Maybe
     (Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar, [Ct])
forall a. a -> Maybe a
Just ( TyCon -> [Type] -> Type
mkTyConApp TyCon
rec1Tc [Type
kTy, Type
m]
                                     , \Expr TyVar
e -> Expr TyVar -> Coercion -> Expr TyVar
forall b. Expr b -> Coercion -> Expr b
Cast Expr TyVar
e (Coercion
co Coercion -> Coercion -> Coercion
`mkTransCo` Coercion -> Coercion
mkSymCo (Type -> Coercion
rec1Co Type
m))
                                     , \Expr TyVar
e -> Expr TyVar -> Coercion -> Expr TyVar
forall b. Expr b -> Coercion -> Expr b
Cast Expr TyVar
e (Type -> Coercion
rec1Co Type
m Coercion -> Coercion -> Coercion
`mkTransCo` Coercion -> Coercion
mkSymCo Coercion
co), [] ))
                  else do
                    minner <- Maybe Type
-> Type
-> TcPluginM
     (Maybe
        (Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar, [Ct]))
classify1 Maybe Type
forall a. Maybe a
Nothing Type
larg
                    case minner of
                      Maybe
  (Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar, [Ct])
Nothing -> Maybe
  (Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar, [Ct])
-> TcPluginM
     (Maybe
        (Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar, [Ct]))
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe
  (Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar, [Ct])
forall a. Maybe a
Nothing
                      Just (Type
innerRep, Expr TyVar -> Expr TyVar
innerWrap, Expr TyVar -> Expr TyVar
innerUnwrap, [Ct]
iws) -> do
                        ev  <- CtLoc -> Type -> TcPluginM CtEvidence
newWanted CtLoc
loc (Class -> [Type] -> Type
mkClassPred Class
functorCls [Type
h])
                        yId <- freshId larg "y"
                        zId <- freshId (mkAppTy innerRep aTy) "z"
                        let dict      = HasDebugCallStack => CtEvidence -> Expr TyVar
CtEvidence -> Expr TyVar
ctEvExpr CtEvidence
ev
                            compTy    = TyCon -> [Type] -> Type
mkTyConApp TyCon
compTc [Type
kTy, Type
kTy, Type
h, Type
innerRep]
                            comp1Co   = Role -> CoAxiom Unbranched -> [Type] -> [Coercion] -> Coercion
mkUnbranchedAxInstCo Role
Representational
                                          (TyCon -> CoAxiom Unbranched
newTyConCo TyCon
compTc) [Type
kTy, Type
kTy, Type
h, Type
innerRep, Type
aTy] []
                            innerAppA = Type -> Type -> Type
mkAppTy Type
innerRep Type
aTy
                            fmapAt Type
aT Type
bT Expr TyVar
fn Expr TyVar
x = Expr TyVar -> [Expr TyVar] -> Expr TyVar
forall b. Expr b -> [Expr b] -> Expr b
mkApps (TyVar -> Expr TyVar
forall b. TyVar -> Expr b
Var TyVar
fmapSel) [Type -> Expr TyVar
forall b. Type -> Expr b
Type Type
h, Expr TyVar
dict, Type -> Expr TyVar
forall b. Type -> Expr b
Type Type
aT, Type -> Expr TyVar
forall b. Type -> Expr b
Type Type
bT, Expr TyVar
fn, Expr TyVar
x]
                            -- Comp1 (fmap innerWrap e)        :: (h :.: innerRep) a
                            wrapE Expr TyVar
e   = Expr TyVar -> Coercion -> Expr TyVar
forall b. Expr b -> Coercion -> Expr b
Cast (Type -> Type -> Expr TyVar -> Expr TyVar -> Expr TyVar
fmapAt Type
larg Type
innerAppA ([TyVar] -> Expr TyVar -> Expr TyVar
forall b. [b] -> Expr b -> Expr b
mkLams [TyVar
yId] (Expr TyVar -> Expr TyVar
innerWrap (TyVar -> Expr TyVar
forall b. TyVar -> Expr b
Var TyVar
yId))) Expr TyVar
e)
                                             (Coercion -> Coercion
mkSymCo Coercion
comp1Co)
                            -- fmap innerUnwrap (unComp1 e)    :: h larg
                            unwrapE Expr TyVar
e = Type -> Type -> Expr TyVar -> Expr TyVar -> Expr TyVar
fmapAt Type
innerAppA Type
larg ([TyVar] -> Expr TyVar -> Expr TyVar
forall b. [b] -> Expr b -> Expr b
mkLams [TyVar
zId] (Expr TyVar -> Expr TyVar
innerUnwrap (TyVar -> Expr TyVar
forall b. TyVar -> Expr b
Var TyVar
zId))) (Expr TyVar -> Coercion -> Expr TyVar
forall b. Expr b -> Coercion -> Expr b
Cast Expr TyVar
e Coercion
comp1Co)
                        pure (Just (compTy, wrapE, unwrapE, mkNonCanonical ev : iws))
            | Bool
otherwise = Maybe
  (Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar, [Ct])
-> TcPluginM
     (Maybe
        (Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar, [Ct]))
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe
  (Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar, [Ct])
forall a. Maybe a
Nothing
      classifiedM <- forM dcons \DataCon
dc ->
        (Int
 -> Type
 -> TcPluginM
      (Maybe
         (Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar, [Ct])))
-> [Int]
-> [Type]
-> TcPluginM
     [Maybe
        (Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar, [Ct])]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (\Int
i Type
ft -> Maybe Type
-> Type
-> TcPluginM
     (Maybe
        (Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar, [Ct]))
classify1 (GenEnv -> Maybe [Type] -> Int -> Maybe Type
override1Mod GenEnv
gen Maybe [Type]
mMods Int
i) Type
ft) [Int
0 :: Int ..] (DataCon -> [Type]
fieldsOf DataCon
dc)
      case traverse sequence classifiedM of
        Maybe
  [[(Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar,
     [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 [[(Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar,
   [Ct])]]
classified -> do
          fixOf <- MetaEnv -> [DataCon] -> TcPluginM (DataCon -> Type)
mkFixOf (GenEnv -> MetaEnv
geMeta GenEnv
gen) [DataCon]
dcons
          let fieldWanteds = ([(Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar, [Ct])]
 -> [Ct])
-> [[(Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar,
      [Ct])]]
-> [Ct]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (((Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar, [Ct])
 -> [Ct])
-> [(Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar,
     [Ct])]
-> [Ct]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(Type
_, Expr TyVar -> Expr TyVar
_, Expr TyVar -> Expr TyVar
_, [Ct]
ws) -> [Ct]
ws)) [[(Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar,
   [Ct])]]
classified
              leafTys [(a, b, c, d)]
con = [ a
lt | (a
lt, b
_, c
_, d
_) <- [(a, b, c, d)]
con ]
              bareCon [(Type, b, c, d)]
con = case [(Type, b, c, d)] -> [Type]
forall {a} {b} {c} {d}. [(a, b, c, d)] -> [a]
leafTys [(Type, b, c, d)]
con of { [] -> Type
u1Ty; [Type]
lts -> (Type -> Type -> Type) -> [Type] -> Type
forall a. (a -> a -> a) -> [a] -> a
foldBal Type -> Type -> Type
prodTy [Type]
lts }
              structBare  = case ([(Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar, [Ct])]
 -> Type)
-> [[(Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar,
      [Ct])]]
-> [Type]
forall a b. (a -> b) -> [a] -> [b]
map [(Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar, [Ct])]
-> Type
forall {b} {c} {d}. [(Type, b, c, d)] -> Type
bareCon [[(Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar,
   [Ct])]]
classified of { [Type
s] -> Type
s; [Type]
ss -> (Type -> Type -> Type) -> [Type] -> Type
forall a. (a -> a -> a) -> [a] -> a
foldBal Type -> Type -> Type
sumTy [Type]
ss }
              structMeta  = GenEnv
-> (DataCon -> Type)
-> (Type -> Type)
-> Type
-> [(DataCon, [Type])]
-> Type
repMetaWith GenEnv
gen DataCon -> Type
fixOf (Maybe Type -> Type
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Type -> Type) -> (Type -> Maybe Type) -> Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenEnv -> TyVar -> Type -> Maybe Type
rep1Field GenEnv
gen TyVar
atv) Type
innerA
                              [ (DataCon
dc, GenEnv -> Maybe [Type] -> TyVar -> Type -> [Type] -> [Type]
reshape1Ftys GenEnv
gen Maybe [Type]
mMods TyVar
atv Type
aTy (Type -> DataCon -> [Type]
fieldTysAt Type
innerA DataCon
dc)) | DataCon
dc <- [DataCon]
dcons ]
              lhs1   = TyCon -> [Type] -> Type
mkTyConApp (Gen1Env -> TyCon
g1RepTc Gen1Env
g1) [Type
liftedTypeKind, Type
wrappedTy]
              coRep  = UnivCoProvenance -> Role -> Type -> Type -> Coercion
mkStockCo (String -> UnivCoProvenance
PluginProv String
"stock") Role
Nominal Type
lhs1 Type
structMeta
              coStrip = UnivCoProvenance -> Role -> Type -> Type -> Coercion
mkStockCo (String -> UnivCoProvenance
PluginProv String
"stock") Role
Representational Type
structMeta Type
structBare
              castDn = HasDebugCallStack => Coercion -> Coercion
Coercion -> Coercion
mkSubCo (Coercion -> Coercion -> Coercion
mkAppCo Coercion
coRep (Type -> Coercion
mkNomReflCo Type
aTy))
                         Coercion -> Coercion -> Coercion
`mkTransCo` Coercion -> Coercion -> Coercion
mkAppCo Coercion
coStrip (Type -> Coercion
mkNomReflCo Type
aTy)   -- Rep1..a ~R structBare a
              castUp = Coercion -> Coercion
mkSymCo Coercion
castDn
              -- balanced :*: VALUE for one constructor (over the leaf values/types)
              buildV [(Expr TyVar
v, Type
t)] = (Expr TyVar
v, Type
t)
              buildV [(Expr TyVar, Type)]
vs = let ([(Expr TyVar, Type)]
l, [(Expr TyVar, Type)]
r) = Int
-> [(Expr TyVar, Type)]
-> ([(Expr TyVar, Type)], [(Expr TyVar, Type)])
forall a. Int -> [a] -> ([a], [a])
splitAt ([(Expr TyVar, Type)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Expr TyVar, Type)]
vs Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2) [(Expr TyVar, Type)]
vs
                              (Expr TyVar
lv, Type
lt) = [(Expr TyVar, Type)] -> (Expr TyVar, Type)
buildV [(Expr TyVar, Type)]
l ; (Expr TyVar
rv, Type
rt) = [(Expr TyVar, Type)] -> (Expr TyVar, Type)
buildV [(Expr TyVar, Type)]
r
                          in ( DataCon -> [Expr TyVar] -> Expr TyVar
mkCoreConApps DataCon
prodDc [Type -> Expr TyVar
forall b. Type -> Expr b
Type Type
kTy, Type -> Expr TyVar
forall b. Type -> Expr b
Type Type
lt, Type -> Expr TyVar
forall b. Type -> Expr b
Type Type
rt, Type -> Expr TyVar
forall b. Type -> Expr b
Type Type
aTy, Expr TyVar
lv, Expr TyVar
rv]
                             , Type -> Type -> Type
prodTy Type
lt Type
rt )
              prodValOf [(Type, Expr b -> Expr TyVar, c, d)]
con [TyVar]
fis
                | [(Type, Expr b -> Expr TyVar, c, d)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Type, Expr b -> Expr TyVar, c, d)]
con  = DataCon -> [Expr TyVar] -> Expr TyVar
mkCoreConApps DataCon
u1Dc [Type -> Expr TyVar
forall b. Type -> Expr b
Type Type
kTy, Type -> Expr TyVar
forall b. Type -> Expr b
Type Type
aTy]
                | Bool
otherwise = (Expr TyVar, Type) -> Expr TyVar
forall a b. (a, b) -> a
fst ([(Expr TyVar, Type)] -> (Expr TyVar, Type)
buildV [ (Expr b -> Expr TyVar
wrap (TyVar -> Expr b
forall b. TyVar -> Expr b
Var TyVar
fi), Type
lt) | ((Type
lt, Expr b -> Expr TyVar
wrap, c
_, d
_), TyVar
fi) <- [(Type, Expr b -> Expr TyVar, c, d)]
-> [TyVar] -> [((Type, Expr b -> Expr TyVar, c, d), TyVar)]
forall a b. [a] -> [b] -> [(a, b)]
zip [(Type, Expr b -> Expr TyVar, c, d)]
con [TyVar]
fis ])
              -- balanced :+: injectors, by the bare struct types
              injectors [[(Type, b, c, d)]
con] = ([Expr TyVar -> Expr TyVar
forall a. a -> a
id], [(Type, b, c, d)] -> Type
forall {b} {c} {d}. [(Type, b, c, d)] -> Type
bareCon [(Type, b, c, d)]
con)
              injectors [[(Type, b, c, d)]]
cs =
                let ([[(Type, b, c, d)]]
l, [[(Type, b, c, d)]]
r) = Int
-> [[(Type, b, c, d)]]
-> ([[(Type, b, c, d)]], [[(Type, b, c, d)]])
forall a. Int -> [a] -> ([a], [a])
splitAt ([[(Type, b, c, d)]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[(Type, b, c, d)]]
cs Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2) [[(Type, b, c, d)]]
cs
                    ([Expr TyVar -> Expr TyVar]
li, Type
lt) = [[(Type, b, c, d)]] -> ([Expr TyVar -> Expr TyVar], Type)
injectors [[(Type, b, c, d)]]
l ; ([Expr TyVar -> Expr TyVar]
ri, Type
rt) = [[(Type, b, c, d)]] -> ([Expr TyVar -> Expr TyVar], Type)
injectors [[(Type, b, c, d)]]
r
                    wrapL :: Expr TyVar -> Expr TyVar
wrapL Expr TyVar
v = DataCon -> [Expr TyVar] -> Expr TyVar
mkCoreConApps DataCon
l1Dc [Type -> Expr TyVar
forall b. Type -> Expr b
Type Type
kTy, Type -> Expr TyVar
forall b. Type -> Expr b
Type Type
lt, Type -> Expr TyVar
forall b. Type -> Expr b
Type Type
rt, Type -> Expr TyVar
forall b. Type -> Expr b
Type Type
aTy, Expr TyVar
v]
                    wrapR :: Expr TyVar -> Expr TyVar
wrapR Expr TyVar
v = DataCon -> [Expr TyVar] -> Expr TyVar
mkCoreConApps DataCon
r1Dc [Type -> Expr TyVar
forall b. Type -> Expr b
Type Type
kTy, Type -> Expr TyVar
forall b. Type -> Expr b
Type Type
lt, Type -> Expr TyVar
forall b. Type -> Expr b
Type Type
rt, Type -> Expr TyVar
forall b. Type -> Expr b
Type Type
aTy, Expr TyVar
v]
                in (((Expr TyVar -> Expr TyVar) -> Expr TyVar -> Expr TyVar)
-> [Expr TyVar -> Expr TyVar] -> [Expr TyVar -> Expr TyVar]
forall a b. (a -> b) -> [a] -> [b]
map (Expr TyVar -> Expr TyVar
wrapL (Expr TyVar -> Expr TyVar)
-> (Expr TyVar -> Expr TyVar) -> Expr TyVar -> Expr TyVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) [Expr TyVar -> Expr TyVar]
li [Expr TyVar -> Expr TyVar]
-> [Expr TyVar -> Expr TyVar] -> [Expr TyVar -> Expr TyVar]
forall a. [a] -> [a] -> [a]
++ ((Expr TyVar -> Expr TyVar) -> Expr TyVar -> Expr TyVar)
-> [Expr TyVar -> Expr TyVar] -> [Expr TyVar -> Expr TyVar]
forall a b. (a -> b) -> [a] -> [b]
map (Expr TyVar -> Expr TyVar
wrapR (Expr TyVar -> Expr TyVar)
-> (Expr TyVar -> Expr TyVar) -> Expr TyVar -> Expr TyVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) [Expr TyVar -> Expr TyVar]
ri, Type -> Type -> Type
sumTy Type
lt Type
rt)
              (injs, _) = injectors classified

          vId <- freshId (mkAppTy wrappedTy aTy) "v"
          cbV <- freshId innerA "cb"
          fromAlts <- forM (zip3 dcons classified injs) \(DataCon
dc, [(Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar, [Ct])]
con, Expr TyVar -> Expr TyVar
inj) -> do
            fis <- (Int -> Type -> TcPluginM TyVar)
-> [Int] -> [Type] -> TcPluginM [TyVar]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (\Int
n Type
ft -> Type -> String -> TcPluginM TyVar
freshId Type
ft (String
"f" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n)) [Int
0 :: Int ..] (DataCon -> [Type]
fieldsOf DataCon
dc)
            pure (Alt (DataAlt dc) fis (Cast (inj (prodValOf con fis)) castUp))
          let fromImpl = TyVar -> Expr TyVar -> Expr TyVar
forall b. b -> Expr b -> Expr b
Lam TyVar
atv (TyVar -> Expr TyVar -> Expr TyVar
forall b. b -> Expr b -> Expr b
Lam TyVar
vId
                           (Expr TyVar -> TyVar -> Type -> [Alt TyVar] -> Expr TyVar
forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Case (Expr TyVar -> Coercion -> Expr TyVar
forall b. Expr b -> Coercion -> Expr b
Cast (TyVar -> Expr TyVar
forall b. TyVar -> Expr b
Var TyVar
vId) (Type -> Coercion
coAt Type
aTy)) TyVar
cbV (Type -> Type -> Type
mkAppTy Type
lhs1 Type
aTy) [Alt TyVar]
fromAlts))

          rId <- freshId (mkAppTy lhs1 aTy) "r"
          let destruct Expr TyVar
scr [(Type
_, b
_, Expr TyVar -> a
unwrap, d
_)] = ([a], Expr TyVar -> Expr TyVar)
-> TcPluginM ([a], Expr TyVar -> Expr TyVar)
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Expr TyVar -> a
unwrap Expr TyVar
scr], Expr TyVar -> Expr TyVar
forall a. a -> a
id)
              destruct Expr TyVar
scr [(Type, b, Expr TyVar -> a, d)]
con = do
                let ([(Type, b, Expr TyVar -> a, d)]
lc, [(Type, b, Expr TyVar -> a, d)]
rc) = Int
-> [(Type, b, Expr TyVar -> a, d)]
-> ([(Type, b, Expr TyVar -> a, d)],
    [(Type, b, Expr TyVar -> a, d)])
forall a. Int -> [a] -> ([a], [a])
splitAt ([(Type, b, Expr TyVar -> a, d)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Type, b, Expr TyVar -> a, d)]
con Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2) [(Type, b, Expr TyVar -> a, d)]
con
                    lt :: Type
lt = [(Type, b, Expr TyVar -> a, d)] -> Type
forall {b} {c} {d}. [(Type, b, c, d)] -> Type
bareCon [(Type, b, Expr TyVar -> a, d)]
lc ; rt :: Type
rt = [(Type, b, Expr TyVar -> a, d)] -> Type
forall {b} {c} {d}. [(Type, b, c, d)] -> Type
bareCon [(Type, b, Expr TyVar -> a, d)]
rc
                lv <- Type -> String -> TcPluginM TyVar
freshId (Type -> Type -> Type
mkAppTy Type
lt Type
aTy) String
"l"
                rv <- freshId (mkAppTy rt aTy) "rr"
                cb <- freshId (mkAppTy (prodTy lt rt) aTy) "pc"
                (lfs, lw) <- destruct (Var lv) lc
                (rfs, rw) <- destruct (Var rv) rc
                pure (lfs ++ rfs, \Expr TyVar
body -> Expr TyVar -> TyVar -> Type -> [Alt TyVar] -> Expr TyVar
forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Case Expr TyVar
scr TyVar
cb (Type -> Type -> Type
mkAppTy Type
wrappedTy Type
aTy)
                        [AltCon -> [TyVar] -> Expr TyVar -> Alt TyVar
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt (DataCon -> AltCon
DataAlt DataCon
prodDc) [TyVar
lv, TyVar
rv] (Expr TyVar -> Expr TyVar
lw (Expr TyVar -> Expr TyVar
rw Expr TyVar
body))])
              rebuildCon Expr TyVar
scr [(Type, b, Expr TyVar -> Expr TyVar, d)]
con DataCon
dc
                | [(Type, b, Expr TyVar -> Expr TyVar, d)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Type, b, Expr TyVar -> Expr TyVar, d)]
con  = Expr TyVar -> TcPluginM (Expr TyVar)
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr TyVar -> Coercion -> Expr TyVar
forall b. Expr b -> Coercion -> Expr b
Cast (Type -> DataCon -> [Expr TyVar] -> Expr TyVar
conAppAt Type
innerA DataCon
dc []) (Coercion -> Coercion
mkSymCo (Type -> Coercion
coAt Type
aTy)))
                | Bool
otherwise = do (fields, wrap) <- Expr TyVar
-> [(Type, b, Expr TyVar -> Expr TyVar, d)]
-> TcPluginM ([Expr TyVar], Expr TyVar -> Expr TyVar)
forall {b} {a} {d}.
Expr TyVar
-> [(Type, b, Expr TyVar -> a, d)]
-> TcPluginM ([a], Expr TyVar -> Expr TyVar)
destruct Expr TyVar
scr [(Type, b, Expr TyVar -> Expr TyVar, d)]
con
                                 pure (wrap (Cast (conAppAt innerA dc fields) (mkSymCo (coAt aTy))))
              destructSum Expr TyVar
scr [[(Type, b, Expr TyVar -> Expr TyVar, d)]
con] [DataCon
dc] = Expr TyVar
-> [(Type, b, Expr TyVar -> Expr TyVar, d)]
-> DataCon
-> TcPluginM (Expr TyVar)
forall {b} {d}.
Expr TyVar
-> [(Type, b, Expr TyVar -> Expr TyVar, d)]
-> DataCon
-> TcPluginM (Expr TyVar)
rebuildCon Expr TyVar
scr [(Type, b, Expr TyVar -> Expr TyVar, d)]
con DataCon
dc
              destructSum Expr TyVar
scr [[(Type, b, Expr TyVar -> Expr TyVar, d)]]
cs    [DataCon]
dcs  = do
                let h :: Int
h = [[(Type, b, Expr TyVar -> Expr TyVar, d)]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[(Type, b, Expr TyVar -> Expr TyVar, d)]]
cs Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2
                    ([[(Type, b, Expr TyVar -> Expr TyVar, d)]]
lc, [[(Type, b, Expr TyVar -> Expr TyVar, d)]]
rc) = Int
-> [[(Type, b, Expr TyVar -> Expr TyVar, d)]]
-> ([[(Type, b, Expr TyVar -> Expr TyVar, d)]],
    [[(Type, b, Expr TyVar -> Expr TyVar, d)]])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
h [[(Type, b, Expr TyVar -> Expr TyVar, d)]]
cs ; ([DataCon]
ldc, [DataCon]
rdc) = Int -> [DataCon] -> ([DataCon], [DataCon])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
h [DataCon]
dcs
                    lt :: Type
lt = case [[(Type, b, Expr TyVar -> Expr TyVar, d)]]
lc of { [[(Type, b, Expr TyVar -> Expr TyVar, d)]
c] -> [(Type, b, Expr TyVar -> Expr TyVar, d)] -> Type
forall {b} {c} {d}. [(Type, b, c, d)] -> Type
bareCon [(Type, b, Expr TyVar -> Expr TyVar, d)]
c; [[(Type, b, Expr TyVar -> Expr TyVar, d)]]
_ -> (Type -> Type -> Type) -> [Type] -> Type
forall a. (a -> a -> a) -> [a] -> a
foldBal Type -> Type -> Type
sumTy (([(Type, b, Expr TyVar -> Expr TyVar, d)] -> Type)
-> [[(Type, b, Expr TyVar -> Expr TyVar, d)]] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map [(Type, b, Expr TyVar -> Expr TyVar, d)] -> Type
forall {b} {c} {d}. [(Type, b, c, d)] -> Type
bareCon [[(Type, b, Expr TyVar -> Expr TyVar, d)]]
lc) }
                    rt :: Type
rt = case [[(Type, b, Expr TyVar -> Expr TyVar, d)]]
rc of { [[(Type, b, Expr TyVar -> Expr TyVar, d)]
c] -> [(Type, b, Expr TyVar -> Expr TyVar, d)] -> Type
forall {b} {c} {d}. [(Type, b, c, d)] -> Type
bareCon [(Type, b, Expr TyVar -> Expr TyVar, d)]
c; [[(Type, b, Expr TyVar -> Expr TyVar, d)]]
_ -> (Type -> Type -> Type) -> [Type] -> Type
forall a. (a -> a -> a) -> [a] -> a
foldBal Type -> Type -> Type
sumTy (([(Type, b, Expr TyVar -> Expr TyVar, d)] -> Type)
-> [[(Type, b, Expr TyVar -> Expr TyVar, d)]] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map [(Type, b, Expr TyVar -> Expr TyVar, d)] -> Type
forall {b} {c} {d}. [(Type, b, c, d)] -> Type
bareCon [[(Type, b, Expr TyVar -> Expr TyVar, d)]]
rc) }
                lv <- Type -> String -> TcPluginM TyVar
freshId (Type -> Type -> Type
mkAppTy Type
lt Type
aTy) String
"sl"
                rv <- freshId (mkAppTy rt aTy) "sr"
                cb <- freshId (mkAppTy (sumTy lt rt) aTy) "sc"
                lb <- destructSum (Var lv) lc ldc
                rb <- destructSum (Var rv) rc rdc
                pure (Case scr cb (mkAppTy wrappedTy aTy)
                        [Alt (DataAlt l1Dc) [lv] lb, Alt (DataAlt r1Dc) [rv] rb])
          toBody <- destructSum (Cast (Var rId) castDn) classified dcons
          let toImpl = TyVar -> Expr TyVar -> Expr TyVar
forall b. b -> Expr b -> Expr b
Lam TyVar
atv (TyVar -> Expr TyVar -> Expr TyVar
forall b. b -> Expr b -> Expr b
Lam TyVar
rId Expr TyVar
toBody)
              -- Generic1 is poly-kinded: its dictionary constructor takes the
              -- kind argument before the type argument.
              dict = Expr TyVar -> [Expr TyVar] -> Expr TyVar
forall b. Expr b -> [Expr b] -> Expr b
mkApps (TyVar -> Expr TyVar
forall b. TyVar -> Expr b
Var (DataCon -> TyVar
dataConWorkId (Class -> DataCon
classDataCon Class
cls)))
                       [Type -> Expr TyVar
forall b. Type -> Expr b
Type Type
liftedTypeKind, Type -> Expr TyVar
forall b. Type -> Expr b
Type Type
wrappedTy, Expr TyVar
fromImpl, Expr TyVar
toImpl]
          pure (Just (EvExpr dict, fieldWanteds))
    (Maybe TyCon, 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
  where (Type
realF, Maybe [Type]
mMods) = GenEnv -> Type -> (Type, Maybe [Type])
peelOverride1 GenEnv
gen Type
f

-- | Variance of an occurrence of the type parameter.