{-# 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
      DataCon -> Type
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 :: Type
struct = GenEnv -> (DataCon -> Type) -> Type -> [(DataCon, [Type])] -> Type
repMetaFts GenEnv
gen DataCon -> Type
fixOf Type
realInner [(DataCon, [Type])]
cons
          lhs :: Type
lhs    = TyCon -> [Type] -> Type
mkTyConApp (GenEnv -> TyCon
geRepTc GenEnv
gen) [Type
arg]
          co :: Coercion
co     = UnivCoProvenance -> Role -> Type -> Type -> Coercion
mkStockCo (String -> UnivCoProvenance
PluginProv String
"stock") Role
Nominal Type
lhs Type
struct
      TcPluginRewriteResult -> TcPluginM TcPluginRewriteResult
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Reduction -> [Ct] -> TcPluginRewriteResult
TcPluginRewriteTo (Coercion -> Type -> Reduction
mkReduction Coercion
co Type
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
      DataCon -> Type
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 :: Type
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 :: Type
lhs    = TyCon -> [Type] -> Type
mkTyConApp (GenEnv -> TyCon
geRepTc GenEnv
gen) [Type
arg]
          co :: Coercion
co     = UnivCoProvenance -> Role -> Type -> Type -> Coercion
mkStockCo (String -> UnivCoProvenance
PluginProv String
"stock") Role
Nominal Type
lhs Type
struct
      TcPluginRewriteResult -> TcPluginM TcPluginRewriteResult
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Reduction -> [Ct] -> TcPluginRewriteResult
TcPluginRewriteTo (Coercion -> Type -> Reduction
mkReduction Coercion
co Type
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]
_) <- HasDebugCallStack => 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
      TyVar
a0 <- String -> TcPluginM TyVar
freshTyVar String
"a"
      let aT0 :: Type
aT0   = TyVar -> Type
mkTyVarTy TyVar
a0
          fixed :: [Type]
fixed = HasDebugCallStack => Type -> [Type]
Type -> [Type]
tyConAppArgs Type
realF
          dcons :: [DataCon]
dcons = TyCon -> [DataCon]
tyConDataCons TyCon
fTc
          innerF :: Type
innerF = TyCon -> [Type] -> Type
mkTyConApp TyCon
fTc ([Type]
fixed [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type
aT0])
          ftysOf :: DataCon -> [Type]
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 :: Bool
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 Bool -> Bool
not Bool
ok then TcPluginRewriteResult -> TcPluginM TcPluginRewriteResult
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TcPluginRewriteResult
TcPluginNoRewrite else do
        DataCon -> Type
fixOf <- MetaEnv -> [DataCon] -> TcPluginM (DataCon -> Type)
mkFixOf (GenEnv -> MetaEnv
geMeta GenEnv
gen) [DataCon]
dcons
        let struct :: Type
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 :: Type
lhs    = TyCon -> [Type] -> Type
mkTyConApp (Gen1Env -> TyCon
g1RepTc (GenEnv -> Gen1Env
geGen1 GenEnv
gen)) [Type]
args
            co :: Coercion
co     = UnivCoProvenance -> Role -> Type -> Type -> Coercion
mkStockCo (String -> UnivCoProvenance
PluginProv String
"stock") Role
Nominal Type
lhs Type
struct
        TcPluginRewriteResult -> TcPluginM TcPluginRewriteResult
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Reduction -> [Ct] -> TcPluginRewriteResult
TcPluginRewriteTo (Coercion -> Type -> Reduction
mkReduction Coercion
co Type
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
  DataCon -> Type
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 :: Class
genCls = GenEnv -> Class
geGen GenEnv
gen
      k1Tc :: TyCon
k1Tc   = GenEnv -> TyCon
geK1Tc GenEnv
gen
      prodTc :: TyCon
prodTc = GenEnv -> TyCon
geProdTc GenEnv
gen ; prodDc :: DataCon
prodDc = GenEnv -> DataCon
geProdDc GenEnv
gen
      sumTc :: TyCon
sumTc  = GenEnv -> TyCon
geSumTc GenEnv
gen
      [DataCon
l1Dc, DataCon
r1Dc] = TyCon -> [DataCon]
tyConDataCons TyCon
sumTc
      u1Dc :: DataCon
u1Dc   = [DataCon] -> DataCon
forall a. HasCallStack => [a] -> a
head (TyCon -> [DataCon]
tyConDataCons (GenEnv -> TyCon
geU1Tc GenEnv
gen))
      rTy :: Type
rTy    = GenEnv -> Type
geRTy GenEnv
gen
      kTy :: Type
kTy    = Type
liftedTypeKind
      dcons :: [DataCon]
dcons    = (ConInfo -> DataCon) -> [ConInfo] -> [DataCon]
forall a b. (a -> b) -> [a] -> [b]
map ConInfo -> DataCon
ciCon [ConInfo]
cons
      modFtss :: [[Type]]
modFtss  = (ConInfo -> [Type]) -> [ConInfo] -> [[Type]]
forall a b. (a -> b) -> [a] -> [b]
map ConInfo -> [Type]
ciFields [ConInfo]
cons                    -- Rep leaves (modifier types)
      cosss :: [[Coercion]]
cosss    = (ConInfo -> [Coercion]) -> [ConInfo] -> [[Coercion]]
forall a b. (a -> b) -> [a] -> [b]
map ConInfo -> [Coercion]
ciFieldCos [ConInfo]
cons                  -- realFt ~R modFt per field
      realFtss :: [[Type]]
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)]]
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 :: Type
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 :: Type
structBare = GenEnv -> [[Type]] -> Type
repData GenEnv
gen [[Type]]
modFtss                          -- the un-M1 value structure
      lhs :: Type
