+import GHC.Tc.Utils.TcType (isStringTy, topTcLevel)

+initTyState = TySt 0 (emptyInert topTcLevel)

+        mkTopLevEnv, mkTopLevImportedEnv,

+                (IfaceTopEnv exports _imports) -> do

+                  imports_env <- mkTopLevImportedEnv hsc_env details

+-- | Make the top-level environment with all bindings imported by this module.

+-- Exported bindings from this module are not included in the result.

+mkTopLevImportedEnv :: HscEnv -> HomeModInfo -> IO GlobalRdrEnv

+mkTopLevImportedEnv hsc_env details = do

+    runInteractiveHsc hsc_env

+  $ ioMsgMaybe $ hoistTcRnMessage $ runTcInteractive hsc_env

+  $ fmap (foldr plusGlobalRdrEnv emptyGlobalRdrEnv)

+  $ forM imports $ \iface_import -> do

+    let ImpUserSpec spec details = tcIfaceImport iface_import

+    iface <- loadInterfaceForModule (text "imported by GHCi") (is_mod spec)

+    pure $ case details of

+      ImpUserAll -> importsFromIface hsc_env iface spec Nothing

+      ImpUserEverythingBut ns -> importsFromIface hsc_env iface spec (Just ns)

+      ImpUserExplicit x _parents_of_implicits ->

+        -- TODO: Not quite right, is_explicit should refer to whether the user wrote A(..) or A(x,y).

+        -- It is only used for error messages. It seems dubious even to add an import context to these GREs as

+        -- they are not "imported" into the top-level scope of the REPL. I changed this for now so that

+        -- the test case produce the same output as before.

+        let spec' = ImpSpec { is_decl = spec, is_item = ImpSome { is_explicit = True, is_iloc = noSrcSpan } }

