+    gHC_CLASSES, gHC_CLASSES_IP, gHC_PRIMOPWRAPPERS :: Module

+gHC_CLASSES_IP     = mkGhcInternalModule (fsLit "GHC.Internal.Classes.IP")

+  = clsQual gHC_CLASSES_IP (fsLit "IP") ipClassKey

+                           , fim_tys      = substTyVars subst tpl_tvs `chkAppend` match_tys2

+                           , fim_cos      = assert (all (isJust . lookupCoVar subst) tpl_cvs) $

+                                            substCoVars subst tpl_cvs

+                           })

+        tcUnwrapNewtype_maybe,

+-- | 'tcUnwrapNewtype_mabye' gets rid of /one layer/ of top-level newtypes

+-- It is capable of unwrapping a newtype /instance/.  E.g

+--    data D a

+--    newtype instance D Int = MkD Bool

+-- Then `tcUnwrapNewtype_maybe (D Int)` will unwrap to give the `Bool` inside.

+-- However, it is careful not to unwrap data/newtype instances if it can't

+-- unwrap the newtype inside it; that might in the example if `MkD` was

+-- not in scope.  Such care is necessary for proper error messages.

+-- It does not normalise arguments to the tycon.

+-- If the result is Just (gre, co, rep_ty), then

+--    gre is the GRE for the data constructor that had to be in scope

+tcUnwrapNewtype_maybe :: FamInstEnvs

+                      -> GlobalRdrEnv

+                      -> Type

+                      -> Maybe (GlobalRdrElt, TcCoercion, Type)

+tcUnwrapNewtype_maybe faminsts rdr_env ty

+  | Just (tc,tys) <- tcSplitTyConApp_maybe ty

+  = firstJust (try_nt_unwrap tc tys)

+              (try_fam_unwrap tc tys)

+  | otherwise

+  = Nothing

+    -- For newtype /instances/ we take a double step or nothing, so that

+    try_fam_unwrap tc tys

+      | Just (tc', tys', fam_co) <- tcLookupDataFamInst_maybe faminsts tc tys