lhs    = TyCon -> [Type] -> Type
mkTyConApp (GenEnv -> TyCon
geRepTc GenEnv
gen) [Type
wrappedTy]
      coRep :: Coercion
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 :: Coercion
coStrip = UnivCoProvenance -> Role -> Type -> Type -> Coercion
mkStockCo (String -> UnivCoProvenance
PluginProv String
"stock") Role
Representational Type
structMeta Type
structBare

  Unique
ux <- TcM Unique -> TcPluginM Unique
forall a. TcM a -> TcPluginM a
unsafeTcPluginTcM TcM Unique
forall (m :: * -> *). MonadUnique m => m Unique
getUniqueM
  let xtv :: TyVar
xtv = Name -> Type -> TyVar
mkTyVar (Unique -> OccName -> Name
mkSystemName Unique
ux (String -> OccName
mkTyVarOcc String
"x")) Type
liftedTypeKind
      xty :: Type
xty = TyVar -> Type
mkTyVarTy TyVar
xtv
      prodTy :: Type -> Type -> Type
prodTy Type
f Type
g = TyCon -> [Type] -> Type
mkTyConApp TyCon
prodTc [Type
kTy, Type
f, Type
g]
      sumTy :: Type -> Type -> Type
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 :: Coercion
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
castUp = Coercion -> Coercion
mkSymCo Coercion
castDn                                        -- structBare x ~R Rep x
      k1Co :: Type -> Coercion
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 -> Type -> TyVar -> Expr TyVar
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 -> Type -> Expr TyVar -> Expr TyVar
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, Type)] -> (Expr TyVar, Type)
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)] -> [TyVar] -> Expr TyVar
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]] -> ([Expr TyVar -> Expr TyVar], 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]
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]
ri, Type -> Type -> Type
sumTy Type
lt Type
rt)
      ([Expr TyVar -> Expr TyVar]
injs, Type
_) = [[Type]] -> ([Expr TyVar -> Expr TyVar], Type)
injectors [[Type]]
modFtss

  -- from = /\x. \v -> case (v |> co) of  Cᵢ f.. -> injᵢ <product> |> castUp
  TyVar
vId <- Type -> String -> TcPluginM TyVar
freshId Type
wrappedTy String
"v"
  TyVar
cbV <- Type -> String -> TcPluginM TyVar
freshId Type
innerTy String
"cb"
  [Alt TyVar]
fromAlts <- [(DataCon, ([Type], [(Type, Coercion)], Expr TyVar -> Expr TyVar))]
-> ((DataCon,
     ([Type], [(Type, Coercion)], Expr TyVar -> Expr TyVar))
    -> TcPluginM (Alt TyVar))
