| Safe Haskell | Ignore |
|---|---|
| Language | GHC2021 |
GHC.Core.Reduction
Synopsis
- data Reduction = Reduction {}
- type ReductionN = Reduction
- type ReductionR = Reduction
- data HetReduction = HetReduction Reduction MCoercionN
- data Reductions = Reductions [Coercion] [Type]
- mkReduction :: Coercion -> Type -> Reduction
- mkReductions :: [Coercion] -> [Type] -> Reductions
- mkHetReduction :: Reduction -> MCoercionN -> HetReduction
- coercionRedn :: Coercion -> Reduction
- reductionOriginalType :: Reduction -> Type
- downgradeRedn :: Role -> Role -> Reduction -> Reduction
- mkSubRedn :: Reduction -> Reduction
- mkTransRedn :: Coercion -> Reduction -> Reduction
- mkCoherenceRightRedn :: Role -> Reduction -> CoercionN -> Reduction
- mkCoherenceRightMRedn :: Role -> Reduction -> MCoercionN -> Reduction
- mkCastRedn1 :: Role -> Type -> CoercionN -> Reduction -> Reduction
- mkCastRedn2 :: Role -> Type -> CoercionN -> Reduction -> CoercionN -> Reduction
- mkReflRedn :: Role -> Type -> Reduction
- mkGReflRightRedn :: Role -> Type -> CoercionN -> Reduction
- mkGReflRightMRedn :: Role -> Type -> MCoercionN -> Reduction
- mkGReflLeftRedn :: Role -> Type -> CoercionN -> Reduction
- mkGReflLeftMRedn :: Role -> Type -> MCoercionN -> Reduction
- mkAppRedn :: Reduction -> Reduction -> Reduction
- mkAppRedns :: Reduction -> Reductions -> Reduction
- mkFunRedn :: Role -> FunTyFlag -> ReductionN -> Reduction -> Reduction -> Reduction
- mkForAllRedn :: ForAllTyFlag -> TyVar -> ReductionN -> Reduction -> Reduction
- mkHomoForAllRedn :: [TyVarBinder] -> Reduction -> Reduction
- mkTyConAppRedn :: Role -> TyCon -> Reductions -> Reduction
- mkClassPredRedn :: Class -> Reductions -> Reduction
- mkProofIrrelRedn :: Role -> CoercionN -> Coercion -> Coercion -> Reduction
- mkReflCoRedn :: Role -> Coercion -> Reduction
- homogeniseHetRedn :: Role -> HetReduction -> Reduction
- unzipRedns :: [Reduction] -> Reductions
- data ArgsReductions = ArgsReductions !Reductions !MCoercionN
- simplifyArgsWorker :: HasDebugCallStack => [PiTyBinder] -> Kind -> TyCoVarSet -> Infinite Role -> [Reduction] -> ArgsReductions
Reductions
A Reduction is the result of an operation that rewrites a type ty_in.
The Reduction includes the rewritten type ty_out and a Coercion co
such that co :: ty_in ~ ty_out, where the role of the coercion is determined
by the context. That is, the LHS type of the coercion is the original type
ty_in, while its RHS type is the rewritten type ty_out.
A Reduction is always homogeneous, unless it is wrapped inside a HetReduction,
which separately stores the kind coercion.
See Note [The Reduction type].
Constructors
| Reduction | |
Fields | |
Instances
type ReductionR = Reduction Source #
A Reduction in which the Coercion has Representational role.
data HetReduction Source #
Stores a heterogeneous reduction.
The stored kind coercion must relate the kinds of the
stored reduction. That is, in HetReduction (Reduction co xi) kco,
we must have:
co :: ty ~ xi kco :: typeKind ty ~ typeKind xi
Constructors
| HetReduction Reduction MCoercionN |
data Reductions Source #
A collection of Reductions where the coercions and the types are stored separately.
Use unzipRedns to obtain Reductions from a list of Reductions.
This datatype is used in mkAppRedns, mkClassPredRedns and mkTyConAppRedn,
which expect separate types and coercions.
Invariant: the two stored lists are of the same length, and the RHS type of each coercion is the corresponding type.
Constructors
| Reductions [Coercion] [Type] |
Stores a heterogeneous reduction.
The stored kind coercion must relate the kinds of the
stored reduction. That is, in This funa href="#v:cla funa">ant: the two stored lists are of the same length,
orm">Platforrd">forall data CoAxBranch p k) xs
Note: if p is not actually antitone, then spanAntitone will split the map
at some unspecified point.N -&geFlagsunsafeFlagsForInfergetOpts getVerbFlags
setOutputFilesetDynOutputFile setOutputHisetDynOutputHiaddPluginModuleName updOptLevelparseDynamicFlagsCmdLineparseDynashould_fail(T16326_Fail3
unsafeFlagsForInfergetOpts getVerbFlags
setOutputFilesetDynOutputFile setOutputHisetDynOutputHiaynOutputHiaynOutputHiaynOutputHiaynOutputHiaynOutputHiaynOutputHiaynOutputHiaynOutputHiaynOutputHi -> HetReduction (Reduction