+      , Just (gre, nt_co, ty') <- try_nt_unwrap tc' tys'

+      = Just (gre, mkTransCo fam_co nt_co, ty')

+      | otherwise

+      = Nothing

+    try_nt_unwrap tc tys

+      , Just (ty', co) <- instNewTyCon_maybe tc tys

+      = Just (gre, co, ty')

+      = Nothing

+import GHC.Tc.Instance.Family ( tcUnwrapNewtype_maybe )

+-- Look for (N s1 .. sn) ~R# (N t1 .. tn)

+-- where either si=ti

+--       or     N is phantom in i'th position

+-- See Note [Solving newtype equalities: overview]

+-- and (for details) Note [Eager newtype decomposition]

+-- We try this /before/ attempting to unwrap N, because if N is

+-- recursive, unwrapping will loop.

+-- This /matters/ for newtypes, but is /safe/ for all types

+can_eq_nc _rewritten _rdr_env _envs ev eq_rel ty1 _ ty2 _

+  | ReprEq <- eq_rel

+  , TyConApp tc1 tys1 <- ty1

+  , TyConApp tc2 tys2 <- ty2

+  , tc1 == tc2

+  , ok tys1 tys2 (tyConRoles tc1)

+  = canDecomposableTyConAppOK ev eq_rel tc1 (ty1,tys1) (ty2,tys2)

+  where

+    ok :: [TcType] -> [TcType] -> [Role] -> Bool

+    -- OK to decompose a representational equality

+    --   if the args are already equal

+    --   or are phantom role

+    -- See Note [Eager newtype decomposition]

+    -- You might think that representational role would also be OK, but

+    --   see Note [Even more eager newtype decomposition]

+    ok (ty1:tys1) (ty2:tys2) rs

+      | Phantom : rs' <- rs = ok tys1 tys2 rs'

+      | ty1 `tcEqType` ty2  = ok tys1 tys2 (drop 1 rs)

+      | otherwise           = False

+    ok [] [] _  = True

+    ok _  _  _  = False  -- Mis-matched lengths, just about possible because of

+                         -- kind polymorphism.  Anyway False is a safe result!

+

+-- Unwrap newtypes, when in ReprEq only

+-- See Note [Solving newtype equalities: overview]

+-- and (for details) Note [Unwrap newtypes first]

+--

+-- We unwrap *one layer only*; `can_eq_newtype_nc` then loops back to

+-- `can_eq_nc`.  If there is a recursive newtype, so that we keep

+-- unwrapping, the depth limit in `can_eq_newtype_nc` will blow up.

+  , Just stuff1 <- tcUnwrapNewtype_maybe envs rdr_env ty1

+  , Just stuff2 <- tcUnwrapNewtype_maybe envs rdr_env ty2

+can_eq_nc _rewritten _rdr_env _envs ev eq_rel

+           s1@ForAllTy{} _

+           s2@ForAllTy{} _

+  = can_eq_nc_forall ev eq_rel s1 s2

+

+-- Decompose applications

+can_eq_nc rewritten _rdr_env _envs ev eq_rel ty1 _ ty2 _

+  | True <- rewritten -- Why True?  See Note [Canonicalising type applications]

+  -- Use tcSplitAppTy, not matching on AppTy, to catch oversaturated type families

+  , Just (t1, s1) <- tcSplitAppTy_maybe ty1

+  = case eq_rel of

+       NomEq  -> can_eq_app ev t1 s1 t2 s2

+                 -- Only decompose AppTy for nominal equality.

+                 -- See (APT1) in Note [Decomposing AppTy equalities]

+

+       ReprEq | ty1 `tcEqType` ty2 -> canEqReflexive ev ReprEq ty1

+                 -- tcEqType: see (APT2) in Note [Decomposing AppTy equalities]

+              | otherwise          -> finishCanWithIrred ReprEqReason ev

+                  -> (GlobalRdrElt, TcCoercion, TcType)  -- ^ :: ty1 ~ ty1'

+can_eq_newtype_nc rdr_env envs ev swapped (gre, co1, ty1') ty2 ps_ty2

+         vcat [ ppr ev, ppr swapped, ppr co1, ppr gre, ppr ty1', ppr ty2 ]

+       ; recordUsedGRE gre

+       ; new_ev <- rewriteEqEvidence ev' (flipSwap swapped) redn2 redn1

+       -- ty1 is the one being unwrapped. Loop back to can_eq_nc with

+       -- the arguments flipped so that ty2 is looked at first in the

+       -- next iteration.  That way if we have (Id Rec) ~R# (Id Rec)

+       -- where newtype Id a = MkId a  and newtype Rec = MkRec Rec

+       -- we'll unwrap both Ids, then spot Rec=Rec.

+       -- See (END2) in Note [Eager newtype decomposition]

+       ; can_eq_nc False rdr_env envs new_ev ReprEq ty2 ps_ty2 ty1' ty1' }

+       ; if canDecomposeTcApp ev eq_rel tc1 inerts

+

+canDecomposeTcApp :: CtEvidence -> EqRel -> TyCon -> InertSet -> Bool

+canDecomposeTcApp ev eq_rel tc inerts

+  | isInjectiveTyCon tc eq_role = True

+  | isGiven ev                  = False

+  | otherwise                   = assert (eq_rel == ReprEq) $

+                                  assert (isNewTyCon tc ||

+                                          isDataFamilyTyCon tc ||

+                                          isAbstractTyCon tc ) $

+                                  noGivenNewtypeReprEqs tc inerts

+    -- The otherwise case deals with

+    --    * Representational equalities (T s1..sn) ~R# (T t1..tn)

+    --    * where T is a newtype or data family or abstract

+    -- Why? isInjectiveTyCon is always True for eq_rel=NomEq except for type

+    --   synonyms/families, neither of which happen here; and isInjectiveTyCon

+    --   is True for Representational for algebraic data types.

+    --

+    -- noGivenNewtypeReprEqs: see Note [Decomposing newtype equalities] (EX4)

+    --    Decomposing here is a last resort

+    -- NB: despite all these tests, decomposition of data familiies is alas

+    --     /still/ incomplete. See (EX3) in Note [Decomposing newtype equalities]

+  where

+    eq_role = eqRelRole eq_rel

+      and then the `tcUnwrapNewtype_maybe` call would fire and

+Note [Solving newtype equalities: overview]

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

+This Note also applies to data families, which we treat like

+newtype in case of 'newtype instance'.

+

+Consider (N s1..sn) ~R#  (N t1..tn), where N is a newtype.

+We try three strategies, in order:

+

+(NTE1) Decompose if the si/ti are either (a) identical or (b) phantom. This step

+   avoids unwrapping, which allows success in some cases where the newtype

+   would unwrap infinitely. See Note [Eager newtype decomposition]

+

+(NTE2) Unwrap the newtype, if possible.  Always good, but it requires the data

+   constructor to be in scope.  See Note [Unwrap newtypes first].

+

+   If the newtype is recursive, this unwrapping might go on forever,

+   so `can_eq_newtype_nc` has a depth bound check.

+   See Note [Newtypes can blow the stack]

+

+(NTE3) Decompose the tycon application.  This step is a last resort, because it

+   risks losing completeness. See Note [Decomposing newtype equalities]

+

+Note [Newtypes can blow the stack]

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

+Suppose we have

+

+  newtype X = MkX (Int -> X)

+  newtype Y = MkY (Int -> Y)

+

+and now wish to prove

+

+  [W] X ~R Y

+

+This Wanted will loop, expanding out the newtypes ever deeper looking

+for a solid match or a solid discrepancy. Indeed, there is something

+appropriate to this looping, because X and Y *do* have the same representation,

+in the limit -- they're both (Fix ((->) Int)). However, no finitely-sized

+coercion will ever witness it. This loop won't actually cause GHC to hang,

+though, because we check our depth in `can_eq_newtype_nc`.

+

+However, GHC can still loop badly: see #26757, which shows how we can create

+types whose size is exponential in the depth of newtype expansion. That makes

+GHC go out to lunch unless the depth bound is very small indeed; and a small

+depth bound makes perfectly legitimate programs fail.  We don't have solid

+solution for this, but it's rare.

+

+Note [Unwrap newtypes first]

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

+See also Note [Decomposing newtype equalities]

+

+Consider

+  newtype N m a = MkN (m a)

+N will get a conservative, Nominal role for its second parameter 'a',

+because it appears as an argument to the unknown 'm'. Now consider

+  [W] N Maybe a  ~R#  N Maybe b

+

+If we /decompose/, we'll get

+  [W] a ~N# b

+

+But if instead we /unwrap/ we'll get

+  [W] Maybe a ~R# Maybe b

+which in turn gives us

+  [W] a ~R# b

+which is easier to satisfy.

+

+Conclusion: we must unwrap newtypes before decomposing them. This happens

+in `can_eq_newtype_nc`

+

+We did flirt with making the /rewriter/ expand newtypes, rather than

+doing it in `can_eq_newtype_nc`.   But with recursive newtypes we want

+to be super-careful about expanding!

+

+   newtype A = MkA [A]   -- Recursive!

+

+   f :: A -> [A]

+   f = coerce

+

+We have [W] A ~R# [A].  If we rewrite [A], it'll expand to

+   [[[[[...]]]]]

+and blow the reduction stack.  See Note [Newtypes can blow the stack]

+in GHC.Tc.Solver.Rewrite.  But if we expand only the /top level/ of

+both sides, we get

+   [W] [A] ~R# [A]

+which we can, just, solve by reflexivity.

+

+So we simply unwrap, on-demand, at top level, in `can_eq_newtype_nc`.

+

+This is all very delicate. There is a real risk of a loop in the type checker

+with recursive newtypes -- but I think we're doomed to do *something*

+delicate, as we're really trying to solve for equirecursive type

+equality. Bottom line for users: recursive newtypes do not play well with type

+inference for representational equality.  See also Section 5.3.1 and 5.3.4 of

+"Safe Zero-cost Coercions for Haskell" (JFP 2016).

+

+See also Note [Decomposing newtype equalities].

+

+--- Historical side note ---

+

+We flirted with doing /both/ unwrap-at-top-level /and/ rewrite-deeply;

+see #22519.  But that didn't work: see discussion in #22924. Specifically

+we got a loop with a minor variation:

+   f2 :: a -> [A]

+   f2 = coerce

+

+Remember: Decomposing Wanteds is always /sound/.

+          This Note is only about /completeness/.

+

+There are three ways in which decomposing [W] (N ty1) ~r (N ty2) could be incomplete:

+  them.  This is done in `can_eq_nc`.  Of course, we can't unwrap if the data

+      [W] g1: D Int ~R# D alpha

+      [W] g2: alpha ~# Bool

+  If we solve g2 first, giving alpha:=Bool, then we can solve g1 easily:

+  leaving     [W] D Char ~#R D alpha

+  If we decompose now, we'll get (Char ~R# alpha), which is insoluble, since

+  alpha turns out to be Bool.

+* Incompleteness example (EX3)

+  Sadly, the fix for (EX2) is /still/ incomplete:

+     * The equality `g2` might be in a sibling implication constraint,

+       invisible for now.

+     * The equality `g2` might be hidden in a class constraint:

+          class C a

+          instance (a~Bool) => C [a]

+          [W] g3 :: C [alpha]

+       When we get around to solving `g3` we'll discover (g2:alpha~Bool)

+  So that's a real infelicity in the solver.

+

+* Incompleteness example (EX4): check available Givens

+Note [Eager newtype decomposition]

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

+Consider [W] (Rec1 Int) ~R#  (Rec1 Bool) where

+  newtype Rec1 a = MkRec1 (Rec1 a)

+

+If we apply (NTE2), we'll loop because `Rec1` unwraps forever.

+But the role of `a` is inferred as Phantom, so it sound and complete

+to decompose via `canDecomposableTyConAppOK`, giving nothing at all

+(because of the Phantom role).  So we win.

+

+Another useful special case is

+   newtype Rec = MkRec Rec

+where there are no arguments.

+

+So we do an eager decomposition check in step (NTE1), /before/ trying to unwrap

+in (NTE2).  This is a HACK: it catches some cases of recursion, but not all.

+But it's a hack that has been in GHC for some time.

+

+Wrinkles

+

+(END1) The eager-decomposition step is fine for all data types, not just newtypes.

+

+(END2) Consider    newtype Id a = MkId a      -- Not recusrive

+                   newtype Rec  = MkRec Rec   -- Recursive

+  and [W] Id Rec ~R#  Rec

+  Then (NTE1) will fail; (NTE2) will succeed in unwrapping Id, generating

+  [W] Rec ~R# Rec; and (NTE1) will succeed when we go round the loop.

+

+  What about [W] Rec ~R# Id Rec?

+  Here (NTE1) will fail again; (NTE2) will succeed, by unwrapping Rec, to get

+  Rec again.  If we just iterate with [W] Rec ~R# Id Rec, we'll be stuck in

+  a loop.  Instead we want to flip the constraint round so we get

+  [W] Id Rec ~R# Rec.  Now we win.  See the flipping in `can_eq_newtype_nc`.

+

+(END3) See Note [Even more eager newtype decomposition]

+

+Note [Even more eager newtype decomposition]

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

+Note [Eager newtype decomposition] decomposes [W] (N s ~R# N t) if N's role is

+phantom.  We could go further and decompose if the arguments are all Phantom

+/or/ Representational. This is not implemented.  For more details about the

+ideas in this Note see

+With the above rules, if there any Given Irreds, the Wanted is insoluble because

+we can't decompose it.  But in fact, if we look at the defn of IO, roughly,

+     if the roles of all N's arguments are representational (or phantom)

+If N's arguments really /are/ representational this will not lose completeness.

+Here "really are representational" means "if you expand all newtypes in N's RHS,

+we'd infer a representational role for each of N's type variables in that

+expansion".  See Note [Role inference] in GHC.Tc.TyCl.Utils.

+But the user might /override/ a phantom role with an explicit role annotation,

+and then we could (obscurely) get incompleteness.  Consider (#9117):

+   newtype Phant a = MkPhant Char

+   type role Phant representational  -- Override phantom role

+   [W] Phant Int ~R# Phant Char

+We do not want to decompose to Int ~R# Char; better to unwrap

+---- End of speculative aside ---------

+See (APT3) below.

+* At representational role, decomposition of Givens is unsound

+  (see (APT1) below), and decomposition of Wanteds is incomplete.

+requires a nominal role on its second argument. (See (APT3) for an example of

+(APT1) Decomposing a Given AppTy at Representational role is simply

+     For Wanteds, decomposing an AppTy at Representational role is incomplete.

+

+(APT2) What if we have  [W]  (f a) ~R# (f a)

+   We can't decompose because of (APT1).  But it's silly to reject.  So we do

+   an equality check, in the AppTy/AppTy case of `can_eq_nc`.

+

+   (It would be sound to do this reflexivity check in the Nominal case too,

+   but not necessary, and there might be a perf cost.)

+

+(APT3) The role on the AppCo coercion is a conservative choice, because we don't

+    runTcPluginTcS, recordUsedGRE,

+recordUsedGRE :: GlobalRdrElt -> TcS ()

+recordUsedGRE gre

+  = do { wrapTcS $ TcM.addUsedGRE NoDeprecationWarnings gre

+       ; wrapTcS $ TcM.keepAlive (greName gre) }

+- Implicit parameters and ``ImpredicativeTypes``.  GHC now knows

+  that if ``?foo::S`` is coecible to ``?foo::T`` only if ``S`` is coercible to ``T``.

+  Example (from :ghc-ticket:`#26737`)::

+

+    {-# LANGUAGE ImplicitParams, ImpredicativeTypes #-}

+    newtype N = MkN Int

+    test :: ((?foo::N) => Bool) -> ((?foo::Int) => Bool)

+    test = coerce

+

+  This is achieved by arranging that ``?foo :: T`` has a representational

+  role for ``T``.

+

+        GHC.Internal.Classes.IP

+             MultiParamTypeClasses, FunctionalDependencies,

+             UnboxedTuples #-}

+

+import GHC.Internal.Classes.IP

+{-# LANGUAGE Trustworthy #-}

+{-# LANGUAGE NoImplicitPrelude, MagicHash, StandaloneDeriving, BangPatterns,

+             KindSignatures, DataKinds, ConstraintKinds,

+              MultiParamTypeClasses, FunctionalDependencies #-}

+

+{-# LANGUAGE AllowAmbiguousTypes, RoleAnnotations, IncoherentInstances #-}

+  -- LANGUAGE pragmas: see Note [IP: implicit parameter class]

+

+{-# OPTIONS_HADDOCK not-home #-}

+-----------------------------------------------------------------------------

+-- |

+-- Module      :  GHC.Internal.Classes.IP

+-- Copyright   :  (c) The University of Glasgow, 1992-2002

+-- License     :  see libraries/base/LICENSE

+--

+-- Maintainer  :  ghc-devs@haskell.org

+-- Stability   :  internal

+-- Portability :  non-portable (GHC extensions)

+--

+-- Basic classes.

+-- Do not import this module directly.  It is an GHC internal only

+-- module.  Some of its contents are instead available from @Prelude@

+-- and @GHC.Int@.

+--

+-----------------------------------------------------------------------------

+

+module GHC.Internal.Classes.IP( IP(..)) where

+

+import GHC.Internal.Types

+

+

+default ()              -- Double isn't available yet

+

+-- | The syntax @?x :: a@ is desugared into @IP "x" a@

+-- IP is declared very early, so that libraries can take

+-- advantage of the implicit-call-stack feature