-> TcPluginM [Alt TyVar]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ([DataCon]
-> [([Type], [(Type, Coercion)], Expr TyVar -> Expr TyVar)]
-> [(DataCon,
     ([Type], [(Type, Coercion)], Expr TyVar -> Expr TyVar))]
forall a b. [a] -> [b] -> [(a, b)]
zip [DataCon]
dcons ([[Type]]
-> [[(Type, Coercion)]]
-> [Expr TyVar -> Expr TyVar]
-> [([Type], [(Type, Coercion)], Expr TyVar -> Expr TyVar)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [[Type]]
realFtss [[(Type, Coercion)]]
mfcss [Expr TyVar -> Expr TyVar]
injs)) \(DataCon
dc, ([Type]
realFts, [(Type, Coercion)]
mfcs, Expr TyVar -> Expr TyVar
inj)) -> do
    [TyVar]
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
    Alt TyVar -> TcPluginM (Alt TyVar)
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AltCon -> [TyVar] -> Expr TyVar -> Alt TyVar
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt (DataCon -> AltCon
DataAlt DataCon
dc) [TyVar]
fis (Expr TyVar -> Coercion -> Expr TyVar
forall b. Expr b -> Coercion -> Expr b
Cast (Expr TyVar -> Expr TyVar
inj ([(Type, Coercion)] -> [TyVar] -> Expr TyVar
prodValOf [(Type, Coercion)]
mfcs [TyVar]
fis)) Coercion
castUp))
  let fromImpl :: Expr TyVar
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ᵢ>
  TyVar
rId <- Type -> String -> TcPluginM TyVar
freshId (Type -> Type -> Type
mkAppTy Type
lhs Type
xty) String
"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
-> [(Type, Coercion)]
-> TcPluginM ([Expr TyVar], Expr TyVar -> Expr TyVar)
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)
        TyVar
lv <- Type -> String -> TcPluginM TyVar
freshId (Type -> Type -> Type
mkAppTy Type
lt Type
xty) String
"l"
        TyVar
rv <- Type -> String -> TcPluginM TyVar
freshId (Type -> Type -> Type
mkAppTy Type
rt Type
xty) String
"rr"
        TyVar
cb <- Type -> String -> TcPluginM TyVar
freshId (Type -> Type -> Type
mkAppTy (Type -> Type -> Type
prodTy Type
lt Type
rt) Type
xty) String
"pc"
        ([Expr TyVar]
lfs, Expr TyVar -> Expr TyVar
lwrap) <- Expr TyVar
-> [(Type, Coercion)]
-> TcPluginM ([Expr TyVar], Expr TyVar -> Expr TyVar)
destruct (TyVar -> Expr TyVar
forall b. TyVar -> Expr b
Var TyVar
lv) [(Type, Coercion)]
lT
        ([Expr TyVar]
rfs, Expr TyVar -> Expr TyVar
rwrap) <- Expr TyVar
-> [(Type, Coercion)]
-> TcPluginM ([Expr TyVar], Expr TyVar -> Expr TyVar)
destruct (TyVar -> Expr TyVar
forall b. TyVar -> Expr b
Var TyVar
rv) [(Type, Coercion)]
rT
        let wrap :: Expr TyVar -> Expr TyVar
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))]
        ([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 ([Expr TyVar]
lfs [Expr TyVar] -> [Expr TyVar] -> [Expr TyVar]
forall a. [a] -> [a] -> [a]
++ [Expr TyVar]
rfs, Expr TyVar -> Expr TyVar
wrap)
      -- rebuild one constructor from its product struct
      rebuildCon :: Expr TyVar
-> [(Type, Coercion)] -> DataCon -> TcPluginM (Expr TyVar)
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 ([Expr TyVar]
fields, Expr TyVar -> Expr TyVar
wrap) <- Expr TyVar
-> [(Type, Coercion)]
-> TcPluginM ([Expr TyVar], Expr TyVar -> Expr TyVar)
destruct Expr TyVar
scr [(Type, Coercion)]
mfs
                         Expr TyVar -> TcPluginM (Expr TyVar)
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr TyVar -> Expr TyVar
wrap (Expr TyVar -> Coercion -> Expr TyVar
forall b. Expr b -> Coercion -> Expr b
Cast (Type -> DataCon -> [Expr TyVar] -> Expr TyVar
conAppAt Type
innerTy DataCon
dc [Expr TyVar]
fields) (Coercion -> Coercion
mkSymCo Coercion
co)))
      -- project through the balanced :+: tree, rebuilding at each leaf
      destructSum :: Expr TyVar
-> [[(Type, Coercion)]] -> [DataCon] -> TcPluginM (Expr TyVar)
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)
        TyVar
lv <- Type -> String -> TcPluginM TyVar
freshId (Type -> Type -> Type
mkAppTy Type
lt Type
xty) String
"sl"
        TyVar
