HowAreEqualityConstraintsCompiled.hs

{-# 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#];