+        in mkGlobalRdrEnv $ gresFromAvails hsc_env (Just spec') x

+  where

+    IfaceTopEnv _ imports = mi_top_env (hm_iface details)

+

+       -- NB: we must gather up all the bindings from doing this solving; hence

+       -- (runTcSWithEvBinds ev_binds_var).  And note that since there are

+       -- nested implications, calling solveWanteds will side-effect their

+       -- evidence bindings, so we can't just revert to the input constraint.

+       --

+       -- See also Note [Inferring principal types]

+            <- runTcSWithEvBinds ev_binds_var $

+               setTcLevelTcS rhs_tclvl        $

+               -- setLevelTcS: we do setLevel /inside/ the runTcS, so that

+               --              we initialise the InertSet inert_given_eq_lvl as far

+               --              out as possible, maximising oppportunities to unify

+             -- The `no_quant_tvs` are free in constraints we can't quantify.

+             (can_quant_cts, no_quant_tvs) = approximateWCX False wanted

+             can_quant_tvs = tyCoVarsOfTypes can_quant

+             mr_no_quant_tvs              = tyCoVarsOfTypes mr_no_quant

+             -- outer_tvs are mentioned in `wanted`, and belong to some outer level.

+                         can_quant_tvs `unionVarSet` no_quant_tvs

+             -- Step 3 of Note [decideAndPromoteTyVars], (a-c)

+             -- At top level we are much less keen to create mono tyvars, to avoid

+             -- spooky action at a distance.

+               | is_top_level = outer_tvs    -- See (DP2)

+               | otherwise    = outer_tvs                    -- (a)

+                                `unionVarSet` no_quant_tvs   -- (b)

+                                `unionVarSet` co_var_tvs     -- (c)

+             -- Step 3 of Note [decideAndPromoteTyVars], (d)

+                 mono_tvs_without_mr `unionVarSet` mr_no_quant_tvs

+             add_determined tvs preds = closeWrtFunDeps preds tvs

+                                        `delVarSetList` psig_qtvs

+             mono_tvs_with_mr_det    = add_determined mono_tvs_with_mr    post_mr_quant

+             mono_tvs_without_mr_det = add_determined mono_tvs_without_mr can_quant

+           , text "no_quant_tvs =" <+> ppr no_quant_tvs

+  We don't want to quantify over beta or gamma because they are fixed by alpha,

+  which is monomorphic. Actual test case:   typecheck/should_compile/tc213

+  An example is in #26004.

+      f w e = case e of

+        T1 -> let y = not w in False

+        T2 -> True

+  When generalising `f` we have a constraint

+      forall. (a ~ Bool) => alpha ~ Bool

+  where our provisional type for `f` is `f :: T alpha -> blah`.

+  In a /nested/ setting, we might simply not-generalise `f`, hoping to learn

+  about `alpha` from f's call sites (test T5266b is an example).  But at top

+  level, to avoid spooky action at a distance.

+

+Key principles:

+  * we never want to show the programmer a type with `Any` in it.

+  * avoid "spooky action at a distance" and silent defaulting

+Moreover,

+ * If (elsewhere in this module) we add a call to `f`, say (f True), then

+   `f` will get the type `Bool -> Int`

+ * If we add /another/ call, say (f 'x'), we will then get a type error.

+ * If we have no calls, the final exported type of `f` may get set by

+   defaulting, and might not be principal (#26004).

+

+distance".  This also moves in the direction of `MonoLocalBinds`, which we like.

+emptyInertCans :: TcLevel -> InertCans

+emptyInertCans given_eq_lvl

+       , inert_given_eq_lvl = given_eq_lvl

+emptyInert :: TcLevel -> InertSet

+emptyInert given_eq_lvl

+  = IS { inert_cans           = emptyInertCans given_eq_lvl

+(TGE6) A subtle point is this: when initialising the solver, giving it

+   an empty InertSet, we must conservatively initialise `inert_given_lvl`

+   to the /current/ TcLevel.  This matters when doing let-generalisation.

+   Consider #26004:

+      f w e = case e of

+                  T1 -> let y = not w in False   -- T1 is a GADT

+                  T2 -> True

+   When let-generalising `y`, we will have (w :: alpha[1]) in the type

+   envt; and we are under GADT pattern match.  So when we solve the

+   constraints from y's RHS, in simplifyInfer, we must NOT unify

+       alpha[1] := Bool

+   Since we don't know what enclosing equalities there are, we just

+   conservatively assume that there are some.

+

+   This initialisation in done in `runTcSWithEvBinds`, which passes

+   the current TcLevl to `emptyInert`.

+

+    nestTcS, nestImplicTcS, setEvBindsTcS, setTcLevelTcS,

+  | TcSPMCheck    -- ^ Used when doing patterm match overlap checks

+  | TcSSpecPrag   -- ^ Fully solve all constraints

+* TcSPMCheck: Used by the pattern match overlap checker.

+      Like TcSVanilla, but the idea is that the returned InertSet will

+      later be resumed, so we do not want to restore type-equality cycles

+      See also Note [Type equality cycles] in GHC.Tc.Solver.Equality

+

+       ; runTcSWithEvBinds' TcSEarlyAbort ev_binds_var tcs }

+  = runTcSWithEvBinds' TcSSpecPrag ev_binds_var tcs

+  runTcSWithEvBinds' TcSPMCheck ev_binds_var $ do

+runTcSWithEvBinds = runTcSWithEvBinds' TcSVanilla

+runTcSWithEvBinds' :: TcSMode

+runTcSWithEvBinds' mode ev_binds_var tcs

+       ; step_count  <- TcM.newTcRef 0

+

+       -- Make a fresh, empty inert set

+       -- Subtle point: see (TGE6) in Note [Tracking Given equalities]

+       --               in GHC.Tc.Solver.InertSet

+       ; tc_lvl      <- TcM.getTcLevel

+       ; inert_var   <- TcM.newTcRef (emptyInert tc_lvl)

+

+       ; wl_var      <- TcM.newTcRef emptyWorkList

+       -- Restore tyvar cycles: see Note [Type equality cycles] in

+       --                       GHC.Tc.Solver.Equality

+       -- But /not/ in TCsPMCheck mode: see Note [TcSMode]

+       ; case mode of

+            TcSPMCheck -> return ()

+            _ -> do { inert_set <- TcM.readTcRef inert_var

+                    ; restoreTyVarCycles inert_set }

+setTcLevelTcS :: TcLevel -> TcS a -> TcS a

+setTcLevelTcS lvl (TcS thing_inside)

+ = TcS $ \ env -> TcM.setTcLevel lvl (thing_inside env)

+

+    keep_ct ct

+      = case classifyPredType (ctPred ct) of

+           ClassPred cls _ -> isEqualityClass cls

+             -- isEqualityClass: see (CERR2) in Note [Constraints and errors]

+             --                  in GHC.Tc.Utils.Monad

+           _ -> True

+type ApproxWC = ( Bag Ct          -- Free quantifiable constraints

+                , TcTyCoVarSet )  -- Free vars of non-quantifiable constraints

+                                  -- due to shape, or enclosing equality

+  = fst (approximateWCX include_non_quantifiable cts)

+approximateWCX :: Bool -> WantedConstraints -> ApproxWC

+approximateWCX include_non_quantifiable wc

+  = float_wc False emptyVarSet wc (emptyBag, emptyVarSet)

+       | insolubleCt ct                       = acc

+       | pred_tvs `intersectsVarSet` skol_tvs = acc

+       | include_non_quantifiable             = add_to_quant

+       | is_quantifiable encl_eqs (ctPred ct) = add_to_quant

+       | otherwise                            = add_to_no_quant

+       where

+         pred     = ctPred ct

+         pred_tvs = tyCoVarsOfType pred

+         add_to_quant    = (ct `consBag` quant, no_quant)

+         add_to_no_quant = (quant, no_quant `unionVarSet` pred_tvs)

+

+    is_quantifiable encl_eqs pred

+       = case classifyPredType pred of

+             | encl_eqs  -> False  -- encl_eqs: See Wrinkle (W1)

+             | otherwise -> quantify_equality eq_rel ty1 ty2

+             -> False

+             -> True  -- See Wrinkle (W2)

+           IrredPred {}  -> True  -- See Wrinkle (W2)

+           ForAllPred {} -> False  -- Never quantify these

+  do *not* quantify over equality constraint if the implication binds

+       ; case mb_res of

+            Just {} -> return (mb_res, lie)

+            Nothing -> do { let pruned_lie = dropMisleading lie

+                          ; traceTc "tryCaptureConstraints" $

+                            vcat [ text "lie:" <+> ppr lie

+                                 , text "dropMisleading lie:" <+> ppr pruned_lie ]

+                          ; return (Nothing, pruned_lie) } }

+  class constraints mentioned above.

+

+  We may /also/ end up taking constraints built at some inner level, and

+  emitting them (via the exception catching in `tryCaptureConstraints` at some

+  outer level, and then breaking the TcLevel invariants See Note [TcLevel

+  invariants] in GHC.Tc.Utils.TcType

+

+So `dropMisleading` has a horridly ad-hoc structure:

+

+* It keeps only /insoluble/ flat constraints (which are unlikely to very visibly

+  trip up on the TcLevel invariant

+

+* But it keeps all /implication/ constraints (except the class constraints

+  inside them).  The implication constraints are OK because they set the ambient

+  level before attempting to solve any inner constraints.

+

+Ugh! I hate this. But it seems to work.

+

+Other wrinkles

+

+(CERR1) Note that freshly-generated constraints like (Int ~ Bool), or

+    ((a -> b) ~ Int) are all CNonCanonical, and hence won't be flagged as

+    insoluble.  The constraint solver does that.  So they'll be discarded.

+    That's probably ok; but see th/5358 as a not-so-good example:

+       t1 :: Int

+       t1 x = x   -- Manifestly wrong

+

+       foo = $(...raises exception...)

+    We report the exception, but not the bug in t1.  Oh well.  Possible

+    solution: make GHC.Tc.Utils.Unify.uType spot manifestly-insoluble constraints.

+

+(CERR2) In #26015 I found that from the constraints

+           [W] alpha ~ Int      -- A class constraint

+           [W] F alpha ~# Bool  -- An equality constraint

+  we were dropping the first (becuase it's a class constraint) but not the

+  second, and then getting a misleading error message from the second.  As

+  #25607 shows, we can get not just one but a zillion bogus messages, which

+  conceal the one genuine error.  Boo.

+

+  For now I have added an even more ad-hoc "drop class constraints except

+  equality classes (~) and (~~)"; see `dropMisleading`.  That just kicks the can

+  down the road; but this problem seems somewhat rare anyway.  The code in

+  `dropMisleading` hasn't changed for years.

+

+It would be great to have a more systematic solution to this entire mess.

+        sizeOccEnv,

+sizeOccEnv :: OccEnv a -> Int

+sizeOccEnv (MkOccEnv as) =

+  nonDetStrictFoldUFM (\ m !acc -> acc + sizeUFM m) 0 as

+

+{-# LANGUAGE GADTs #-}

+{-# LANGUAGE NoMonoLocalBinds #-}

+

+module T26004 where

+

+data T a where

+  T1 :: T Bool

+  T2 :: T a

+

+-- This funcion should be rejected:

+-- we should not infer a non-principal type for `f`

+f w e = case e of

+  T1 -> let y = not w in False

+  T2 -> True

+

+T26004.hs:13:21: error: [GHC-25897]

+    • Could not deduce ‘p ~ Bool’

+      from the context: a ~ Bool

+        bound by a pattern with constructor: T1 :: T Bool,

+                 in a case alternative

+        at T26004.hs:13:3-4

+      ‘p’ is a rigid type variable bound by

+        the inferred type of f :: p -> T a -> Bool

+        at T26004.hs:(12,1)-(14,12)

+    • In the first argument of ‘not’, namely ‘w’

+      In the expression: not w

+      In an equation for ‘y’: y = not w

+    • Relevant bindings include

+        w :: p (bound at T26004.hs:12:3)

+        f :: p -> T a -> Bool (bound at T26004.hs:12:1)

+    Suggested fix: Consider giving ‘f’ a type signature

+{-# LANGUAGE MonoLocalBinds, GADTs, TypeFamilies #-}

+

+module Foo where

+

+type family F a

+type instance F Int = Bool

+

+data T where

+  T1 :: a -> T

+  T2 :: Int -> T

+

+woo :: (a ~ Int) => Int -> F a

+woo = error "urk"

+

+f x = case x of

+         T1 y -> not (woo 3)

+         T2 -> True

+T26015.hs:17:10: error: [GHC-27346]

+    • The data constructor ‘T2’ should have 1 argument, but has been given none

+    • In the pattern: T2

+      In a case alternative: T2 -> True

+      In the expression:

+        case x of

+          T1 y -> not (woo 3)

+          T2 -> True

+

+T7453.hs:10:30: error: [GHC-25897]

+    • Couldn't match expected type ‘t’ with actual type ‘p’

+    • In the first argument of ‘Id’, namely ‘v’

+      In the expression: Id v

+      In an equation for ‘aux’: aux = Id v

+        aux :: Id t (bound at T7453.hs:10:21)

+T7453.hs:16:33: error: [GHC-25897]

+    • Couldn't match expected type ‘t1’ with actual type ‘p’

+    • In the first argument of ‘const’, namely ‘v’

+      In the expression: const v

+      In an equation for ‘aux’: aux = const v

+        aux :: b -> t1 (bound at T7453.hs:16:21)

+

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