rv <- Type -> String -> TcPluginM TyVar
freshId (Type -> Type -> Type
mkAppTy Type
rt Type
xty) String
"sr"
        TyVar
cb <- Type -> String -> TcPluginM TyVar
freshId (Type -> Type -> Type
mkAppTy (Type -> Type -> Type
sumTy Type
lt Type
rt) Type
xty) String
"sc"
        Expr TyVar
lbody <- Expr TyVar
-> [[(Type, Coercion)]] -> [DataCon] -> TcPluginM (Expr TyVar)
destructSum (TyVar -> Expr TyVar
forall b. TyVar -> Expr b
Var TyVar
lv) [[(Type, Coercion)]]
lfs [DataCon]
ldc
        Expr TyVar
rbody <- Expr TyVar
-> [[(Type, Coercion)]] -> [DataCon] -> TcPluginM (Expr TyVar)
destructSum (TyVar -> Expr TyVar
forall b. TyVar -> Expr b
Var TyVar
rv) [[(Type, Coercion)]]
rfs [DataCon]
rdc
        Expr TyVar -> TcPluginM (Expr TyVar)
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (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
l1Dc) [TyVar
lv] Expr TyVar
lbody, AltCon -> [TyVar] -> Expr TyVar -> Alt TyVar
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt (DataCon -> AltCon
DataAlt DataCon
r1Dc) [TyVar
rv] Expr TyVar
rbody ])
  Expr TyVar
