Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
{-# LANGUAGE GADTs #-}
module HowAreEqualityConstraintsCompiled where
data TypeEq a b where
Refl :: (a ~ b) => TypeEq a b
cast :: TypeEq a b -> a -> b
cast Refl x = x
something :: TypeEq ((), (), ()) ((),(),())
something = Refl
liftPair :: TypeEq a c -> TypeEq b d -> TypeEq (a,b) (c,d)
liftPair Refl Refl = Refl
-----------------------------------------------
==================== Tidy Core ====================
Result size of Tidy Core = {terms: 33, types: 109, coercions: 17}
HowAreEqualityConstraintsCompiled.$WRefl [InlPrag=INLINE]
:: forall a_alE b_alF. (a_alE ~ b_alF) => TypeEq a_alE b_alF
[GblId[DataConWrapper],
Arity=1,
Caf=NoCafRefs,
Str=DmdType <S,U>,
Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True,
Guidance=ALWAYS_IF(arity=1,unsat_ok=False,boring_ok=False)
Tmpl= \ (@ a_alE)
(@ b_alF)
(dt_ame [Occ=Once!] :: a_alE ~ b_alF) ->
case dt_ame of _ [Occ=Dead] { GHC.Types.Eq# dt_amf ->
HowAreEqualityConstraintsCompiled.Refl @ a_alE @ b_alF @~ dt_amf
}}]
HowAreEqualityConstraintsCompiled.$WRefl =
\ (@ a_alE) (@ b_alF) (dt_ame [Occ=Once!] :: a_alE ~ b_alF) ->
case dt_ame of _ [Occ=Dead] { GHC.Types.Eq# dt_amf ->
HowAreEqualityConstraintsCompiled.Refl @ a_alE @ b_alF @~ dt_amf
}
liftPair
:: forall a_alG c_alH b_alI d_alJ.
TypeEq a_alG c_alH
-> TypeEq b_alI d_alJ -> TypeEq (a_alG, b_alI) (c_alH, d_alJ)
[GblId, Arity=2, Caf=NoCafRefs, Str=DmdType]
liftPair =
\ (@ a_amy)
(@ c_amz)
(@ b_amA)
(@ d_amB)
(ds_dne :: TypeEq a_amy c_amz)
(ds1_dnf :: TypeEq b_amA d_amB) ->
case ds_dne of _ [Occ=Dead] { Refl dt_dnw ->
case ds1_dnf of _ [Occ=Dead] { Refl dt1_dnx ->
(HowAreEqualityConstraintsCompiled.Refl
@ (a_amy, b_amA) @ (a_amy, b_amA) @~ <(a_amy, b_amA)>_N)
`cast` ((TypeEq <(a_amy, b_amA)>_N (dt_dnw, dt1_dnx)_N)_R
:: TypeEq (a_amy, b_amA) (a_amy, b_amA)
~R# TypeEq (a_amy, b_amA) (c_amz, d_amB))
}
}
something :: TypeEq ((), (), ()) ((), (), ())
[GblId, Caf=NoCafRefs, Str=DmdType]
something =
HowAreEqualityConstraintsCompiled.Refl
@ ((), (), ()) @ ((), (), ()) @~ <((), (), ())>_N
cast :: forall a_alK b_alL. TypeEq a_alK b_alL -> a_alK -> b_alL
[GblId, Arity=2, Caf=NoCafRefs, Str=DmdType]
cast =
\ (@ a_amN)
(@ b_amO)
(ds_dno :: TypeEq a_amN b_amO)
(x_alM :: a_amN) ->
case ds_dno of _ [Occ=Dead] { Refl dt_dns ->
x_alM `cast` (Sub dt_dns :: a_amN ~R# b_amO)
}
---------------------------
==================== STG syntax: ====================
HowAreEqualityConstraintsCompiled.$WRefl [InlPrag=INLINE]
:: forall a_alE b_alF.
(a_alE ~ b_alF) =>
HowAreEqualityConstraintsCompiled.TypeEq a_alE b_alF
[GblId[DataConWrapper],
Arity=1,
Caf=NoCafRefs,
Str=DmdType <S,U>,
Unf=OtherCon []] =
\r srt:SRT:[] [dt_swD]
case dt_swD of _ [Occ=Dead] {
GHC.Types.Eq# dt_amf ->
HowAreEqualityConstraintsCompiled.Refl [GHC.Prim.coercionToken#];
};
HowAreEqualityConstraintsCompiled.cast
:: forall a_alK b_alL.
HowAreEqualityConstraintsCompiled.TypeEq a_alK b_alL
-> a_alK -> b_alL
[GblId, Arity=2, Caf=NoCafRefs, Str=DmdType, Unf=OtherCon []] =
\r srt:SRT:[] [ds_swF x_swG]
case ds_swF of _ [Occ=Dead] {
HowAreEqualityConstraintsCompiled.Refl dt_dnA -> x_swG;
};
HowAreEqualityConstraintsCompiled.liftPair
:: forall a_alG c_alH b_alI d_alJ.
HowAreEqualityConstraintsCompiled.TypeEq a_alG c_alH
-> HowAreEqualityConstraintsCompiled.TypeEq b_alI d_alJ
-> HowAreEqualityConstraintsCompiled.TypeEq
(a_alG, b_alI) (c_alH, d_alJ)
[GblId, Arity=2, Caf=NoCafRefs, Str=DmdType, Unf=OtherCon []] =
\r srt:SRT:[] [ds_swI ds1_swJ]
case ds_swI of _ [Occ=Dead] {
HowAreEqualityConstraintsCompiled.Refl dt_dns ->
case ds1_swJ of _ [Occ=Dead] {
HowAreEqualityConstraintsCompiled.Refl dt1_dnt ->
HowAreEqualityConstraintsCompiled.Refl [GHC.Prim.coercionToken#];
};
};
HowAreEqualityConstraintsCompiled.something
:: HowAreEqualityConstraintsCompiled.TypeEq
((), (), ()) ((), (), ())
[GblId, Caf=NoCafRefs, Str=DmdType, Unf=OtherCon []] =
NO_CCS HowAreEqualityConstraintsCompiled.Refl! [GHC.Prim.coercionToken#];
HowAreEqualityConstraintsCompiled.Refl
:: forall a_alE b_alF.
a_alE GHC.Prim.~# b_alF
-> HowAreEqualityConstraintsCompiled.TypeEq a_alE b_alF
[GblId[DataCon],
Arity=1,
Caf=NoCafRefs,
Str=DmdType <L,U>,
Unf=OtherCon []] =
\r srt:SRT:[] [eta_B1]
HowAreEqualityConstraintsCompiled.Refl [GHC.Prim.coercionToken#];
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment