+import Data.Coerce

+setElems (LS s) = coerce $ S.elems s

+mapToList (LM m) = coerce $ M.toList m

+To achieve this, `go` in `uVarOrFam` does this;

+

+* We maintain /two/ substitutions, not just one:

+     * um_tv_env: the regular substitution, mapping TyVar :-> Type

+     * um_fam_env: maps (TyCon,[Type]) :-> Type, where the LHS is a type-fam application

+  In effect, these constitute one substitution mapping

+     CanEqLHS :-> Types

+  but we /also/ add a "family substitution" [G Float :-> Int],

+  to `um_fam_env`. See the `BindMe` case of `go` in `uVarOrFam`.

+  when we encounter a type variable.  See the `lookupFamEnv` in `go` in

+   `go` in `uVarOrFam`

+(ATF13) Consider unifying

+    [F a, F Int, Int]  ~  [Bool, Char, a]

+  Working left to right you might think we would build the mapping

+    F a   :-> Bool

+    F Int :-> Char

+  Now we discover that `a` unifies with `Int`. So really these two lists are Apart

+  because F Int can't be both Bool and Char.

+

+  But that is very tricky! Perhaps whenever we unify a type variable we should

+  run it over the domain and (maybe range) of the type-family mapping too?

+  Sigh.

+

+  For we make no such attempt.  The um_fam_env has only pre-substituted types.

+  Fortunately, while this may make use say MaybeApart when we could say SurelyApart,

+  it has no effect on the correctness of unification: if we return Unifiable, it

+  really is Unifiable.

+

+(ATF14) We have to be careful about the occurs check.

+  See Note [The occurs check in the Core unifier]

+

+    -- LHS is a type variable

+    go swapped substs lhs@(TyVarLHS tv1) ty2 kco

+        occurs_check = um_unif env && uOccursCheck substs lhs rhs

+          -- Make sure you include `kco` in rhs #14846

+    -- LHS is a saturated type-family application

+    go swapped substs lhs@(TyFamLHS tc1 tys1) ty2 kco

+      = if uOccursCheck substs lhs rhs

+        then maybeApart MARInfinite

+        else do { extendFamEnv tc1 tys1 rhs  -- We don't substitue tys1; see (ATF13)

+                ; maybeApart MARTypeFamily }

+uOccursCheck :: UMState -> CanEqLHS -> Type -> Bool

+-- See Note [The occurs check in the Core unifier] and (ATF13)

+uOccursCheck (UMState { um_tv_env = tv_env, um_fam_env = fam_env }) lhs ty

+  = go emptyVarSet ty

+    go :: TyCoVarSet   -- Bound by enclosing foralls

+       -> Type -> Bool

+    go bvs ty | Just ty' <- coreView ty = go bvs ty'

+    go bvs (TyVarTy tv) | Just ty' <- lookupVarEnv tv_env tv

+                        = go bvs ty'

+                        | TyVarLHS tv' <- lhs, tv==tv'

+                        = True

+                        | otherwise

+                        = go bvs (tyVarKind tv)

+    go bvs (AppTy ty1 ty2)           = go bvs ty1 || go bvs ty2

+    go _   (LitTy {})                = False

+    go bvs (FunTy _ w arg res)       = go bvs w || go bvs arg || go bvs res

+    go bvs (TyConApp tc tys)         = go_tc bvs tc tys

+

+    go bvs (ForAllTy (Bndr tv _) ty)

+      = go bvs (tyVarKind tv) ||

+        (case lhs of

+           TyVarLHS tv' | tv==tv'   -> False  -- Shadowing

+                        | otherwise -> go (bvs `extendVarSet` tv) ty

+           TyFamLHS {} -> False)  -- Lookups don't happen under a forall

+

+    go bvs (CastTy ty  _co) = go bvs ty  -- ToDo: should we worry about `co`?

+    go _   (CoercionTy _co) = False      -- ToDo: should we worry about `co`?

+

+    go_tc bvs tc tys

+      | isTypeFamilyTyCon tc

+      , Just ty' <- lookupFamEnv fam_env tc (take arity tys)

+      = go bvs ty' || any (go bvs) (drop arity tys)

+

+      | TyFamLHS tc' tys' <- lhs

+      , tc == tc'

+      , tys `lengthAtLeast` arity  -- Saturated, or over-saturated