toBody <- Expr TyVar
-> [[(Type, Coercion)]] -> [DataCon] -> TcPluginM (Expr TyVar)
destructSum (Expr TyVar -> Coercion -> Expr TyVar
forall b. Expr b -> Coercion -> Expr b
Cast (TyVar -> Expr TyVar
forall b. TyVar -> Expr b
Var TyVar
rId) Coercion
castDn) [[(Type, Coercion)]]
mfcss [DataCon]
dcons
  let toImpl :: Expr TyVar
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)

  EvTerm -> TcPluginM EvTerm
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (EvTerm -> TcPluginM EvTerm) -> EvTerm -> TcPluginM EvTerm
forall a b. (a -> b) -> a -> b
$ Expr TyVar -> EvTerm
EvExpr (Expr TyVar -> EvTerm) -> Expr TyVar -> EvTerm
forall a b. (a -> b) -> a -> b
$ Class -> Type -> [Expr TyVar] -> Expr TyVar
mkClassDict Class
genCls Type
wrappedTy [Expr TyVar
fromImpl, Expr TyVar
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
      Class
functorCls <- Name -> TcPluginM Class
tcLookupClass Name
functorClassName
      let g1 :: Gen1Env
g1     = GenEnv -> Gen1Env
geGen1 GenEnv
gen
          fixed :: [Type]
fixed  = HasDebugCallStack => Type -> [Type]
Type -> [Type]
tyConAppArgs Type
realF
          dcons :: [DataCon]
dcons  = TyCon -> [DataCon]
tyConDataCons TyCon
fTc
          k1Tc :: TyCon
k1Tc   = GenEnv -> TyCon
geK1Tc GenEnv
gen ; rTy :: Type
rTy = GenEnv -> Type
geRTy GenEnv
gen ; kTy :: Type
kTy = Type
liftedTypeKind
          par1Tc :: TyCon
par1Tc = Gen1Env -> TyCon
g1Par1Tc Gen1Env
g1 ; rec1Tc :: TyCon
rec1Tc = Gen1Env -> TyCon
g1Rec1Tc Gen1Env
g1 ; compTc :: TyCon
compTc = Gen1Env -> TyCon
g1CompTc Gen1Env
g1
          fmapSel :: TyVar
fmapSel = String -> Class -> TyVar
classMethod String
"fmap" Class
functorCls
          prodTc :: TyCon
prodTc = GenEnv -> TyCon
geProdTc GenEnv
gen ; prodDc :: DataCon
prodDc = GenEnv -> DataCon
geProdDc GenEnv
gen
          sumTc :: TyCon
sumTc  = GenEnv -> TyCon
geSumTc GenEnv
gen ; [DataCon
l1Dc, DataCon
r1Dc] = TyCon -> [DataCon]
tyConDataCons TyCon
sumTc
          u1Dc :: DataCon
u1Dc   = [DataCon] -> DataCon
forall a. HasCallStack => [a] -> a
head (TyCon -> [DataCon]
tyConDataCons (GenEnv -> TyCon
geU1Tc GenEnv
gen))
          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
      TyVar
atv <- String -> TcPluginM TyVar
freshTyVar String
"a"
      let aTy :: Type
aTy    = TyVar -> Type
mkTyVarTy TyVar
atv
          innerA :: Type
innerA = TyCon -> [Type] -> Type
mkTyConApp TyCon
fTc ([Type]
fixed [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type
aTy])
          prodTy :: Type -> Type -> Type
prodTy Type
a Type
b = TyCon -> [Type] -> Type
mkTyConApp TyCon
prodTc [Type
kTy, Type
a, Type
b]
          sumTy :: Type -> Type -> Type
sumTy  Type
a Type
b = TyCon -> [Type] -> Type
mkTyConApp TyCon
sumTc  [Type
kTy, Type
a, Type
b]
          u1Ty :: Type
u1Ty   = TyCon -> [Type] -> Type
mkTyConApp (GenEnv -> TyCon
geU1Tc GenEnv
gen) [Type
kTy]
          par1Co :: Coercion
par1Co   = Role -> CoAxiom Unbranched -> [Type] -> [Coercion] -> Coercion
mkUnbranchedAxInstCo Role
Representational (TyCon -> CoAxiom Unbranched
newTyConCo TyCon
par1Tc) [Type
aTy] []
          rec1Co :: Type -> Coercion
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 -> Coercion
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 -> [Type]
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
-> Type
-> TcPluginM
     (Maybe
        (Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar, [Ct]))
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
                    Maybe
  (Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar, [Ct])
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 Maybe
  (Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar, [Ct])
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
                        CtEvidence
ev  <- CtLoc -> Type -> TcPluginM CtEvidence
newWanted CtLoc
loc (Class -> [Type] -> Type
mkClassPred Class
functorCls [Type
h])
                        TyVar
yId <- Type -> String -> TcPluginM TyVar
freshId Type
larg String
"y"
                        TyVar
zId <- Type -> String -> TcPluginM TyVar
freshId (Type -> Type -> Type
mkAppTy Type
innerRep Type
aTy) String
"z"
                        let dict :: Expr TyVar
dict      = HasDebugCallStack => CtEvidence -> Expr TyVar
CtEvidence -> Expr TyVar
ctEvExpr CtEvidence
ev
                            compTy :: Type
compTy    = TyCon -> [Type] -> Type
mkTyConApp TyCon
compTc [Type
kTy, Type
kTy, Type
h, Type
innerRep]
                            comp1Co :: Coercion
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
innerAppA = Type -> Type -> Type
mkAppTy Type
innerRep Type
aTy
                            fmapAt :: Type -> Type -> Expr TyVar -> Expr TyVar -> Expr TyVar
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 -> Expr TyVar
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 -> Expr TyVar
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)
                        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 (Type
compTy, Expr TyVar -> Expr TyVar
wrapE, Expr TyVar -> Expr TyVar
unwrapE, CtEvidence -> Ct
mkNonCanonical CtEvidence
ev Ct -> [Ct] -> [Ct]
forall a. a -> [a] -> [a]
: [Ct]
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
      [[Maybe
    (Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar, [Ct])]]
classifiedM <- [DataCon]
-> (DataCon
    -> TcPluginM
         [Maybe
            (Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar, [Ct])])
-> TcPluginM
     [[Maybe
         (Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar, [Ct])]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [DataCon]
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 ([Maybe
    (Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar, [Ct])]
 -> Maybe
      [(Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar, [Ct])])
-> [[Maybe
       (Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar, [Ct])]]
-> Maybe
     [[(Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar,
        [Ct])]]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse [Maybe
   (Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar, [Ct])]
-> Maybe
     [(Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar, [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
    (Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar, [Ct])]]
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
          DataCon -> Type
fixOf <- MetaEnv -> [DataCon] -> TcPluginM (DataCon -> Type)
mkFixOf (GenEnv -> MetaEnv
geMeta GenEnv
gen) [DataCon]
dcons
          let fieldWanteds :: [Ct]
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)] -> [a]
leafTys [(a, b, c, d)]
con = [ a
lt | (a
lt, b
_, c
_, d
_) <- [(a, b, c, d)]
con ]
              bareCon :: [(Type, b, c, d)] -> Type
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 :: Type
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 :: Type
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 :: Type
lhs1   = TyCon -> [Type] -> Type
mkTyConApp (Gen1Env -> TyCon
g1RepTc Gen1Env
g1) [Type
liftedTypeKind, Type
wrappedTy]
              coRep :: Coercion
coRep  = UnivCoProvenance -> Role -> Type -> Type -> Coercion
mkStockCo (String -> UnivCoProvenance
PluginProv String
"stock") Role
Nominal Type
lhs1 Type
structMeta
              coStrip :: Coercion
coStrip = UnivCoProvenance -> Role -> Type -> Type -> Coercion
mkStockCo (String -> UnivCoProvenance
PluginProv String
"stock") Role
Representational Type
structMeta Type
structBare
              castDn :: Coercion
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
castUp = Coercion -> Coercion
mkSymCo Coercion
castDn
              -- balanced :*: VALUE for one constructor (over the leaf values/types)
              buildV :: [(Expr TyVar, Type)] -> (Expr TyVar, Type)
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)] -> [TyVar] -> Expr TyVar
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)]] -> ([Expr TyVar -> Expr TyVar], Type)
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]
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]
ri, Type -> Type -> Type
sumTy Type
lt Type
rt)
              ([Expr TyVar -> Expr TyVar]
injs, Type
_) = [[(Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar,
   [Ct])]]
