Type-changing: inlined type synonyms in type-annotations cause $\Gamma$ in the respective typing derivations to have $\delta$-equivalent types. This could be expressed as a type equality relation
\Delta^+ \vdash \tau =_\delta \sigma
where $\Delta^+$ is a kinding context, extended with type-let RHS information.
Refined notion of logical relation: The logical approximation we have used so far requires arbitrary substitutions $\gamma, \gamma' \in [\Gamma^+]$, but we will have to constrain them slightly: if $x \mapsto v \in \gamma$, then $t_x \Downarrow v$, where $t_x$ is the unfolding of x. (Also see #46)
LetNonStrict (type-changing)
Type-changing The types of let-bound variables are different in $\Gamma$. A lazily bound let-variable $x : \tau$ now has type $x : () \to \tau$.
ThunkRecursions (type-changing)
Same as LetNonStrict.
Rename (type-changing, $\alpha$-equivalent)
Generalize RC: The case of Ty_Fun/Ty_Forall are too constraining, second lambda should not also bind x, but a new name y. This will include alpha conversion in the logical relation.
Datatype encoding
Kinds in $\Delta$ and types in $\Gamma$ actually stay the same. Substituting different type rep, different constructor implementations. This should be doable with parametricity and using Rel in the right way.
Desugaring/Resugaring
LetNonRec (let "desugaring")
The argument is that evaluating both results in the same substitution
vs.
This idea is extended to the sequence of bindings in a (non-recursive) let group.
BetaLet (let "resugaring")
The same argument as LetNonRec
LetRec (desugaring of let-rec into fixpoint construction)
We don't have a translation relation for this pass.
Scoping
FloatLet
SplitRec
Type-changing
Typed Closure Conversion (complex, introduces new bindings): https://dl.acm.org/doi/pdf/10.1145/237721.237791 (evt https://www.ccs.neu.edu/home/amal/papers/tccpoe.pdf) CPS transformation (type-changing, but no new bindings): https://www.hpl.hp.com/people/mark_lillibridge/PolyCPST/cw92.PDF ()
Inline
Type-changing: inlined type synonyms in type-annotations cause $\Gamma$ in the respective typing derivations to have $\delta$-equivalent types. This could be expressed as a type equality relation
where $\Delta^+$ is a kinding context, extended with type-let RHS information.
Refined notion of logical relation: The logical approximation we have used so far requires arbitrary substitutions $\gamma, \gamma' \in [\Gamma^+]$, but we will have to constrain them slightly: if $x \mapsto v \in \gamma$, then $t_x \Downarrow v$, where $t_x$ is the unfolding of x. (Also see #46)
LetNonStrict (type-changing)
Type-changing The types of let-bound variables are different in $\Gamma$. A lazily bound let-variable $x : \tau$ now has type $x : () \to \tau$.
ThunkRecursions (type-changing)
Same as LetNonStrict.
Rename (type-changing, $\alpha$-equivalent)
Generalize RC: The case of
Ty_Fun/Ty_Forallare too constraining, second lambda should not also bindx, but a new namey. This will include alpha conversion in the logical relation.Datatype encoding
Kinds in $\Delta$ and types in $\Gamma$ actually stay the same. Substituting different type rep, different constructor implementations. This should be doable with parametricity and using
Relin the right way.Other
Wrap/Unwrap cancel: should be trivial
Dead code: substitution does nothing
Othe