+      , and (zipWith tcEqType tys tys')

+      = True

+

+      | otherwise

+      = any (go bvs) tys

+      where

+        arity = tyConArity tc

+{- Note [The occurs check in the Core unifier]

+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

+The unifier applies both substitutions (um_tv_env and um_fam_env) as it goes,

+so we'll get an infinite loop if we have, for example

+    um_tv_env:   a :-> F b      -- (1)

+    um_fam_env   F b :-> a      -- (2)

+

+So (uOccursCheck substs lhs ty) returns True iff extending `substs` with `lhs :-> ty`

+could lead to a loop. That is, could there by a type `s` such that

+  applySubsts( (substs + lhs:->ty), s ) is infinite

+

+It's vital that we do both at once: we might have (1) already and add (2);

+or we might have (2) already and add (1).

+

+Note [Unifying coercion-foralls]

+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

+       ; checkPromotedDataConName env tv Prefix ip name

+        ; checkPromotedDataConName env ty Infix prom op_name

+-- | If a 'Name' is that of a promoted data constructor, perform various

+-- validity checks on it.

+checkPromotedDataConName ::

+  RnTyKiEnv ->

+  -- | The type that the 'Name' belongs to. This will always be an 'HsTyVar'

+  -- (for 'Prefix' names) or an 'HsOpTy' (for 'Infix' names).

+  HsType GhcPs ->

+  -- | Whether the type is written 'Prefix' or 'Infix'.

+  LexicalFixity ->

+  -- | Whether the name was written with an explicit promotion tick or not.

+  PromotionFlag ->

+  -- | The name to check.

+  Name ->

+  TcM ()

+checkPromotedDataConName env ty fixity ip name

+  = do when (isDataConName name && not (isKindName name)) $

+         -- Any use of a promoted data constructor name (that is not

+         -- specifically exempted by isKindName) is illegal without the use

+         -- of DataKinds. See Note [Checking for DataKinds] in

+         -- GHC.Tc.Validity.

+         checkDataKinds env ty

+       when (isDataConName name && not (isPromoted ip)) $

+         addDiagnostic (TcRnUntickedPromotedThing $ UntickedConstructor fixity name)

+

+  = -- | TFTyFam: LHS is a type family application

+    -- Invariant: we are not unifying; see `notUnifying_TEFTask`

+    TEFTyFam

+

+  -- | TEFTyVar: LHS is a 'TyVar'.

+- Fix a bug introduced in GHC 9.10 where GHC would erroneously accept infix uses

+  of promoted data constructors without enabling :extension:`DataKinds`. As a

+  result, you may need to enable :extension:`DataKinds` in code that did not

+  previously require it.

+

+    outer  = StgTRecHeader_enclosing_trec(trec);

+    (r) = ccall stmCommitNestedTransaction(MyCapability() "ptr", trec "ptr");

+    if (r != 0) {

+        // Succeeded (either first branch or second branch)

+        StgTSO_trec(CurrentTSO) = outer;

+        return (ret);

+    } else {

+        // Did not commit: abort and restart.

+        StgTSO_trec(CurrentTSO) = outer;

+        jump stg_abort();

+        // The retry reaches a CATCH_RETRY_FRAME before the atomic frame

+        ASSERT(outer != NO_TREC);

+        // Abort the transaction attempting the current branch

+        ccall stmAbortTransaction(MyCapability() "ptr", trec "ptr");

+        ccall stmFreeAbortedTRec(MyCapability() "ptr", trec "ptr");

+            // Retry in the first branch: try the alternative

+            ("ptr" trec) = ccall stmStartTransaction(MyCapability() "ptr", outer "ptr");

+            StgTSO_trec(CurrentTSO) = trec;

+            // Retry in the alternative code: propagate the retry

+            StgTSO_trec(CurrentTSO) = outer;

+        case CATCH_RETRY_FRAME:

+            // CATCH frames within an atomically block: abort the

+            debugTraceCap(DEBUG_stm, cap,

+                          "found atomically block delivering async exception");

+{-# LANGUAGE GHC2024 #-}

+{-# LANGUAGE TypeFamilies #-}

+{-# LANGUAGE UndecidableInstances #-}

+module T26346 (warble) where

+

+import Data.Kind (Type)

+import Data.Type.Equality ((:~:)(..))

+

+type Nat :: Type

+data Nat = Z | S Nat

+

+type SNat :: Nat -> Type

+data SNat n where

+  SZ :: SNat Z

+  SS :: SNat n -> SNat (S n)

+

+type NatPlus :: Nat -> Nat -> Nat

+type family NatPlus a b where

+  NatPlus Z     b = b

+  NatPlus (S a) b = S (NatPlus a b)

+

+sNatPlus ::

+  forall (a :: Nat) (b :: Nat).

+  SNat a ->

+  SNat b ->

+  SNat (NatPlus a b)

+sNatPlus SZ     b = b

+sNatPlus (SS a) b = SS (sNatPlus a b)

+

+data Bin

+  = Zero

+  | Even Bin

+  | Odd Bin

+

+type SBin :: Bin -> Type

+data SBin b where

+  SZero :: SBin Zero

+  SEven :: SBin n -> SBin (Even n)

+  SOdd  :: SBin n -> SBin (Odd n)

+

+type Incr :: Bin -> Bin

+type family Incr b where

+  Incr Zero     = Odd Zero      -- 0 + 1 = (2*0) + 1

+  Incr (Even n) = Odd n         -- 2n + 1

+  Incr (Odd n)  = Even (Incr n) -- (2n + 1) + 1 = 2*(n + 1)

+

+type BinToNat :: Bin -> Nat

+type family BinToNat b where

+  BinToNat Zero     = Z

+  BinToNat (Even n) = NatPlus (BinToNat n) (BinToNat n)

+  BinToNat (Odd n)  = S (NatPlus (BinToNat n) (BinToNat n))

+

+sBinToNat ::

+  forall (b :: Bin).

+  SBin b ->

+  SNat (BinToNat b)

+sBinToNat SZero     = SZ

+sBinToNat (SEven n) = sNatPlus (sBinToNat n) (sBinToNat n)

+sBinToNat (SOdd n)  = SS (sNatPlus (sBinToNat n) (sBinToNat n))

+

+warble ::

+  forall (b :: Bin).

+  SBin b ->

+  BinToNat (Incr b) :~: S (BinToNat b)

+warble SZero = Refl

+warble (SEven {}) = Refl

+warble (SOdd  sb) | Refl <- warble sb

+                  , Refl <- plusComm sbn (SS sbn)

+                  = Refl

+  where

+    sbn = sBinToNat sb

+

+    plus0R ::

+      forall (n :: Nat).

+      SNat n ->

+      NatPlus n Z :~: n

+    plus0R SZ = Refl

+    plus0R (SS sn)

+      | Refl <- plus0R sn

+      = Refl

+

+    plusSnR ::

+      forall (n :: Nat) (m :: Nat).

+      SNat n ->

+      SNat m ->

+      NatPlus n (S m) :~: S (NatPlus n m)

+    plusSnR SZ _ = Refl

+    plusSnR (SS sn) sm

+      | Refl <- plusSnR sn sm

+      = Refl

+

+    plusComm ::

+      forall (n :: Nat) (m :: Nat).

+      SNat n ->

+      SNat m ->

+      NatPlus n m :~: NatPlus m n

+    plusComm SZ sm

+      | Refl <- plus0R sm

+      = Refl

+    plusComm (SS sn) sm

+      | Refl <- plusComm sn sm

+      , Refl <- plusSnR sm sn

+      = Refl

+test('T26346', normal, compile, [''])

+{-# LANGUAGE GHC2021 #-}

+{-# LANGUAGE NoDataKinds #-}

+module T26318 where

+

+class C1 l

+instance C1 (x : xs)

+

+class C2 l

+instance C2 (x ': xs)

+

+class C3 l

+instance C3 ((:) x xs)

+

+class C4 l

+instance C4 ('(:) x xs)

+T26318.hs:6:16: error: [GHC-68567]

+    Illegal type: ‘x : xs’

+    Suggested fix:

+      Perhaps you intended to use the ‘DataKinds’ extension (implied by ‘UnliftedDatatypes’)

+

+T26318.hs:9:16: error: [GHC-68567]

+    Illegal type: ‘x ': xs’

+    Suggested fix:

+      Perhaps you intended to use the ‘DataKinds’ extension (implied by ‘UnliftedDatatypes’)

+

+T26318.hs:12:14: error: [GHC-68567]

+    Illegal type: ‘(:)’

+    Suggested fix:

+      Perhaps you intended to use the ‘DataKinds’ extension (implied by ‘UnliftedDatatypes’)

+

+T26318.hs:15:14: error: [GHC-68567]

+    Illegal type: ‘'(:)’

+    Suggested fix:

+      Perhaps you intended to use the ‘DataKinds’ extension (implied by ‘UnliftedDatatypes’)

+

+test('T26318', normal, compile_fail, [''])

+

+        // At this point the RTS symbols in linear memory are fixed

+        // and constructors are run, especially the one in JSFFI.c

+        // that does GHC RTS initialization for any code that links

+        // JSFFI.o. Luckily no Haskell computation or gc has taken

+        // place yet, so we must set keepCAFs=1 right now! Otherwise,

+        // any BCO created by later TH splice or ghci expression may

+        // refer to any CAF that's not reachable from GC roots (here

+        // our only entry point is defaultServer) and the CAF could

+        // have been GC'ed! (#26106)

+        //

+        // We call it here instead of in RTS C code, since we only

+        // want keepCAFs=1 for ghci, not user code.

+        this.exportFuncs.setKeepCAFs();