-> ([Expr TyVar -> Expr TyVar], Type)
forall {b} {c} {d}.
[[(Type, b, c, d)]] -> ([Expr TyVar -> Expr TyVar], Type)
injectors [[(Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar,
   [Ct])]]
classified

          TyVar
vId <- Type -> String -> TcPluginM TyVar
freshId (Type -> Type -> Type
mkAppTy Type
wrappedTy Type
aTy) String
"v"
          TyVar
cbV <- Type -> String -> TcPluginM TyVar
freshId Type
innerA String
"cb"
          [Alt TyVar]
fromAlts <- [(DataCon,
  [(Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar, [Ct])],
  Expr TyVar -> Expr TyVar)]
-> ((DataCon,
     [(Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar, [Ct])],
     Expr TyVar -> Expr TyVar)
    -> TcPluginM (Alt TyVar))
-> TcPluginM [Alt TyVar]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ([DataCon]
-> [[(Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar,
      [Ct])]]
-> [Expr TyVar -> Expr TyVar]
-> [(DataCon,
     [(Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar, [Ct])],
     Expr TyVar -> Expr TyVar)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [DataCon]
dcons [[(Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar,
   [Ct])]]
classified [Expr TyVar -> Expr TyVar]
injs) \(DataCon
dc, [(Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar, [Ct])]
con, Expr TyVar -> Expr TyVar
inj) -> do
            [TyVar]
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)
            Alt TyVar -> TcPluginM (Alt TyVar)
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AltCon -> [TyVar] -> Expr TyVar -> Alt TyVar
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt (DataCon -> AltCon
DataAlt DataCon
dc) [TyVar]
fis (Expr TyVar -> Coercion -> Expr TyVar
forall b. Expr b -> Coercion -> Expr b
Cast (Expr TyVar -> Expr TyVar
inj ([(Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar, [Ct])]
-> [TyVar] -> Expr TyVar
forall {b} {c} {d}.
[(Type, Expr b -> Expr TyVar, c, d)] -> [TyVar] -> Expr TyVar
prodValOf [(Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar, [Ct])]
con [TyVar]
fis)) Coercion
castUp))
          let fromImpl :: Expr TyVar
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))

          TyVar
rId <- Type -> String -> TcPluginM TyVar
freshId (Type -> Type -> Type
mkAppTy Type
lhs1 Type
aTy) String
"r"
          let destruct :: Expr TyVar
-> [(Type, b, Expr TyVar -> a, d)]
-> TcPluginM ([a], Expr TyVar -> Expr TyVar)
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
                TyVar
lv <- Type -> String -> TcPluginM TyVar
freshId (Type -> Type -> Type
mkAppTy Type
lt Type
aTy) String
"l"
                TyVar
rv <- Type -> String -> TcPluginM TyVar
freshId (Type -> Type -> Type
mkAppTy Type
rt Type
aTy) String
"rr"
                TyVar
cb <- Type -> String -> TcPluginM TyVar
freshId (Type -> Type -> Type
mkAppTy (Type -> Type -> Type
prodTy Type
lt Type
rt) Type
aTy) String
"pc"
                ([a]
lfs, Expr TyVar -> Expr TyVar
lw) <- Expr TyVar
-> [(Type, b, Expr TyVar -> a, d)]
-> TcPluginM ([a], Expr TyVar -> Expr TyVar)
destruct (TyVar -> Expr TyVar
forall b. TyVar -> Expr b
Var TyVar
lv) [(Type, b, Expr TyVar -> a, d)]
lc
                ([a]
rfs, Expr TyVar -> Expr TyVar
rw) <- Expr TyVar
-> [(Type, b, Expr TyVar -> a, d)]
-> TcPluginM ([a], Expr TyVar -> Expr TyVar)
destruct (TyVar -> Expr TyVar
forall b. TyVar -> Expr b
Var TyVar
rv) [(Type, b, Expr TyVar -> a, d)]
rc
                ([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 ([a]
lfs [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
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
-> [(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
                | [(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 ([Expr TyVar]
fields, Expr TyVar -> Expr TyVar
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
                                 Expr TyVar -> TcPluginM (Expr TyVar)
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr TyVar -> Expr TyVar
wrap (Expr TyVar -> Coercion -> Expr TyVar
forall b. Expr b -> Coercion -> Expr b
Cast (Type -> DataCon -> [Expr TyVar] -> Expr TyVar
conAppAt Type
innerA DataCon
dc [Expr TyVar]
fields) (Coercion -> Coercion
mkSymCo (Type -> Coercion
coAt Type
aTy))))
              destructSum :: Expr TyVar
-> [[(Type, b, Expr TyVar -> Expr TyVar, d)]]
-> [DataCon]
-> TcPluginM (Expr TyVar)
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) }
                TyVar
lv <- Type -> String -> TcPluginM TyVar
freshId (Type -> Type -> Type
mkAppTy Type
lt Type
aTy) String
"sl"
                TyVar
rv <- Type -> String -> TcPluginM TyVar
freshId (Type -> Type -> Type
mkAppTy Type
rt Type
aTy) String
"sr"
                TyVar
cb <- Type -> String -> TcPluginM TyVar
freshId (Type -> Type -> Type
mkAppTy (Type -> Type -> Type
sumTy Type
lt Type
rt) Type
aTy) String
"sc"
                Expr TyVar
lb <- Expr TyVar
-> [[(Type, b, Expr TyVar -> Expr TyVar, d)]]
-> [DataCon]
-> TcPluginM (Expr TyVar)
destructSum (TyVar -> Expr TyVar
forall b. TyVar -> Expr b
Var TyVar
lv) [[(Type, b, Expr TyVar -> Expr TyVar, d)]]
lc [DataCon]
ldc
                Expr TyVar
rb <- Expr TyVar
-> [[(Type, b, Expr TyVar -> Expr TyVar, d)]]
-> [DataCon]
-> TcPluginM (Expr TyVar)
destructSum (TyVar -> Expr TyVar
forall b. TyVar -> Expr b
Var TyVar
rv) [[(Type, b, Expr TyVar -> Expr TyVar, d)]]
rc [DataCon]
rdc
                Expr TyVar -> TcPluginM (Expr TyVar)
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (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
l1Dc) [TyVar
lv] Expr TyVar
lb, AltCon -> [TyVar] -> Expr TyVar -> Alt TyVar
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt (DataCon -> AltCon
DataAlt DataCon
r1Dc) [TyVar
rv] Expr TyVar
rb])
          Expr TyVar
toBody <- Expr TyVar
-> [[(Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar,
      [Ct])]]
-> [DataCon]
-> TcPluginM (Expr TyVar)
forall {b} {d}.
Expr TyVar
-> [[(Type, b, Expr TyVar -> Expr TyVar, d)]]
-> [DataCon]
-> TcPluginM (Expr TyVar)
destructSum (Expr TyVar -> Coercion -> Expr TyVar
forall b. Expr b -> Coercion -> Expr b
Cast (TyVar -> Expr TyVar
forall b. TyVar -> Expr b
Var TyVar
rId) Coercion
castDn) [[(Type, Expr TyVar -> Expr TyVar, Expr TyVar -> Expr TyVar,
   [Ct])]]
classified [DataCon]
dcons
          let toImpl :: Expr TyVar
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
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]
          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 TyVar -> EvTerm
EvExpr Expr TyVar
dict, [Ct]
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.