never executed always true always false
    1 {-# LANGUAGE FlexibleContexts    #-}
    2 {-# LANGUAGE RankNTypes          #-}
    3 {-# LANGUAGE ScopedTypeVariables #-}
    4 
    5 {-
    6 (c) The University of Glasgow 2006
    7 -}
    8 
    9 -- | Module for (a) type kinds and (b) type coercions,
   10 -- as used in System FC. See 'GHC.Core.Expr' for
   11 -- more on System FC and how coercions fit into it.
   12 --
   13 module GHC.Core.Coercion (
   14         -- * Main data type
   15         Coercion, CoercionN, CoercionR, CoercionP, MCoercion(..), MCoercionN, MCoercionR,
   16         UnivCoProvenance, CoercionHole(..),
   17         coHoleCoVar, setCoHoleCoVar,
   18         LeftOrRight(..),
   19         Var, CoVar, TyCoVar,
   20         Role(..), ltRole,
   21 
   22         -- ** Functions over coercions
   23         coVarTypes, coVarKind, coVarKindsTypesRole, coVarRole,
   24         coercionType, mkCoercionType,
   25         coercionKind, coercionLKind, coercionRKind,coercionKinds,
   26         coercionRole, coercionKindRole,
   27 
   28         -- ** Constructing coercions
   29         mkGReflCo, mkReflCo, mkRepReflCo, mkNomReflCo,
   30         mkCoVarCo, mkCoVarCos,
   31         mkAxInstCo, mkUnbranchedAxInstCo,
   32         mkAxInstRHS, mkUnbranchedAxInstRHS,
   33         mkAxInstLHS, mkUnbranchedAxInstLHS,
   34         mkPiCo, mkPiCos, mkCoCast,
   35         mkSymCo, mkTransCo,
   36         mkNthCo, mkNthCoFunCo, nthCoRole, mkLRCo,
   37         mkInstCo, mkAppCo, mkAppCos, mkTyConAppCo, mkFunCo, mkFunResCo,
   38         mkForAllCo, mkForAllCos, mkHomoForAllCos,
   39         mkPhantomCo,
   40         mkHoleCo, mkUnivCo, mkSubCo,
   41         mkAxiomInstCo, mkProofIrrelCo,
   42         downgradeRole, mkAxiomRuleCo,
   43         mkGReflRightCo, mkGReflLeftCo, mkCoherenceLeftCo, mkCoherenceRightCo,
   44         mkKindCo,
   45         castCoercionKind, castCoercionKind1, castCoercionKind2,
   46         mkFamilyTyConAppCo,
   47 
   48         mkHeteroCoercionType,
   49         mkPrimEqPred, mkReprPrimEqPred, mkPrimEqPredRole,
   50         mkHeteroPrimEqPred, mkHeteroReprPrimEqPred,
   51 
   52         -- ** Decomposition
   53         instNewTyCon_maybe,
   54 
   55         NormaliseStepper, NormaliseStepResult(..), composeSteppers,
   56         mapStepResult, unwrapNewTypeStepper,
   57         topNormaliseNewType_maybe, topNormaliseTypeX,
   58 
   59         decomposeCo, decomposeFunCo, decomposePiCos, getCoVar_maybe,
   60         splitTyConAppCo_maybe,
   61         splitAppCo_maybe,
   62         splitFunCo_maybe,
   63         splitForAllCo_maybe,
   64         splitForAllCo_ty_maybe, splitForAllCo_co_maybe,
   65 
   66         nthRole, tyConRolesX, tyConRolesRepresentational, setNominalRole_maybe,
   67 
   68         pickLR,
   69 
   70         isGReflCo, isReflCo, isReflCo_maybe, isGReflCo_maybe, isReflexiveCo, isReflexiveCo_maybe,
   71         isReflCoVar_maybe, isGReflMCo, mkGReflLeftMCo, mkGReflRightMCo,
   72         mkCoherenceRightMCo,
   73 
   74         coToMCo, mkTransMCo, mkTransMCoL, mkTransMCoR, mkCastTyMCo, mkSymMCo,
   75         mkHomoForAllMCo, mkFunResMCo, mkPiMCos,
   76         isReflMCo, checkReflexiveMCo,
   77 
   78         -- ** Coercion variables
   79         mkCoVar, isCoVar, coVarName, setCoVarName, setCoVarUnique,
   80         isCoVar_maybe,
   81 
   82         -- ** Free variables
   83         tyCoVarsOfCo, tyCoVarsOfCos, coVarsOfCo,
   84         tyCoFVsOfCo, tyCoFVsOfCos, tyCoVarsOfCoDSet,
   85         coercionSize, anyFreeVarsOfCo,
   86 
   87         -- ** Substitution
   88         CvSubstEnv, emptyCvSubstEnv,
   89         lookupCoVar,
   90         substCo, substCos, substCoVar, substCoVars, substCoWith,
   91         substCoVarBndr,
   92         extendTvSubstAndInScope, getCvSubstEnv,
   93 
   94         -- ** Lifting
   95         liftCoSubst, liftCoSubstTyVar, liftCoSubstWith, liftCoSubstWithEx,
   96         emptyLiftingContext, extendLiftingContext, extendLiftingContextAndInScope,
   97         liftCoSubstVarBndrUsing, isMappedByLC,
   98 
   99         mkSubstLiftingContext, zapLiftingContext,
  100         substForAllCoBndrUsingLC, lcTCvSubst, lcInScopeSet,
  101 
  102         LiftCoEnv, LiftingContext(..), liftEnvSubstLeft, liftEnvSubstRight,
  103         substRightCo, substLeftCo, swapLiftCoEnv, lcSubstLeft, lcSubstRight,
  104 
  105         -- ** Comparison
  106         eqCoercion, eqCoercionX,
  107 
  108         -- ** Forcing evaluation of coercions
  109         seqCo,
  110 
  111         -- * Pretty-printing
  112         pprCo, pprParendCo,
  113         pprCoAxiom, pprCoAxBranch, pprCoAxBranchLHS,
  114         pprCoAxBranchUser, tidyCoAxBndrsForUser,
  115         etaExpandCoAxBranch,
  116 
  117         -- * Tidying
  118         tidyCo, tidyCos,
  119 
  120         -- * Other
  121         promoteCoercion, buildCoercion,
  122 
  123         multToCo,
  124 
  125         hasCoercionHoleTy, hasCoercionHoleCo,
  126         HoleSet, coercionHolesOfType, coercionHolesOfCo
  127        ) where
  128 
  129 import {-# SOURCE #-} GHC.CoreToIface (toIfaceTyCon, tidyToIfaceTcArgs)
  130 
  131 import GHC.Prelude
  132 
  133 import GHC.Iface.Type
  134 import GHC.Core.TyCo.Rep
  135 import GHC.Core.TyCo.FVs
  136 import GHC.Core.TyCo.Ppr
  137 import GHC.Core.TyCo.Subst
  138 import GHC.Core.TyCo.Tidy
  139 import GHC.Core.Type
  140 import GHC.Core.TyCon
  141 import GHC.Core.TyCon.RecWalk
  142 import GHC.Core.Coercion.Axiom
  143 import {-# SOURCE #-} GHC.Core.Utils ( mkFunctionType )
  144 import GHC.Types.Var
  145 import GHC.Types.Var.Env
  146 import GHC.Types.Var.Set
  147 import GHC.Types.Name hiding ( varName )
  148 import GHC.Types.Basic
  149 import GHC.Types.Unique
  150 import GHC.Data.Pair
  151 import GHC.Types.SrcLoc
  152 import GHC.Builtin.Names
  153 import GHC.Builtin.Types.Prim
  154 import GHC.Data.List.SetOps
  155 import GHC.Data.Maybe
  156 import GHC.Types.Unique.FM
  157 import GHC.Types.Unique.Set
  158 
  159 import GHC.Utils.Misc
  160 import GHC.Utils.Outputable
  161 import GHC.Utils.Panic
  162 import GHC.Utils.Panic.Plain
  163 
  164 import Control.Monad (foldM, zipWithM)
  165 import Data.Function ( on )
  166 import Data.Char( isDigit )
  167 import qualified Data.Monoid as Monoid
  168 
  169 {-
  170 %************************************************************************
  171 %*                                                                      *
  172      -- The coercion arguments always *precisely* saturate
  173      -- arity of (that branch of) the CoAxiom.  If there are
  174      -- any left over, we use AppCo.  See
  175      -- See [Coercion axioms applied to coercions] in GHC.Core.TyCo.Rep
  176 
  177 \subsection{Coercion variables}
  178 %*                                                                      *
  179 %************************************************************************
  180 -}
  181 
  182 coVarName :: CoVar -> Name
  183 coVarName = varName
  184 
  185 setCoVarUnique :: CoVar -> Unique -> CoVar
  186 setCoVarUnique = setVarUnique
  187 
  188 setCoVarName :: CoVar -> Name -> CoVar
  189 setCoVarName   = setVarName
  190 
  191 {-
  192 %************************************************************************
  193 %*                                                                      *
  194                    Pretty-printing CoAxioms
  195 %*                                                                      *
  196 %************************************************************************
  197 
  198 Defined here to avoid module loops. CoAxiom is loaded very early on.
  199 
  200 -}
  201 
  202 etaExpandCoAxBranch :: CoAxBranch -> ([TyVar], [Type], Type)
  203 -- Return the (tvs,lhs,rhs) after eta-expanding,
  204 -- to the way in which the axiom was originally written
  205 -- See Note [Eta reduction for data families] in GHC.Core.Coercion.Axiom
  206 etaExpandCoAxBranch (CoAxBranch { cab_tvs = tvs
  207                                 , cab_eta_tvs = eta_tvs
  208                                 , cab_lhs = lhs
  209                                 , cab_rhs = rhs })
  210   -- ToDo: what about eta_cvs?
  211   = (tvs ++ eta_tvs, lhs ++ eta_tys, mkAppTys rhs eta_tys)
  212  where
  213     eta_tys = mkTyVarTys eta_tvs
  214 
  215 pprCoAxiom :: CoAxiom br -> SDoc
  216 -- Used in debug-printing only
  217 pprCoAxiom ax@(CoAxiom { co_ax_tc = tc, co_ax_branches = branches })
  218   = hang (text "axiom" <+> ppr ax <+> dcolon)
  219        2 (vcat (map (pprCoAxBranchUser tc) (fromBranches branches)))
  220 
  221 pprCoAxBranchUser :: TyCon -> CoAxBranch -> SDoc
  222 -- Used when printing injectivity errors (FamInst.reportInjectivityErrors)
  223 -- and inaccessible branches (GHC.Tc.Validity.inaccessibleCoAxBranch)
  224 -- This happens in error messages: don't print the RHS of a data
  225 --   family axiom, which is meaningless to a user
  226 pprCoAxBranchUser tc br
  227   | isDataFamilyTyCon tc = pprCoAxBranchLHS tc br
  228   | otherwise            = pprCoAxBranch    tc br
  229 
  230 pprCoAxBranchLHS :: TyCon -> CoAxBranch -> SDoc
  231 -- Print the family-instance equation when reporting
  232 --   a conflict between equations (FamInst.conflictInstErr)
  233 -- For type families the RHS is important; for data families not so.
  234 --   Indeed for data families the RHS is a mysterious internal
  235 --   type constructor, so we suppress it (#14179)
  236 -- See FamInstEnv Note [Family instance overlap conflicts]
  237 pprCoAxBranchLHS = ppr_co_ax_branch pp_rhs
  238   where
  239     pp_rhs _ _ = empty
  240 
  241 pprCoAxBranch :: TyCon -> CoAxBranch -> SDoc
  242 pprCoAxBranch = ppr_co_ax_branch ppr_rhs
  243   where
  244     ppr_rhs env rhs = equals <+> pprPrecTypeX env topPrec rhs
  245 
  246 ppr_co_ax_branch :: (TidyEnv -> Type -> SDoc)
  247                  -> TyCon -> CoAxBranch -> SDoc
  248 ppr_co_ax_branch ppr_rhs fam_tc branch
  249   = foldr1 (flip hangNotEmpty 2)
  250     [ pprUserForAll (mkTyCoVarBinders Inferred bndrs')
  251          -- See Note [Printing foralls in type family instances] in GHC.Iface.Type
  252     , pp_lhs <+> ppr_rhs tidy_env ee_rhs
  253     , text "-- Defined" <+> pp_loc ]
  254   where
  255     loc = coAxBranchSpan branch
  256     pp_loc | isGoodSrcSpan loc = text "at" <+> ppr (srcSpanStart loc)
  257            | otherwise         = text "in" <+> ppr loc
  258 
  259     -- Eta-expand LHS and RHS types, because sometimes data family
  260     -- instances are eta-reduced.
  261     -- See Note [Eta reduction for data families] in GHC.Core.Coercion.Axiom.
  262     (ee_tvs, ee_lhs, ee_rhs) = etaExpandCoAxBranch branch
  263 
  264     pp_lhs = pprIfaceTypeApp topPrec (toIfaceTyCon fam_tc)
  265                              (tidyToIfaceTcArgs tidy_env fam_tc ee_lhs)
  266 
  267     (tidy_env, bndrs') = tidyCoAxBndrsForUser emptyTidyEnv ee_tvs
  268 
  269 tidyCoAxBndrsForUser :: TidyEnv -> [Var] -> (TidyEnv, [Var])
  270 -- Tidy wildcards "_1", "_2" to "_", and do not return them
  271 -- in the list of binders to be printed
  272 -- This is so that in error messages we see
  273 --     forall a. F _ [a] _ = ...
  274 -- rather than
  275 --     forall a _1 _2. F _1 [a] _2 = ...
  276 --
  277 -- This is a rather disgusting function
  278 -- See Note [Wildcard names] in GHC.Tc.Gen.HsType
  279 tidyCoAxBndrsForUser init_env tcvs
  280   = (tidy_env, reverse tidy_bndrs)
  281   where
  282     (tidy_env, tidy_bndrs) = foldl tidy_one (init_env, []) tcvs
  283 
  284     tidy_one (env@(occ_env, subst), rev_bndrs') bndr
  285       | is_wildcard bndr = (env_wild, rev_bndrs')
  286       | otherwise        = (env',     bndr' : rev_bndrs')
  287       where
  288         (env', bndr') = tidyVarBndr env bndr
  289         env_wild = (occ_env, extendVarEnv subst bndr wild_bndr)
  290         wild_bndr = setVarName bndr $
  291                     tidyNameOcc (varName bndr) (mkTyVarOcc "_")
  292                     -- Tidy the binder to "_"
  293 
  294     is_wildcard :: Var -> Bool
  295     is_wildcard tv = case occNameString (getOccName tv) of
  296                        ('_' : rest) -> all isDigit rest
  297                        _            -> False
  298 
  299 
  300 {- *********************************************************************
  301 *                                                                      *
  302               MCoercion
  303 *                                                                      *
  304 ********************************************************************* -}
  305 
  306 coToMCo :: Coercion -> MCoercion
  307 -- Convert a coercion to a MCoercion,
  308 -- It's not clear whether or not isReflexiveCo would be better here
  309 coToMCo co | isReflCo co = MRefl
  310            | otherwise   = MCo co
  311 
  312 checkReflexiveMCo :: MCoercion -> MCoercion
  313 checkReflexiveMCo MRefl                       = MRefl
  314 checkReflexiveMCo (MCo co) | isReflexiveCo co = MRefl
  315                            | otherwise        = MCo co
  316 
  317 -- | Tests if this MCoercion is obviously generalized reflexive
  318 -- Guaranteed to work very quickly.
  319 isGReflMCo :: MCoercion -> Bool
  320 isGReflMCo MRefl = True
  321 isGReflMCo (MCo co) | isGReflCo co = True
  322 isGReflMCo _ = False
  323 
  324 -- | Make a generalized reflexive coercion
  325 mkGReflCo :: Role -> Type -> MCoercionN -> Coercion
  326 mkGReflCo r ty mco
  327   | isGReflMCo mco = if r == Nominal then Refl ty
  328                      else GRefl r ty MRefl
  329   | otherwise    = GRefl r ty mco
  330 
  331 -- | Compose two MCoercions via transitivity
  332 mkTransMCo :: MCoercion -> MCoercion -> MCoercion
  333 mkTransMCo MRefl     co2       = co2
  334 mkTransMCo co1       MRefl     = co1
  335 mkTransMCo (MCo co1) (MCo co2) = MCo (mkTransCo co1 co2)
  336 
  337 mkTransMCoL :: MCoercion -> Coercion -> MCoercion
  338 mkTransMCoL MRefl     co2 = MCo co2
  339 mkTransMCoL (MCo co1) co2 = MCo (mkTransCo co1 co2)
  340 
  341 mkTransMCoR :: Coercion -> MCoercion -> MCoercion
  342 mkTransMCoR co1 MRefl     = coToMCo co1
  343 mkTransMCoR co1 (MCo co2) = MCo (mkTransCo co1 co2)
  344 
  345 -- | Get the reverse of an 'MCoercion'
  346 mkSymMCo :: MCoercion -> MCoercion
  347 mkSymMCo MRefl    = MRefl
  348 mkSymMCo (MCo co) = MCo (mkSymCo co)
  349 
  350 -- | Cast a type by an 'MCoercion'
  351 mkCastTyMCo :: Type -> MCoercion -> Type
  352 mkCastTyMCo ty MRefl    = ty
  353 mkCastTyMCo ty (MCo co) = ty `mkCastTy` co
  354 
  355 mkHomoForAllMCo :: TyCoVar -> MCoercion -> MCoercion
  356 mkHomoForAllMCo _   MRefl    = MRefl
  357 mkHomoForAllMCo tcv (MCo co) = MCo (mkHomoForAllCos [tcv] co)
  358 
  359 mkPiMCos :: [Var] -> MCoercion -> MCoercion
  360 mkPiMCos _ MRefl = MRefl
  361 mkPiMCos vs (MCo co) = MCo (mkPiCos Representational vs co)
  362 
  363 mkFunResMCo :: Scaled Type -> MCoercionR -> MCoercionR
  364 mkFunResMCo _      MRefl    = MRefl
  365 mkFunResMCo arg_ty (MCo co) = MCo (mkFunResCo Representational arg_ty co)
  366 
  367 mkGReflLeftMCo :: Role -> Type -> MCoercionN -> Coercion
  368 mkGReflLeftMCo r ty MRefl    = mkReflCo r ty
  369 mkGReflLeftMCo r ty (MCo co) = mkGReflLeftCo r ty co
  370 
  371 mkGReflRightMCo :: Role -> Type -> MCoercionN -> Coercion
  372 mkGReflRightMCo r ty MRefl    = mkReflCo r ty
  373 mkGReflRightMCo r ty (MCo co) = mkGReflRightCo r ty co
  374 
  375 -- | Like 'mkCoherenceRightCo', but with an 'MCoercion'
  376 mkCoherenceRightMCo :: Role -> Type -> MCoercionN -> Coercion -> Coercion
  377 mkCoherenceRightMCo _ _  MRefl    co2 = co2
  378 mkCoherenceRightMCo r ty (MCo co) co2 = mkCoherenceRightCo r ty co co2
  379 
  380 isReflMCo :: MCoercion -> Bool
  381 isReflMCo MRefl = True
  382 isReflMCo _     = False
  383 
  384 {-
  385 %************************************************************************
  386 %*                                                                      *
  387         Destructing coercions
  388 %*                                                                      *
  389 %************************************************************************
  390 
  391 Note [Function coercions]
  392 ~~~~~~~~~~~~~~~~~~~~~~~~~
  393 Remember that
  394   (->) :: forall {r1} {r2}. TYPE r1 -> TYPE r2 -> TYPE LiftedRep
  395 whose `RuntimeRep' arguments are intentionally marked inferred to
  396 avoid type application.
  397 
  398 Hence
  399   FunCo r mult co1 co2 :: (s1->t1) ~r (s2->t2)
  400 is short for
  401   TyConAppCo (->) mult co_rep1 co_rep2 co1 co2
  402 where co_rep1, co_rep2 are the coercions on the representations.
  403 -}
  404 
  405 
  406 -- | This breaks a 'Coercion' with type @T A B C ~ T D E F@ into
  407 -- a list of 'Coercion's of kinds @A ~ D@, @B ~ E@ and @E ~ F@. Hence:
  408 --
  409 -- > decomposeCo 3 c [r1, r2, r3] = [nth r1 0 c, nth r2 1 c, nth r3 2 c]
  410 decomposeCo :: Arity -> Coercion
  411             -> [Role]  -- the roles of the output coercions
  412                        -- this must have at least as many
  413                        -- entries as the Arity provided
  414             -> [Coercion]
  415 decomposeCo arity co rs
  416   = [mkNthCo r n co | (n,r) <- [0..(arity-1)] `zip` rs ]
  417            -- Remember, Nth is zero-indexed
  418 
  419 decomposeFunCo :: HasDebugCallStack
  420                => Role      -- Role of the input coercion
  421                -> Coercion  -- Input coercion
  422                -> (CoercionN, Coercion, Coercion)
  423 -- Expects co :: (s1 -> t1) ~ (s2 -> t2)
  424 -- Returns (co1 :: s1~s2, co2 :: t1~t2)
  425 -- See Note [Function coercions] for the "3" and "4"
  426 
  427 decomposeFunCo _ (FunCo _ w co1 co2) = (w, co1, co2)
  428    -- Short-circuits the calls to mkNthCo
  429 
  430 decomposeFunCo r co = assertPpr all_ok (ppr co)
  431                       (mkNthCo Nominal 0 co, mkNthCo r 3 co, mkNthCo r 4 co)
  432   where
  433     Pair s1t1 s2t2 = coercionKind co
  434     all_ok = isFunTy s1t1 && isFunTy s2t2
  435 
  436 {- Note [Pushing a coercion into a pi-type]
  437 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  438 Suppose we have this:
  439     (f |> co) t1 .. tn
  440 Then we want to push the coercion into the arguments, so as to make
  441 progress. For example of why you might want to do so, see Note
  442 [Respecting definitional equality] in GHC.Core.TyCo.Rep.
  443 
  444 This is done by decomposePiCos.  Specifically, if
  445     decomposePiCos co [t1,..,tn] = ([co1,...,cok], cor)
  446 then
  447     (f |> co) t1 .. tn   =   (f (t1 |> co1) ... (tk |> cok)) |> cor) t(k+1) ... tn
  448 
  449 Notes:
  450 
  451 * k can be smaller than n! That is decomposePiCos can return *fewer*
  452   coercions than there are arguments (ie k < n), if the kind provided
  453   doesn't have enough binders.
  454 
  455 * If there is a type error, we might see
  456        (f |> co) t1
  457   where co :: (forall a. ty) ~ (ty1 -> ty2)
  458   Here 'co' is insoluble, but we don't want to crash in decoposePiCos.
  459   So decomposePiCos carefully tests both sides of the coercion to check
  460   they are both foralls or both arrows.  Not doing this caused #15343.
  461 -}
  462 
  463 decomposePiCos :: HasDebugCallStack
  464                => CoercionN -> Pair Type  -- Coercion and its kind
  465                -> [Type]
  466                -> ([CoercionN], CoercionN)
  467 -- See Note [Pushing a coercion into a pi-type]
  468 decomposePiCos orig_co (Pair orig_k1 orig_k2) orig_args
  469   = go [] (orig_subst,orig_k1) orig_co (orig_subst,orig_k2) orig_args
  470   where
  471     orig_subst = mkEmptyTCvSubst $ mkInScopeSet $
  472                  tyCoVarsOfTypes orig_args `unionVarSet` tyCoVarsOfCo orig_co
  473 
  474     go :: [CoercionN]      -- accumulator for argument coercions, reversed
  475        -> (TCvSubst,Kind)  -- Lhs kind of coercion
  476        -> CoercionN        -- coercion originally applied to the function
  477        -> (TCvSubst,Kind)  -- Rhs kind of coercion
  478        -> [Type]           -- Arguments to that function
  479        -> ([CoercionN], Coercion)
  480     -- Invariant:  co :: subst1(k1) ~ subst2(k2)
  481 
  482     go acc_arg_cos (subst1,k1) co (subst2,k2) (ty:tys)
  483       | Just (a, t1) <- splitForAllTyCoVar_maybe k1
  484       , Just (b, t2) <- splitForAllTyCoVar_maybe k2
  485         -- know     co :: (forall a:s1.t1) ~ (forall b:s2.t2)
  486         --    function :: forall a:s1.t1   (the function is not passed to decomposePiCos)
  487         --           a :: s1
  488         --           b :: s2
  489         --          ty :: s2
  490         -- need arg_co :: s2 ~ s1
  491         --      res_co :: t1[ty |> arg_co / a] ~ t2[ty / b]
  492       = let arg_co  = mkNthCo Nominal 0 (mkSymCo co)
  493             res_co  = mkInstCo co (mkGReflLeftCo Nominal ty arg_co)
  494             subst1' = extendTCvSubst subst1 a (ty `CastTy` arg_co)
  495             subst2' = extendTCvSubst subst2 b ty
  496         in
  497         go (arg_co : acc_arg_cos) (subst1', t1) res_co (subst2', t2) tys
  498 
  499       | Just (_w1, _s1, t1) <- splitFunTy_maybe k1
  500       , Just (_w1, _s2, t2) <- splitFunTy_maybe k2
  501         -- know     co :: (s1 -> t1) ~ (s2 -> t2)
  502         --    function :: s1 -> t1
  503         --          ty :: s2
  504         -- need arg_co :: s2 ~ s1
  505         --      res_co :: t1 ~ t2
  506       = let (_, sym_arg_co, res_co) = decomposeFunCo Nominal co
  507             -- It should be fine to ignore the multiplicity bit of the coercion
  508             -- for a Nominal coercion.
  509             arg_co               = mkSymCo sym_arg_co
  510         in
  511         go (arg_co : acc_arg_cos) (subst1,t1) res_co (subst2,t2) tys
  512 
  513       | not (isEmptyTCvSubst subst1) || not (isEmptyTCvSubst subst2)
  514       = go acc_arg_cos (zapTCvSubst subst1, substTy subst1 k1)
  515                        co
  516                        (zapTCvSubst subst2, substTy subst1 k2)
  517                        (ty:tys)
  518 
  519       -- tys might not be empty, if the left-hand type of the original coercion
  520       -- didn't have enough binders
  521     go acc_arg_cos _ki1 co _ki2 _tys = (reverse acc_arg_cos, co)
  522 
  523 -- | Attempts to obtain the type variable underlying a 'Coercion'
  524 getCoVar_maybe :: Coercion -> Maybe CoVar
  525 getCoVar_maybe (CoVarCo cv) = Just cv
  526 getCoVar_maybe _            = Nothing
  527 
  528 -- | Attempts to tease a coercion apart into a type constructor and the application
  529 -- of a number of coercion arguments to that constructor
  530 splitTyConAppCo_maybe :: Coercion -> Maybe (TyCon, [Coercion])
  531 splitTyConAppCo_maybe co
  532   | Just (ty, r) <- isReflCo_maybe co
  533   = do { (tc, tys) <- splitTyConApp_maybe ty
  534        ; let args = zipWith mkReflCo (tyConRolesX r tc) tys
  535        ; return (tc, args) }
  536 splitTyConAppCo_maybe (TyConAppCo _ tc cos) = Just (tc, cos)
  537 splitTyConAppCo_maybe (FunCo _ w arg res)     = Just (funTyCon, cos)
  538   where cos = [w, mkRuntimeRepCo arg, mkRuntimeRepCo res, arg, res]
  539 splitTyConAppCo_maybe _                     = Nothing
  540 
  541 multToCo :: Mult -> Coercion
  542 multToCo r = mkNomReflCo r
  543 
  544 -- first result has role equal to input; third result is Nominal
  545 splitAppCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
  546 -- ^ Attempt to take a coercion application apart.
  547 splitAppCo_maybe (AppCo co arg) = Just (co, arg)
  548 splitAppCo_maybe (TyConAppCo r tc args)
  549   | args `lengthExceeds` tyConArity tc
  550   , Just (args', arg') <- snocView args
  551   = Just ( mkTyConAppCo r tc args', arg' )
  552 
  553   | not (mustBeSaturated tc)
  554     -- Never create unsaturated type family apps!
  555   , Just (args', arg') <- snocView args
  556   , Just arg'' <- setNominalRole_maybe (nthRole r tc (length args')) arg'
  557   = Just ( mkTyConAppCo r tc args', arg'' )
  558        -- Use mkTyConAppCo to preserve the invariant
  559        --  that identity coercions are always represented by Refl
  560 
  561 splitAppCo_maybe co
  562   | Just (ty, r) <- isReflCo_maybe co
  563   , Just (ty1, ty2) <- splitAppTy_maybe ty
  564   = Just (mkReflCo r ty1, mkNomReflCo ty2)
  565 splitAppCo_maybe _ = Nothing
  566 
  567 -- Only used in specialise/Rules
  568 splitFunCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
  569 splitFunCo_maybe (FunCo _ _ arg res) = Just (arg, res)
  570 splitFunCo_maybe _ = Nothing
  571 
  572 splitForAllCo_maybe :: Coercion -> Maybe (TyCoVar, Coercion, Coercion)
  573 splitForAllCo_maybe (ForAllCo tv k_co co) = Just (tv, k_co, co)
  574 splitForAllCo_maybe _                     = Nothing
  575 
  576 -- | Like 'splitForAllCo_maybe', but only returns Just for tyvar binder
  577 splitForAllCo_ty_maybe :: Coercion -> Maybe (TyVar, Coercion, Coercion)
  578 splitForAllCo_ty_maybe (ForAllCo tv k_co co)
  579   | isTyVar tv = Just (tv, k_co, co)
  580 splitForAllCo_ty_maybe _ = Nothing
  581 
  582 -- | Like 'splitForAllCo_maybe', but only returns Just for covar binder
  583 splitForAllCo_co_maybe :: Coercion -> Maybe (CoVar, Coercion, Coercion)
  584 splitForAllCo_co_maybe (ForAllCo cv k_co co)
  585   | isCoVar cv = Just (cv, k_co, co)
  586 splitForAllCo_co_maybe _ = Nothing
  587 
  588 -------------------------------------------------------
  589 -- and some coercion kind stuff
  590 
  591 coVarLType, coVarRType :: HasDebugCallStack => CoVar -> Type
  592 coVarLType cv | (_, _, ty1, _, _) <- coVarKindsTypesRole cv = ty1
  593 coVarRType cv | (_, _, _, ty2, _) <- coVarKindsTypesRole cv = ty2
  594 
  595 coVarTypes :: HasDebugCallStack => CoVar -> Pair Type
  596 coVarTypes cv
  597   | (_, _, ty1, ty2, _) <- coVarKindsTypesRole cv
  598   = Pair ty1 ty2
  599 
  600 coVarKindsTypesRole :: HasDebugCallStack => CoVar -> (Kind,Kind,Type,Type,Role)
  601 coVarKindsTypesRole cv
  602  | Just (tc, [k1,k2,ty1,ty2]) <- splitTyConApp_maybe (varType cv)
  603  = (k1, k2, ty1, ty2, eqTyConRole tc)
  604  | otherwise
  605  = pprPanic "coVarKindsTypesRole, non coercion variable"
  606             (ppr cv $$ ppr (varType cv))
  607 
  608 coVarKind :: CoVar -> Type
  609 coVarKind cv
  610   = assert (isCoVar cv )
  611     varType cv
  612 
  613 coVarRole :: CoVar -> Role
  614 coVarRole cv
  615   = eqTyConRole (case tyConAppTyCon_maybe (varType cv) of
  616                    Just tc0 -> tc0
  617                    Nothing  -> pprPanic "coVarRole: not tyconapp" (ppr cv))
  618 
  619 eqTyConRole :: TyCon -> Role
  620 -- Given (~#) or (~R#) return the Nominal or Representational respectively
  621 eqTyConRole tc
  622   | tc `hasKey` eqPrimTyConKey
  623   = Nominal
  624   | tc `hasKey` eqReprPrimTyConKey
  625   = Representational
  626   | otherwise
  627   = pprPanic "eqTyConRole: unknown tycon" (ppr tc)
  628 
  629 -- | Given a coercion @co1 :: (a :: TYPE r1) ~ (b :: TYPE r2)@,
  630 -- produce a coercion @rep_co :: r1 ~ r2@.
  631 mkRuntimeRepCo :: HasDebugCallStack => Coercion -> Coercion
  632 mkRuntimeRepCo co
  633   = mkNthCo Nominal 0 kind_co
  634   where
  635     kind_co = mkKindCo co  -- kind_co :: TYPE r1 ~ TYPE r2
  636                            -- (up to silliness with Constraint)
  637 
  638 isReflCoVar_maybe :: Var -> Maybe Coercion
  639 -- If cv :: t~t then isReflCoVar_maybe cv = Just (Refl t)
  640 -- Works on all kinds of Vars, not just CoVars
  641 isReflCoVar_maybe cv
  642   | isCoVar cv
  643   , Pair ty1 ty2 <- coVarTypes cv
  644   , ty1 `eqType` ty2
  645   = Just (mkReflCo (coVarRole cv) ty1)
  646   | otherwise
  647   = Nothing
  648 
  649 -- | Tests if this coercion is obviously a generalized reflexive coercion.
  650 -- Guaranteed to work very quickly.
  651 isGReflCo :: Coercion -> Bool
  652 isGReflCo (GRefl{}) = True
  653 isGReflCo (Refl{})  = True -- Refl ty == GRefl N ty MRefl
  654 isGReflCo _         = False
  655 
  656 -- | Tests if this coercion is obviously reflexive. Guaranteed to work
  657 -- very quickly. Sometimes a coercion can be reflexive, but not obviously
  658 -- so. c.f. 'isReflexiveCo'
  659 isReflCo :: Coercion -> Bool
  660 isReflCo (Refl{}) = True
  661 isReflCo (GRefl _ _ mco) | isGReflMCo mco = True
  662 isReflCo _ = False
  663 
  664 -- | Returns the type coerced if this coercion is a generalized reflexive
  665 -- coercion. Guaranteed to work very quickly.
  666 isGReflCo_maybe :: Coercion -> Maybe (Type, Role)
  667 isGReflCo_maybe (GRefl r ty _) = Just (ty, r)
  668 isGReflCo_maybe (Refl ty)      = Just (ty, Nominal)
  669 isGReflCo_maybe _ = Nothing
  670 
  671 -- | Returns the type coerced if this coercion is reflexive. Guaranteed
  672 -- to work very quickly. Sometimes a coercion can be reflexive, but not
  673 -- obviously so. c.f. 'isReflexiveCo_maybe'
  674 isReflCo_maybe :: Coercion -> Maybe (Type, Role)
  675 isReflCo_maybe (Refl ty) = Just (ty, Nominal)
  676 isReflCo_maybe (GRefl r ty mco) | isGReflMCo mco = Just (ty, r)
  677 isReflCo_maybe _ = Nothing
  678 
  679 -- | Slowly checks if the coercion is reflexive. Don't call this in a loop,
  680 -- as it walks over the entire coercion.
  681 isReflexiveCo :: Coercion -> Bool
  682 isReflexiveCo = isJust . isReflexiveCo_maybe
  683 
  684 -- | Extracts the coerced type from a reflexive coercion. This potentially
  685 -- walks over the entire coercion, so avoid doing this in a loop.
  686 isReflexiveCo_maybe :: Coercion -> Maybe (Type, Role)
  687 isReflexiveCo_maybe (Refl ty) = Just (ty, Nominal)
  688 isReflexiveCo_maybe (GRefl r ty mco) | isGReflMCo mco = Just (ty, r)
  689 isReflexiveCo_maybe co
  690   | ty1 `eqType` ty2
  691   = Just (ty1, r)
  692   | otherwise
  693   = Nothing
  694   where (Pair ty1 ty2, r) = coercionKindRole co
  695 
  696 
  697 {-
  698 %************************************************************************
  699 %*                                                                      *
  700             Building coercions
  701 %*                                                                      *
  702 %************************************************************************
  703 
  704 These "smart constructors" maintain the invariants listed in the definition
  705 of Coercion, and they perform very basic optimizations.
  706 
  707 Note [Role twiddling functions]
  708 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  709 
  710 There are a plethora of functions for twiddling roles:
  711 
  712 mkSubCo: Requires a nominal input coercion and always produces a
  713 representational output. This is used when you (the programmer) are sure you
  714 know exactly that role you have and what you want.
  715 
  716 downgradeRole_maybe: This function takes both the input role and the output role
  717 as parameters. (The *output* role comes first!) It can only *downgrade* a
  718 role -- that is, change it from N to R or P, or from R to P. This one-way
  719 behavior is why there is the "_maybe". If an upgrade is requested, this
  720 function produces Nothing. This is used when you need to change the role of a
  721 coercion, but you're not sure (as you're writing the code) of which roles are
  722 involved.
  723 
  724 This function could have been written using coercionRole to ascertain the role
  725 of the input. But, that function is recursive, and the caller of downgradeRole_maybe
  726 often knows the input role. So, this is more efficient.
  727 
  728 downgradeRole: This is just like downgradeRole_maybe, but it panics if the
  729 conversion isn't a downgrade.
  730 
  731 setNominalRole_maybe: This is the only function that can *upgrade* a coercion.
  732 The result (if it exists) is always Nominal. The input can be at any role. It
  733 works on a "best effort" basis, as it should never be strictly necessary to
  734 upgrade a coercion during compilation. It is currently only used within GHC in
  735 splitAppCo_maybe. In order to be a proper inverse of mkAppCo, the second
  736 coercion that splitAppCo_maybe returns must be nominal. But, it's conceivable
  737 that splitAppCo_maybe is operating over a TyConAppCo that uses a
  738 representational coercion. Hence the need for setNominalRole_maybe.
  739 splitAppCo_maybe, in turn, is used only within coercion optimization -- thus,
  740 it is not absolutely critical that setNominalRole_maybe be complete.
  741 
  742 Note that setNominalRole_maybe will never upgrade a phantom UnivCo. Phantom
  743 UnivCos are perfectly type-safe, whereas representational and nominal ones are
  744 not. (Nominal ones are no worse than representational ones, so this function *will*
  745 change a UnivCo Representational to a UnivCo Nominal.)
  746 
  747 Conal Elliott also came across a need for this function while working with the
  748 GHC API, as he was decomposing Core casts. The Core casts use representational
  749 coercions, as they must, but his use case required nominal coercions (he was
  750 building a GADT). So, that's why this function is exported from this module.
  751 
  752 One might ask: shouldn't downgradeRole_maybe just use setNominalRole_maybe as
  753 appropriate? I (Richard E.) have decided not to do this, because upgrading a
  754 role is bizarre and a caller should have to ask for this behavior explicitly.
  755 
  756 -}
  757 
  758 -- | Make a reflexive coercion
  759 mkReflCo :: Role -> Type -> Coercion
  760 mkReflCo Nominal ty = Refl ty
  761 mkReflCo r       ty = GRefl r ty MRefl
  762 
  763 -- | Make a representational reflexive coercion
  764 mkRepReflCo :: Type -> Coercion
  765 mkRepReflCo ty = GRefl Representational ty MRefl
  766 
  767 -- | Make a nominal reflexive coercion
  768 mkNomReflCo :: Type -> Coercion
  769 mkNomReflCo = Refl
  770 
  771 -- | Apply a type constructor to a list of coercions. It is the
  772 -- caller's responsibility to get the roles correct on argument coercions.
  773 mkTyConAppCo :: HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
  774 mkTyConAppCo r tc cos
  775   | [w, _rep1, _rep2, co1, co2] <- cos   -- See Note [Function coercions]
  776   , isFunTyCon tc
  777   = -- (a :: TYPE ra) -> (b :: TYPE rb)  ~  (c :: TYPE rc) -> (d :: TYPE rd)
  778     -- rep1 :: ra  ~  rc        rep2 :: rb  ~  rd
  779     -- co1  :: a   ~  c         co2  :: b   ~  d
  780     mkFunCo r w co1 co2
  781 
  782                -- Expand type synonyms
  783   | Just (tv_co_prs, rhs_ty, leftover_cos) <- expandSynTyCon_maybe tc cos
  784   = mkAppCos (liftCoSubst r (mkLiftingContext tv_co_prs) rhs_ty) leftover_cos
  785 
  786   | Just tys_roles <- traverse isReflCo_maybe cos
  787   = mkReflCo r (mkTyConApp tc (map fst tys_roles))
  788   -- See Note [Refl invariant]
  789 
  790   | otherwise = TyConAppCo r tc cos
  791 
  792 -- | Build a function 'Coercion' from two other 'Coercion's. That is,
  793 -- given @co1 :: a ~ b@ and @co2 :: x ~ y@ produce @co :: (a -> x) ~ (b -> y)@.
  794 mkFunCo :: Role -> CoercionN -> Coercion -> Coercion -> Coercion
  795 mkFunCo r w co1 co2
  796     -- See Note [Refl invariant]
  797   | Just (ty1, _) <- isReflCo_maybe co1
  798   , Just (ty2, _) <- isReflCo_maybe co2
  799   , Just (w, _) <- isReflCo_maybe w
  800   = mkReflCo r (mkVisFunTy w ty1 ty2)
  801   | otherwise = FunCo r w co1 co2
  802 
  803 -- | Apply a 'Coercion' to another 'Coercion'.
  804 -- The second coercion must be Nominal, unless the first is Phantom.
  805 -- If the first is Phantom, then the second can be either Phantom or Nominal.
  806 mkAppCo :: Coercion     -- ^ :: t1 ~r t2
  807         -> Coercion     -- ^ :: s1 ~N s2, where s1 :: k1, s2 :: k2
  808         -> Coercion     -- ^ :: t1 s1 ~r t2 s2
  809 mkAppCo co arg
  810   | Just (ty1, r) <- isReflCo_maybe co
  811   , Just (ty2, _) <- isReflCo_maybe arg
  812   = mkReflCo r (mkAppTy ty1 ty2)
  813 
  814   | Just (ty1, r) <- isReflCo_maybe co
  815   , Just (tc, tys) <- splitTyConApp_maybe ty1
  816     -- Expand type synonyms; a TyConAppCo can't have a type synonym (#9102)
  817   = mkTyConAppCo r tc (zip_roles (tyConRolesX r tc) tys)
  818   where
  819     zip_roles (r1:_)  []            = [downgradeRole r1 Nominal arg]
  820     zip_roles (r1:rs) (ty1:tys)     = mkReflCo r1 ty1 : zip_roles rs tys
  821     zip_roles _       _             = panic "zip_roles" -- but the roles are infinite...
  822 
  823 mkAppCo (TyConAppCo r tc args) arg
  824   = case r of
  825       Nominal          -> mkTyConAppCo Nominal tc (args ++ [arg])
  826       Representational -> mkTyConAppCo Representational tc (args ++ [arg'])
  827         where new_role = (tyConRolesRepresentational tc) !! (length args)
  828               arg'     = downgradeRole new_role Nominal arg
  829       Phantom          -> mkTyConAppCo Phantom tc (args ++ [toPhantomCo arg])
  830 mkAppCo co arg = AppCo co  arg
  831 -- Note, mkAppCo is careful to maintain invariants regarding
  832 -- where Refl constructors appear; see the comments in the definition
  833 -- of Coercion and the Note [Refl invariant] in GHC.Core.TyCo.Rep.
  834 
  835 -- | Applies multiple 'Coercion's to another 'Coercion', from left to right.
  836 -- See also 'mkAppCo'.
  837 mkAppCos :: Coercion
  838          -> [Coercion]
  839          -> Coercion
  840 mkAppCos co1 cos = foldl' mkAppCo co1 cos
  841 
  842 {- Note [Unused coercion variable in ForAllCo]
  843 
  844 See Note [Unused coercion variable in ForAllTy] in GHC.Core.TyCo.Rep for the
  845 motivation for checking coercion variable in types.
  846 To lift the design choice to (ForAllCo cv kind_co body_co), we have two options:
  847 
  848 (1) In mkForAllCo, we check whether cv is a coercion variable
  849     and whether it is not used in body_co. If so we construct a FunCo.
  850 (2) We don't do this check in mkForAllCo.
  851     In coercionKind, we use mkTyCoForAllTy to perform the check and construct
  852     a FunTy when necessary.
  853 
  854 We chose (2) for two reasons:
  855 
  856 * for a coercion, all that matters is its kind, So ForAllCo or FunCo does not
  857   make a difference.
  858 * even if cv occurs in body_co, it is possible that cv does not occur in the kind
  859   of body_co. Therefore the check in coercionKind is inevitable.
  860 
  861 The last wrinkle is that there are restrictions around the use of the cv in the
  862 coercion, as described in Section 5.8.5.2 of Richard's thesis. The idea is that
  863 we cannot prove that the type system is consistent with unrestricted use of this
  864 cv; the consistency proof uses an untyped rewrite relation that works over types
  865 with all coercions and casts removed. So, we can allow the cv to appear only in
  866 positions that are erased. As an approximation of this (and keeping close to the
  867 published theory), we currently allow the cv only within the type in a Refl node
  868 and under a GRefl node (including in the Coercion stored in a GRefl). It's
  869 possible other places are OK, too, but this is a safe approximation.
  870 
  871 Sadly, with heterogeneous equality, this restriction might be able to be violated;
  872 Richard's thesis is unable to prove that it isn't. Specifically, the liftCoSubst
  873 function might create an invalid coercion. Because a violation of the
  874 restriction might lead to a program that "goes wrong", it is checked all the time,
  875 even in a production compiler and without -dcore-list. We *have* proved that the
  876 problem does not occur with homogeneous equality, so this check can be dropped
  877 once ~# is made to be homogeneous.
  878 -}
  879 
  880 
  881 -- | Make a Coercion from a tycovar, a kind coercion, and a body coercion.
  882 -- The kind of the tycovar should be the left-hand kind of the kind coercion.
  883 -- See Note [Unused coercion variable in ForAllCo]
  884 mkForAllCo :: TyCoVar -> CoercionN -> Coercion -> Coercion
  885 mkForAllCo v kind_co co
  886   | assert (varType v `eqType` (pFst $ coercionKind kind_co)) True
  887   , assert (isTyVar v || almostDevoidCoVarOfCo v co) True
  888   , Just (ty, r) <- isReflCo_maybe co
  889   , isGReflCo kind_co
  890   = mkReflCo r (mkTyCoInvForAllTy v ty)
  891   | otherwise
  892   = ForAllCo v kind_co co
  893 
  894 -- | Like 'mkForAllCo', but the inner coercion shouldn't be an obvious
  895 -- reflexive coercion. For example, it is guaranteed in 'mkForAllCos'.
  896 -- The kind of the tycovar should be the left-hand kind of the kind coercion.
  897 mkForAllCo_NoRefl :: TyCoVar -> CoercionN -> Coercion -> Coercion
  898 mkForAllCo_NoRefl v kind_co co
  899   | assert (varType v `eqType` (pFst $ coercionKind kind_co)) True
  900   , assert (isTyVar v || almostDevoidCoVarOfCo v co) True
  901   , assert (not (isReflCo co)) True
  902   , isCoVar v
  903   , not (v `elemVarSet` tyCoVarsOfCo co)
  904   = FunCo (coercionRole co) (multToCo Many) kind_co co
  905       -- Functions from coercions are always unrestricted
  906   | otherwise
  907   = ForAllCo v kind_co co
  908 
  909 -- | Make nested ForAllCos
  910 mkForAllCos :: [(TyCoVar, CoercionN)] -> Coercion -> Coercion
  911 mkForAllCos bndrs co
  912   | Just (ty, r ) <- isReflCo_maybe co
  913   = let (refls_rev'd, non_refls_rev'd) = span (isReflCo . snd) (reverse bndrs) in
  914     foldl' (flip $ uncurry mkForAllCo_NoRefl)
  915            (mkReflCo r (mkTyCoInvForAllTys (reverse (map fst refls_rev'd)) ty))
  916            non_refls_rev'd
  917   | otherwise
  918   = foldr (uncurry mkForAllCo_NoRefl) co bndrs
  919 
  920 -- | Make a Coercion quantified over a type/coercion variable;
  921 -- the variable has the same type in both sides of the coercion
  922 mkHomoForAllCos :: [TyCoVar] -> Coercion -> Coercion
  923 mkHomoForAllCos vs co
  924   | Just (ty, r) <- isReflCo_maybe co
  925   = mkReflCo r (mkTyCoInvForAllTys vs ty)
  926   | otherwise
  927   = mkHomoForAllCos_NoRefl vs co
  928 
  929 -- | Like 'mkHomoForAllCos', but the inner coercion shouldn't be an obvious
  930 -- reflexive coercion. For example, it is guaranteed in 'mkHomoForAllCos'.
  931 mkHomoForAllCos_NoRefl :: [TyCoVar] -> Coercion -> Coercion
  932 mkHomoForAllCos_NoRefl vs orig_co
  933   = assert (not (isReflCo orig_co))
  934     foldr go orig_co vs
  935   where
  936     go v co = mkForAllCo_NoRefl v (mkNomReflCo (varType v)) co
  937 
  938 mkCoVarCo :: CoVar -> Coercion
  939 -- cv :: s ~# t
  940 -- See Note [mkCoVarCo]
  941 mkCoVarCo cv = CoVarCo cv
  942 
  943 mkCoVarCos :: [CoVar] -> [Coercion]
  944 mkCoVarCos = map mkCoVarCo
  945 
  946 {- Note [mkCoVarCo]
  947 ~~~~~~~~~~~~~~~~~~~
  948 In the past, mkCoVarCo optimised (c :: t~t) to (Refl t).  That is
  949 valid (although see Note [Unbound RULE binders] in GHC.Core.Rules), but
  950 it's a relatively expensive test and perhaps better done in
  951 optCoercion.  Not a big deal either way.
  952 -}
  953 
  954 -- | Extract a covar, if possible. This check is dirty. Be ashamed
  955 -- of yourself. (It's dirty because it cares about the structure of
  956 -- a coercion, which is morally reprehensible.)
  957 isCoVar_maybe :: Coercion -> Maybe CoVar
  958 isCoVar_maybe (CoVarCo cv) = Just cv
  959 isCoVar_maybe _            = Nothing
  960 
  961 mkAxInstCo :: Role -> CoAxiom br -> BranchIndex -> [Type] -> [Coercion]
  962            -> Coercion
  963 -- mkAxInstCo can legitimately be called over-staturated;
  964 -- i.e. with more type arguments than the coercion requires
  965 mkAxInstCo role ax index tys cos
  966   | arity == n_tys = downgradeRole role ax_role $
  967                      mkAxiomInstCo ax_br index (rtys `chkAppend` cos)
  968   | otherwise      = assert (arity < n_tys) $
  969                      downgradeRole role ax_role $
  970                      mkAppCos (mkAxiomInstCo ax_br index
  971                                              (ax_args `chkAppend` cos))
  972                               leftover_args
  973   where
  974     n_tys         = length tys
  975     ax_br         = toBranchedAxiom ax
  976     branch        = coAxiomNthBranch ax_br index
  977     tvs           = coAxBranchTyVars branch
  978     arity         = length tvs
  979     arg_roles     = coAxBranchRoles branch
  980     rtys          = zipWith mkReflCo (arg_roles ++ repeat Nominal) tys
  981     (ax_args, leftover_args)
  982                   = splitAt arity rtys
  983     ax_role       = coAxiomRole ax
  984 
  985 -- worker function
  986 mkAxiomInstCo :: CoAxiom Branched -> BranchIndex -> [Coercion] -> Coercion
  987 mkAxiomInstCo ax index args
  988   = assert (args `lengthIs` coAxiomArity ax index) $
  989     AxiomInstCo ax index args
  990 
  991 -- to be used only with unbranched axioms
  992 mkUnbranchedAxInstCo :: Role -> CoAxiom Unbranched
  993                      -> [Type] -> [Coercion] -> Coercion
  994 mkUnbranchedAxInstCo role ax tys cos
  995   = mkAxInstCo role ax 0 tys cos
  996 
  997 mkAxInstRHS :: CoAxiom br -> BranchIndex -> [Type] -> [Coercion] -> Type
  998 -- Instantiate the axiom with specified types,
  999 -- returning the instantiated RHS
 1000 -- A companion to mkAxInstCo:
 1001 --    mkAxInstRhs ax index tys = snd (coercionKind (mkAxInstCo ax index tys))
 1002 mkAxInstRHS ax index tys cos
 1003   = assert (tvs `equalLength` tys1) $
 1004     mkAppTys rhs' tys2
 1005   where
 1006     branch       = coAxiomNthBranch ax index
 1007     tvs          = coAxBranchTyVars branch
 1008     cvs          = coAxBranchCoVars branch
 1009     (tys1, tys2) = splitAtList tvs tys
 1010     rhs'         = substTyWith tvs tys1 $
 1011                    substTyWithCoVars cvs cos $
 1012                    coAxBranchRHS branch
 1013 
 1014 mkUnbranchedAxInstRHS :: CoAxiom Unbranched -> [Type] -> [Coercion] -> Type
 1015 mkUnbranchedAxInstRHS ax = mkAxInstRHS ax 0
 1016 
 1017 -- | Return the left-hand type of the axiom, when the axiom is instantiated
 1018 -- at the types given.
 1019 mkAxInstLHS :: CoAxiom br -> BranchIndex -> [Type] -> [Coercion] -> Type
 1020 mkAxInstLHS ax index tys cos
 1021   = assert (tvs `equalLength` tys1) $
 1022     mkTyConApp fam_tc (lhs_tys `chkAppend` tys2)
 1023   where
 1024     branch       = coAxiomNthBranch ax index
 1025     tvs          = coAxBranchTyVars branch
 1026     cvs          = coAxBranchCoVars branch
 1027     (tys1, tys2) = splitAtList tvs tys
 1028     lhs_tys      = substTysWith tvs tys1 $
 1029                    substTysWithCoVars cvs cos $
 1030                    coAxBranchLHS branch
 1031     fam_tc       = coAxiomTyCon ax
 1032 
 1033 -- | Instantiate the left-hand side of an unbranched axiom
 1034 mkUnbranchedAxInstLHS :: CoAxiom Unbranched -> [Type] -> [Coercion] -> Type
 1035 mkUnbranchedAxInstLHS ax = mkAxInstLHS ax 0
 1036 
 1037 -- | Make a coercion from a coercion hole
 1038 mkHoleCo :: CoercionHole -> Coercion
 1039 mkHoleCo h = HoleCo h
 1040 
 1041 -- | Make a universal coercion between two arbitrary types.
 1042 mkUnivCo :: UnivCoProvenance
 1043          -> Role       -- ^ role of the built coercion, "r"
 1044          -> Type       -- ^ t1 :: k1
 1045          -> Type       -- ^ t2 :: k2
 1046          -> Coercion   -- ^ :: t1 ~r t2
 1047 mkUnivCo prov role ty1 ty2
 1048   | ty1 `eqType` ty2 = mkReflCo role ty1
 1049   | otherwise        = UnivCo prov role ty1 ty2
 1050 
 1051 -- | Create a symmetric version of the given 'Coercion' that asserts
 1052 --   equality between the same types but in the other "direction", so
 1053 --   a kind of @t1 ~ t2@ becomes the kind @t2 ~ t1@.
 1054 mkSymCo :: Coercion -> Coercion
 1055 
 1056 -- Do a few simple optimizations, but don't bother pushing occurrences
 1057 -- of symmetry to the leaves; the optimizer will take care of that.
 1058 mkSymCo co | isReflCo co          = co
 1059 mkSymCo    (SymCo co)             = co
 1060 mkSymCo    (SubCo (SymCo co))     = SubCo co
 1061 mkSymCo co                        = SymCo co
 1062 
 1063 -- | Create a new 'Coercion' by composing the two given 'Coercion's transitively.
 1064 --   (co1 ; co2)
 1065 mkTransCo :: Coercion -> Coercion -> Coercion
 1066 mkTransCo co1 co2 | isReflCo co1 = co2
 1067                   | isReflCo co2 = co1
 1068 mkTransCo (GRefl r t1 (MCo co1)) (GRefl _ _ (MCo co2))
 1069   = GRefl r t1 (MCo $ mkTransCo co1 co2)
 1070 mkTransCo co1 co2                = TransCo co1 co2
 1071 
 1072 mkNthCo :: HasDebugCallStack
 1073         => Role  -- The role of the coercion you're creating
 1074         -> Int   -- Zero-indexed
 1075         -> Coercion
 1076         -> Coercion
 1077 mkNthCo r n co
 1078   = assertPpr good_call bad_call_msg $
 1079     go n co
 1080   where
 1081     Pair ty1 ty2 = coercionKind co
 1082 
 1083     go 0 co
 1084       | Just (ty, _) <- isReflCo_maybe co
 1085       , Just (tv, _) <- splitForAllTyCoVar_maybe ty
 1086       = -- works for both tyvar and covar
 1087         assert (r == Nominal) $
 1088         mkNomReflCo (varType tv)
 1089 
 1090     go n co
 1091       | Just (ty, r0) <- isReflCo_maybe co
 1092       , let tc = tyConAppTyCon ty
 1093       = assertPpr (ok_tc_app ty n) (ppr n $$ ppr ty) $
 1094         assert (nthRole r0 tc n == r) $
 1095         mkReflCo r (tyConAppArgN n ty)
 1096       where ok_tc_app :: Type -> Int -> Bool
 1097             ok_tc_app ty n
 1098               | Just (_, tys) <- splitTyConApp_maybe ty
 1099               = tys `lengthExceeds` n
 1100               | isForAllTy ty  -- nth:0 pulls out a kind coercion from a hetero forall
 1101               = n == 0
 1102               | otherwise
 1103               = False
 1104 
 1105     go 0 (ForAllCo _ kind_co _)
 1106       = assert (r == Nominal)
 1107         kind_co
 1108       -- If co :: (forall a1:k1. t1) ~ (forall a2:k2. t2)
 1109       -- then (nth 0 co :: k1 ~N k2)
 1110       -- If co :: (forall a1:t1 ~ t2. t1) ~ (forall a2:t3 ~ t4. t2)
 1111       -- then (nth 0 co :: (t1 ~ t2) ~N (t3 ~ t4))
 1112 
 1113     go n (FunCo _ w arg res)
 1114       = mkNthCoFunCo n w arg res
 1115 
 1116     go n (TyConAppCo r0 tc arg_cos) = assertPpr (r == nthRole r0 tc n)
 1117                                                   (vcat [ ppr tc
 1118                                                         , ppr arg_cos
 1119                                                         , ppr r0
 1120                                                         , ppr n
 1121                                                         , ppr r ]) $
 1122                                              arg_cos `getNth` n
 1123 
 1124     go n (SymCo co)  -- Recurse, hoping to get to a TyConAppCo or FunCo
 1125       = mkSymCo (go n co)
 1126 
 1127     go n co
 1128       = NthCo r n co
 1129 
 1130     -- Assertion checking
 1131     bad_call_msg = vcat [ text "Coercion =" <+> ppr co
 1132                         , text "LHS ty =" <+> ppr ty1
 1133                         , text "RHS ty =" <+> ppr ty2
 1134                         , text "n =" <+> ppr n, text "r =" <+> ppr r
 1135                         , text "coercion role =" <+> ppr (coercionRole co) ]
 1136     good_call
 1137       -- If the Coercion passed in is between forall-types, then the Int must
 1138       -- be 0 and the role must be Nominal.
 1139       | Just (_tv1, _) <- splitForAllTyCoVar_maybe ty1
 1140       , Just (_tv2, _) <- splitForAllTyCoVar_maybe ty2
 1141       = n == 0 && r == Nominal
 1142 
 1143       -- If the Coercion passed in is between T tys and T tys', then the Int
 1144       -- must be less than the length of tys/tys' (which must be the same
 1145       -- lengths).
 1146       --
 1147       -- If the role of the Coercion is nominal, then the role passed in must
 1148       -- be nominal. If the role of the Coercion is representational, then the
 1149       -- role passed in must be tyConRolesRepresentational T !! n. If the role
 1150       -- of the Coercion is Phantom, then the role passed in must be Phantom.
 1151       --
 1152       -- See also Note [NthCo Cached Roles] if you're wondering why it's
 1153       -- blaringly obvious that we should be *computing* this role instead of
 1154       -- passing it in.
 1155       | Just (tc1, tys1) <- splitTyConApp_maybe ty1
 1156       , Just (tc2, tys2) <- splitTyConApp_maybe ty2
 1157       , tc1 == tc2
 1158       = let len1 = length tys1
 1159             len2 = length tys2
 1160             good_role = case coercionRole co of
 1161                           Nominal -> r == Nominal
 1162                           Representational -> r == (tyConRolesRepresentational tc1 !! n)
 1163                           Phantom -> r == Phantom
 1164         in len1 == len2 && n < len1 && good_role
 1165 
 1166       | otherwise
 1167       = True
 1168 
 1169 -- | Extract the nth field of a FunCo
 1170 mkNthCoFunCo :: Int         -- ^ "n"
 1171              -> CoercionN   -- ^ multiplicity coercion
 1172              -> Coercion    -- ^ argument coercion
 1173              -> Coercion    -- ^ result coercion
 1174              -> Coercion    -- ^ nth coercion from a FunCo
 1175 -- See Note [Function coercions]
 1176 -- If FunCo _ mult arg_co res_co ::   (s1:TYPE sk1 :mult-> s2:TYPE sk2)
 1177 --                                  ~ (t1:TYPE tk1 :mult-> t2:TYPE tk2)
 1178 -- Then we want to behave as if co was
 1179 --    TyConAppCo mult argk_co resk_co arg_co res_co
 1180 -- where
 1181 --    argk_co :: sk1 ~ tk1  =  mkNthCo 0 (mkKindCo arg_co)
 1182 --    resk_co :: sk2 ~ tk2  =  mkNthCo 0 (mkKindCo res_co)
 1183 --                             i.e. mkRuntimeRepCo
 1184 mkNthCoFunCo n w co1 co2 = case n of
 1185   0 -> w
 1186   1 -> mkRuntimeRepCo co1
 1187   2 -> mkRuntimeRepCo co2
 1188   3 -> co1
 1189   4 -> co2
 1190   _ -> pprPanic "mkNthCo(FunCo)" (ppr n $$ ppr w $$ ppr co1 $$ ppr co2)
 1191 
 1192 -- | If you're about to call @mkNthCo r n co@, then @r@ should be
 1193 -- whatever @nthCoRole n co@ returns.
 1194 nthCoRole :: Int -> Coercion -> Role
 1195 nthCoRole n co
 1196   | Just (tc, _) <- splitTyConApp_maybe lty
 1197   = nthRole r tc n
 1198 
 1199   | Just _ <- splitForAllTyCoVar_maybe lty
 1200   = Nominal
 1201 
 1202   | otherwise
 1203   = pprPanic "nthCoRole" (ppr co)
 1204 
 1205   where
 1206     lty = coercionLKind co
 1207     r   = coercionRole co
 1208 
 1209 mkLRCo :: LeftOrRight -> Coercion -> Coercion
 1210 mkLRCo lr co
 1211   | Just (ty, eq) <- isReflCo_maybe co
 1212   = mkReflCo eq (pickLR lr (splitAppTy ty))
 1213   | otherwise
 1214   = LRCo lr co
 1215 
 1216 -- | Instantiates a 'Coercion'.
 1217 mkInstCo :: Coercion -> Coercion -> Coercion
 1218 mkInstCo (ForAllCo tcv _kind_co body_co) co
 1219   | Just (arg, _) <- isReflCo_maybe co
 1220       -- works for both tyvar and covar
 1221   = substCoUnchecked (zipTCvSubst [tcv] [arg]) body_co
 1222 mkInstCo co arg = InstCo co arg
 1223 
 1224 -- | Given @ty :: k1@, @co :: k1 ~ k2@,
 1225 -- produces @co' :: ty ~r (ty |> co)@
 1226 mkGReflRightCo :: Role -> Type -> CoercionN -> Coercion
 1227 mkGReflRightCo r ty co
 1228   | isGReflCo co = mkReflCo r ty
 1229     -- the kinds of @k1@ and @k2@ are the same, thus @isGReflCo@
 1230     -- instead of @isReflCo@
 1231   | otherwise = GRefl r ty (MCo co)
 1232 
 1233 -- | Given @ty :: k1@, @co :: k1 ~ k2@,
 1234 -- produces @co' :: (ty |> co) ~r ty@
 1235 mkGReflLeftCo :: Role -> Type -> CoercionN -> Coercion
 1236 mkGReflLeftCo r ty co
 1237   | isGReflCo co = mkReflCo r ty
 1238     -- the kinds of @k1@ and @k2@ are the same, thus @isGReflCo@
 1239     -- instead of @isReflCo@
 1240   | otherwise    = mkSymCo $ GRefl r ty (MCo co)
 1241 
 1242 -- | Given @ty :: k1@, @co :: k1 ~ k2@, @co2:: ty ~r ty'@,
 1243 -- produces @co' :: (ty |> co) ~r ty'
 1244 -- It is not only a utility function, but it saves allocation when co
 1245 -- is a GRefl coercion.
 1246 mkCoherenceLeftCo :: Role -> Type -> CoercionN -> Coercion -> Coercion
 1247 mkCoherenceLeftCo r ty co co2
 1248   | isGReflCo co = co2
 1249   | otherwise    = (mkSymCo $ GRefl r ty (MCo co)) `mkTransCo` co2
 1250 
 1251 -- | Given @ty :: k1@, @co :: k1 ~ k2@, @co2:: ty' ~r ty@,
 1252 -- produces @co' :: ty' ~r (ty |> co)
 1253 -- It is not only a utility function, but it saves allocation when co
 1254 -- is a GRefl coercion.
 1255 mkCoherenceRightCo :: Role -> Type -> CoercionN -> Coercion -> Coercion
 1256 mkCoherenceRightCo r ty co co2
 1257   | isGReflCo co = co2
 1258   | otherwise    = co2 `mkTransCo` GRefl r ty (MCo co)
 1259 
 1260 -- | Given @co :: (a :: k) ~ (b :: k')@ produce @co' :: k ~ k'@.
 1261 mkKindCo :: Coercion -> Coercion
 1262 mkKindCo co | Just (ty, _) <- isReflCo_maybe co = Refl (typeKind ty)
 1263 mkKindCo (GRefl _ _ (MCo co)) = co
 1264 mkKindCo (UnivCo (PhantomProv h) _ _ _)    = h
 1265 mkKindCo (UnivCo (ProofIrrelProv h) _ _ _) = h
 1266 mkKindCo co
 1267   | Pair ty1 ty2 <- coercionKind co
 1268        -- generally, calling coercionKind during coercion creation is a bad idea,
 1269        -- as it can lead to exponential behavior. But, we don't have nested mkKindCos,
 1270        -- so it's OK here.
 1271   , let tk1 = typeKind ty1
 1272         tk2 = typeKind ty2
 1273   , tk1 `eqType` tk2
 1274   = Refl tk1
 1275   | otherwise
 1276   = KindCo co
 1277 
 1278 mkSubCo :: HasDebugCallStack => Coercion -> Coercion
 1279 -- Input coercion is Nominal, result is Representational
 1280 -- see also Note [Role twiddling functions]
 1281 mkSubCo (Refl ty) = GRefl Representational ty MRefl
 1282 mkSubCo (GRefl Nominal ty co) = GRefl Representational ty co
 1283 mkSubCo (TyConAppCo Nominal tc cos)
 1284   = TyConAppCo Representational tc (applyRoles tc cos)
 1285 mkSubCo (FunCo Nominal w arg res)
 1286   = FunCo Representational w
 1287           (downgradeRole Representational Nominal arg)
 1288           (downgradeRole Representational Nominal res)
 1289 mkSubCo co = assertPpr (coercionRole co == Nominal) (ppr co <+> ppr (coercionRole co)) $
 1290              SubCo co
 1291 
 1292 -- | Changes a role, but only a downgrade. See Note [Role twiddling functions]
 1293 downgradeRole_maybe :: Role   -- ^ desired role
 1294                     -> Role   -- ^ current role
 1295                     -> Coercion -> Maybe Coercion
 1296 -- In (downgradeRole_maybe dr cr co) it's a precondition that
 1297 --                                   cr = coercionRole co
 1298 
 1299 downgradeRole_maybe Nominal          Nominal          co = Just co
 1300 downgradeRole_maybe Nominal          _                _  = Nothing
 1301 
 1302 downgradeRole_maybe Representational Nominal          co = Just (mkSubCo co)
 1303 downgradeRole_maybe Representational Representational co = Just co
 1304 downgradeRole_maybe Representational Phantom          _  = Nothing
 1305 
 1306 downgradeRole_maybe Phantom          Phantom          co = Just co
 1307 downgradeRole_maybe Phantom          _                co = Just (toPhantomCo co)
 1308 
 1309 -- | Like 'downgradeRole_maybe', but panics if the change isn't a downgrade.
 1310 -- See Note [Role twiddling functions]
 1311 downgradeRole :: Role  -- desired role
 1312               -> Role  -- current role
 1313               -> Coercion -> Coercion
 1314 downgradeRole r1 r2 co
 1315   = case downgradeRole_maybe r1 r2 co of
 1316       Just co' -> co'
 1317       Nothing  -> pprPanic "downgradeRole" (ppr co)
 1318 
 1319 mkAxiomRuleCo :: CoAxiomRule -> [Coercion] -> Coercion
 1320 mkAxiomRuleCo = AxiomRuleCo
 1321 
 1322 -- | Make a "coercion between coercions".
 1323 mkProofIrrelCo :: Role       -- ^ role of the created coercion, "r"
 1324                -> CoercionN  -- ^ :: phi1 ~N phi2
 1325                -> Coercion   -- ^ g1 :: phi1
 1326                -> Coercion   -- ^ g2 :: phi2
 1327                -> Coercion   -- ^ :: g1 ~r g2
 1328 
 1329 -- if the two coercion prove the same fact, I just don't care what
 1330 -- the individual coercions are.
 1331 mkProofIrrelCo r co g  _ | isGReflCo co  = mkReflCo r (mkCoercionTy g)
 1332   -- kco is a kind coercion, thus @isGReflCo@ rather than @isReflCo@
 1333 mkProofIrrelCo r kco        g1 g2 = mkUnivCo (ProofIrrelProv kco) r
 1334                                              (mkCoercionTy g1) (mkCoercionTy g2)
 1335 
 1336 {-
 1337 %************************************************************************
 1338 %*                                                                      *
 1339    Roles
 1340 %*                                                                      *
 1341 %************************************************************************
 1342 -}
 1343 
 1344 -- | Converts a coercion to be nominal, if possible.
 1345 -- See Note [Role twiddling functions]
 1346 setNominalRole_maybe :: Role -- of input coercion
 1347                      -> Coercion -> Maybe Coercion
 1348 setNominalRole_maybe r co
 1349   | r == Nominal = Just co
 1350   | otherwise = setNominalRole_maybe_helper co
 1351   where
 1352     setNominalRole_maybe_helper (SubCo co)  = Just co
 1353     setNominalRole_maybe_helper co@(Refl _) = Just co
 1354     setNominalRole_maybe_helper (GRefl _ ty co) = Just $ GRefl Nominal ty co
 1355     setNominalRole_maybe_helper (TyConAppCo Representational tc cos)
 1356       = do { cos' <- zipWithM setNominalRole_maybe (tyConRolesX Representational tc) cos
 1357            ; return $ TyConAppCo Nominal tc cos' }
 1358     setNominalRole_maybe_helper (FunCo Representational w co1 co2)
 1359       = do { co1' <- setNominalRole_maybe Representational co1
 1360            ; co2' <- setNominalRole_maybe Representational co2
 1361            ; return $ FunCo Nominal w co1' co2'
 1362            }
 1363     setNominalRole_maybe_helper (SymCo co)
 1364       = SymCo <$> setNominalRole_maybe_helper co
 1365     setNominalRole_maybe_helper (TransCo co1 co2)
 1366       = TransCo <$> setNominalRole_maybe_helper co1 <*> setNominalRole_maybe_helper co2
 1367     setNominalRole_maybe_helper (AppCo co1 co2)
 1368       = AppCo <$> setNominalRole_maybe_helper co1 <*> pure co2
 1369     setNominalRole_maybe_helper (ForAllCo tv kind_co co)
 1370       = ForAllCo tv kind_co <$> setNominalRole_maybe_helper co
 1371     setNominalRole_maybe_helper (NthCo _r n co)
 1372       -- NB, this case recurses via setNominalRole_maybe, not
 1373       -- setNominalRole_maybe_helper!
 1374       = NthCo Nominal n <$> setNominalRole_maybe (coercionRole co) co
 1375     setNominalRole_maybe_helper (InstCo co arg)
 1376       = InstCo <$> setNominalRole_maybe_helper co <*> pure arg
 1377     setNominalRole_maybe_helper (UnivCo prov _ co1 co2)
 1378       | case prov of PhantomProv _    -> False  -- should always be phantom
 1379                      ProofIrrelProv _ -> True   -- it's always safe
 1380                      PluginProv _     -> False  -- who knows? This choice is conservative.
 1381                      CorePrepProv _   -> True
 1382       = Just $ UnivCo prov Nominal co1 co2
 1383     setNominalRole_maybe_helper _ = Nothing
 1384 
 1385 -- | Make a phantom coercion between two types. The coercion passed
 1386 -- in must be a nominal coercion between the kinds of the
 1387 -- types.
 1388 mkPhantomCo :: Coercion -> Type -> Type -> Coercion
 1389 mkPhantomCo h t1 t2
 1390   = mkUnivCo (PhantomProv h) Phantom t1 t2
 1391 
 1392 -- takes any coercion and turns it into a Phantom coercion
 1393 toPhantomCo :: Coercion -> Coercion
 1394 toPhantomCo co
 1395   = mkPhantomCo (mkKindCo co) ty1 ty2
 1396   where Pair ty1 ty2 = coercionKind co
 1397 
 1398 -- Convert args to a TyConAppCo Nominal to the same TyConAppCo Representational
 1399 applyRoles :: TyCon -> [Coercion] -> [Coercion]
 1400 applyRoles tc cos
 1401   = zipWith (\r -> downgradeRole r Nominal) (tyConRolesRepresentational tc) cos
 1402 
 1403 -- the Role parameter is the Role of the TyConAppCo
 1404 -- defined here because this is intimately concerned with the implementation
 1405 -- of TyConAppCo
 1406 -- Always returns an infinite list (with a infinite tail of Nominal)
 1407 tyConRolesX :: Role -> TyCon -> [Role]
 1408 tyConRolesX Representational tc = tyConRolesRepresentational tc
 1409 tyConRolesX role             _  = repeat role
 1410 
 1411 -- Returns the roles of the parameters of a tycon, with an infinite tail
 1412 -- of Nominal
 1413 tyConRolesRepresentational :: TyCon -> [Role]
 1414 tyConRolesRepresentational tc = tyConRoles tc ++ repeat Nominal
 1415 
 1416 nthRole :: Role -> TyCon -> Int -> Role
 1417 nthRole Nominal _ _ = Nominal
 1418 nthRole Phantom _ _ = Phantom
 1419 nthRole Representational tc n
 1420   = (tyConRolesRepresentational tc) `getNth` n
 1421 
 1422 ltRole :: Role -> Role -> Bool
 1423 -- Is one role "less" than another?
 1424 --     Nominal < Representational < Phantom
 1425 ltRole Phantom          _       = False
 1426 ltRole Representational Phantom = True
 1427 ltRole Representational _       = False
 1428 ltRole Nominal          Nominal = False
 1429 ltRole Nominal          _       = True
 1430 
 1431 -------------------------------
 1432 
 1433 -- | like mkKindCo, but aggressively & recursively optimizes to avoid using
 1434 -- a KindCo constructor. The output role is nominal.
 1435 promoteCoercion :: Coercion -> CoercionN
 1436 
 1437 -- First cases handles anything that should yield refl.
 1438 promoteCoercion co = case co of
 1439 
 1440     _ | ki1 `eqType` ki2
 1441       -> mkNomReflCo (typeKind ty1)
 1442      -- no later branch should return refl
 1443      --    The assert (False )s throughout
 1444      -- are these cases explicitly, but they should never fire.
 1445 
 1446     Refl _ -> assert False $
 1447               mkNomReflCo ki1
 1448 
 1449     GRefl _ _ MRefl -> assert False $
 1450                        mkNomReflCo ki1
 1451 
 1452     GRefl _ _ (MCo co) -> co
 1453 
 1454     TyConAppCo _ tc args
 1455       | Just co' <- instCoercions (mkNomReflCo (tyConKind tc)) args
 1456       -> co'
 1457       | otherwise
 1458       -> mkKindCo co
 1459 
 1460     AppCo co1 arg
 1461       | Just co' <- instCoercion (coercionKind (mkKindCo co1))
 1462                                  (promoteCoercion co1) arg
 1463       -> co'
 1464       | otherwise
 1465       -> mkKindCo co
 1466 
 1467     ForAllCo tv _ g
 1468       | isTyVar tv
 1469       -> promoteCoercion g
 1470 
 1471     ForAllCo _ _ _
 1472       -> assert False $
 1473          mkNomReflCo liftedTypeKind
 1474       -- See Note [Weird typing rule for ForAllTy] in GHC.Core.TyCo.Rep
 1475 
 1476     FunCo _ _ _ _
 1477       -> assert False $
 1478          mkNomReflCo liftedTypeKind
 1479 
 1480     CoVarCo {}     -> mkKindCo co
 1481     HoleCo {}      -> mkKindCo co
 1482     AxiomInstCo {} -> mkKindCo co
 1483     AxiomRuleCo {} -> mkKindCo co
 1484 
 1485     UnivCo (PhantomProv kco)    _ _ _ -> kco
 1486     UnivCo (ProofIrrelProv kco) _ _ _ -> kco
 1487     UnivCo (PluginProv _)       _ _ _ -> mkKindCo co
 1488     UnivCo (CorePrepProv _)     _ _ _ -> mkKindCo co
 1489 
 1490     SymCo g
 1491       -> mkSymCo (promoteCoercion g)
 1492 
 1493     TransCo co1 co2
 1494       -> mkTransCo (promoteCoercion co1) (promoteCoercion co2)
 1495 
 1496     NthCo _ n co1
 1497       | Just (_, args) <- splitTyConAppCo_maybe co1
 1498       , args `lengthExceeds` n
 1499       -> promoteCoercion (args !! n)
 1500 
 1501       | Just _ <- splitForAllCo_maybe co
 1502       , n == 0
 1503       -> assert False $ mkNomReflCo liftedTypeKind
 1504 
 1505       | otherwise
 1506       -> mkKindCo co
 1507 
 1508     LRCo lr co1
 1509       | Just (lco, rco) <- splitAppCo_maybe co1
 1510       -> case lr of
 1511            CLeft  -> promoteCoercion lco
 1512            CRight -> promoteCoercion rco
 1513 
 1514       | otherwise
 1515       -> mkKindCo co
 1516 
 1517     InstCo g _
 1518       | isForAllTy_ty ty1
 1519       -> assert (isForAllTy_ty ty2) $
 1520          promoteCoercion g
 1521       | otherwise
 1522       -> assert False $
 1523          mkNomReflCo liftedTypeKind
 1524            -- See Note [Weird typing rule for ForAllTy] in GHC.Core.TyCo.Rep
 1525 
 1526     KindCo _
 1527       -> assert False $
 1528          mkNomReflCo liftedTypeKind
 1529 
 1530     SubCo g
 1531       -> promoteCoercion g
 1532 
 1533   where
 1534     Pair ty1 ty2 = coercionKind co
 1535     ki1 = typeKind ty1
 1536     ki2 = typeKind ty2
 1537 
 1538 -- | say @g = promoteCoercion h@. Then, @instCoercion g w@ yields @Just g'@,
 1539 -- where @g' = promoteCoercion (h w)@.
 1540 -- fails if this is not possible, if @g@ coerces between a forall and an ->
 1541 -- or if second parameter has a representational role and can't be used
 1542 -- with an InstCo.
 1543 instCoercion :: Pair Type -- g :: lty ~ rty
 1544              -> CoercionN  -- ^  must be nominal
 1545              -> Coercion
 1546              -> Maybe CoercionN
 1547 instCoercion (Pair lty rty) g w
 1548   | (isForAllTy_ty lty && isForAllTy_ty rty)
 1549   || (isForAllTy_co lty && isForAllTy_co rty)
 1550   , Just w' <- setNominalRole_maybe (coercionRole w) w
 1551     -- g :: (forall t1. t2) ~ (forall t1. t3)
 1552     -- w :: s1 ~ s2
 1553     -- returns mkInstCo g w' :: t2 [t1 |-> s1 ] ~ t3 [t1 |-> s2]
 1554   = Just $ mkInstCo g w'
 1555   | isFunTy lty && isFunTy rty
 1556     -- g :: (t1 -> t2) ~ (t3 -> t4)
 1557     -- returns t2 ~ t4
 1558   = Just $ mkNthCo Nominal 4 g -- extract result type, which is the 5th argument to (->)
 1559   | otherwise -- one forall, one funty...
 1560   = Nothing
 1561 
 1562 -- | Repeated use of 'instCoercion'
 1563 instCoercions :: CoercionN -> [Coercion] -> Maybe CoercionN
 1564 instCoercions g ws
 1565   = let arg_ty_pairs = map coercionKind ws in
 1566     snd <$> foldM go (coercionKind g, g) (zip arg_ty_pairs ws)
 1567   where
 1568     go :: (Pair Type, Coercion) -> (Pair Type, Coercion)
 1569        -> Maybe (Pair Type, Coercion)
 1570     go (g_tys, g) (w_tys, w)
 1571       = do { g' <- instCoercion g_tys g w
 1572            ; return (piResultTy <$> g_tys <*> w_tys, g') }
 1573 
 1574 -- | Creates a new coercion with both of its types casted by different casts
 1575 -- @castCoercionKind2 g r t1 t2 h1 h2@, where @g :: t1 ~r t2@,
 1576 -- has type @(t1 |> h1) ~r (t2 |> h2)@.
 1577 -- @h1@ and @h2@ must be nominal.
 1578 castCoercionKind2 :: Coercion -> Role -> Type -> Type
 1579                  -> CoercionN -> CoercionN -> Coercion
 1580 castCoercionKind2 g r t1 t2 h1 h2
 1581   = mkCoherenceRightCo r t2 h2 (mkCoherenceLeftCo r t1 h1 g)
 1582 
 1583 -- | @castCoercionKind1 g r t1 t2 h@ = @coercionKind g r t1 t2 h h@
 1584 -- That is, it's a specialised form of castCoercionKind, where the two
 1585 --          kind coercions are identical
 1586 -- @castCoercionKind1 g r t1 t2 h@, where @g :: t1 ~r t2@,
 1587 -- has type @(t1 |> h) ~r (t2 |> h)@.
 1588 -- @h@ must be nominal.
 1589 -- See Note [castCoercionKind1]
 1590 castCoercionKind1 :: Coercion -> Role -> Type -> Type
 1591                   -> CoercionN -> Coercion
 1592 castCoercionKind1 g r t1 t2 h
 1593   = case g of
 1594       Refl {} -> assert (r == Nominal) $ -- Refl is always Nominal
 1595                  mkNomReflCo (mkCastTy t2 h)
 1596       GRefl _ _ mco -> case mco of
 1597            MRefl       -> mkReflCo r (mkCastTy t2 h)
 1598            MCo kind_co -> GRefl r (mkCastTy t1 h) $
 1599                           MCo (mkSymCo h `mkTransCo` kind_co `mkTransCo` h)
 1600       _ -> castCoercionKind2 g r t1 t2 h h
 1601 
 1602 -- | Creates a new coercion with both of its types casted by different casts
 1603 -- @castCoercionKind g h1 h2@, where @g :: t1 ~r t2@,
 1604 -- has type @(t1 |> h1) ~r (t2 |> h2)@.
 1605 -- @h1@ and @h2@ must be nominal.
 1606 -- It calls @coercionKindRole@, so it's quite inefficient (which 'I' stands for)
 1607 -- Use @castCoercionKind2@ instead if @t1@, @t2@, and @r@ are known beforehand.
 1608 castCoercionKind :: Coercion -> CoercionN -> CoercionN -> Coercion
 1609 castCoercionKind g h1 h2
 1610   = castCoercionKind2 g r t1 t2 h1 h2
 1611   where
 1612     (Pair t1 t2, r) = coercionKindRole g
 1613 
 1614 mkFamilyTyConAppCo :: TyCon -> [CoercionN] -> CoercionN
 1615 -- ^ Given a family instance 'TyCon' and its arg 'Coercion's, return the
 1616 -- corresponding family 'Coercion'.  E.g:
 1617 --
 1618 -- > data family T a
 1619 -- > data instance T (Maybe b) = MkT b
 1620 --
 1621 -- Where the instance 'TyCon' is :RTL, so:
 1622 --
 1623 -- > mkFamilyTyConAppCo :RTL (co :: a ~# Int) = T (Maybe a) ~# T (Maybe Int)
 1624 --
 1625 -- cf. 'mkFamilyTyConApp'
 1626 mkFamilyTyConAppCo tc cos
 1627   | Just (fam_tc, fam_tys) <- tyConFamInst_maybe tc
 1628   , let tvs = tyConTyVars tc
 1629         fam_cos = assertPpr (tvs `equalLength` cos) (ppr tc <+> ppr cos) $
 1630                   map (liftCoSubstWith Nominal tvs cos) fam_tys
 1631   = mkTyConAppCo Nominal fam_tc fam_cos
 1632   | otherwise
 1633   = mkTyConAppCo Nominal tc cos
 1634 
 1635 -- See note [Newtype coercions] in GHC.Core.TyCon
 1636 
 1637 mkPiCos :: Role -> [Var] -> Coercion -> Coercion
 1638 mkPiCos r vs co = foldr (mkPiCo r) co vs
 1639 
 1640 -- | Make a forall 'Coercion', where both types related by the coercion
 1641 -- are quantified over the same variable.
 1642 mkPiCo  :: Role -> Var -> Coercion -> Coercion
 1643 mkPiCo r v co | isTyVar v = mkHomoForAllCos [v] co
 1644               | isCoVar v = assert (not (v `elemVarSet` tyCoVarsOfCo co)) $
 1645                   -- We didn't call mkForAllCo here because if v does not appear
 1646                   -- in co, the argement coercion will be nominal. But here we
 1647                   -- want it to be r. It is only called in 'mkPiCos', which is
 1648                   -- only used in GHC.Core.Opt.Simplify.Utils, where we are sure for
 1649                   -- now (Aug 2018) v won't occur in co.
 1650                             mkFunResCo r scaled_ty co
 1651               | otherwise = mkFunResCo r scaled_ty co
 1652               where
 1653                 scaled_ty = Scaled (varMult v) (varType v)
 1654 
 1655 mkFunResCo :: Role -> Scaled Type -> Coercion -> Coercion
 1656 -- Given res_co :: res1 -> res2,
 1657 --   mkFunResCo r m arg res_co :: (arg -> res1) ~r (arg -> res2)
 1658 -- Reflexive in the multiplicity argument
 1659 mkFunResCo role (Scaled mult arg_ty) res_co
 1660   = mkFunCo role (multToCo mult) (mkReflCo role arg_ty) res_co
 1661 
 1662 -- mkCoCast (c :: s1 ~?r t1) (g :: (s1 ~?r t1) ~#R (s2 ~?r t2)) :: s2 ~?r t2
 1663 -- The first coercion might be lifted or unlifted; thus the ~? above
 1664 -- Lifted and unlifted equalities take different numbers of arguments,
 1665 -- so we have to make sure to supply the right parameter to decomposeCo.
 1666 -- Also, note that the role of the first coercion is the same as the role of
 1667 -- the equalities related by the second coercion. The second coercion is
 1668 -- itself always representational.
 1669 mkCoCast :: Coercion -> CoercionR -> Coercion
 1670 mkCoCast c g
 1671   | (g2:g1:_) <- reverse co_list
 1672   = mkSymCo g1 `mkTransCo` c `mkTransCo` g2
 1673 
 1674   | otherwise
 1675   = pprPanic "mkCoCast" (ppr g $$ ppr (coercionKind g))
 1676   where
 1677     -- g  :: (s1 ~# t1) ~# (s2 ~# t2)
 1678     -- g1 :: s1 ~# s2
 1679     -- g2 :: t1 ~# t2
 1680     (tc, _) = splitTyConApp (coercionLKind g)
 1681     co_list = decomposeCo (tyConArity tc) g (tyConRolesRepresentational tc)
 1682 
 1683 {- Note [castCoercionKind1]
 1684 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1685 castCoercionKind1 deals with the very important special case of castCoercionKind2
 1686 where the two kind coercions are identical.  In that case we can exploit the
 1687 situation where the main coercion is reflexive, via the special cases for Refl
 1688 and GRefl.
 1689 
 1690 This is important when rewriting  (ty |> co). We rewrite ty, yielding
 1691    fco :: ty ~ ty'
 1692 and now we want a coercion xco between
 1693    xco :: (ty |> co) ~ (ty' |> co)
 1694 That's exactly what castCoercionKind1 does.  And it's very very common for
 1695 fco to be Refl.  In that case we do NOT want to get some terrible composition
 1696 of mkLeftCoherenceCo and mkRightCoherenceCo, which is what castCoercionKind2
 1697 has to do in its full generality.  See #18413.
 1698 -}
 1699 
 1700 {-
 1701 %************************************************************************
 1702 %*                                                                      *
 1703             Newtypes
 1704 %*                                                                      *
 1705 %************************************************************************
 1706 -}
 1707 
 1708 -- | If @co :: T ts ~ rep_ty@ then:
 1709 --
 1710 -- > instNewTyCon_maybe T ts = Just (rep_ty, co)
 1711 --
 1712 -- Checks for a newtype, and for being saturated
 1713 instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, Coercion)
 1714 instNewTyCon_maybe tc tys
 1715   | Just (tvs, ty, co_tc) <- unwrapNewTyConEtad_maybe tc  -- Check for newtype
 1716   , tvs `leLength` tys                                    -- Check saturated enough
 1717   = Just (applyTysX tvs ty tys, mkUnbranchedAxInstCo Representational co_tc tys [])
 1718   | otherwise
 1719   = Nothing
 1720 
 1721 {-
 1722 ************************************************************************
 1723 *                                                                      *
 1724          Type normalisation
 1725 *                                                                      *
 1726 ************************************************************************
 1727 -}
 1728 
 1729 -- | A function to check if we can reduce a type by one step. Used
 1730 -- with 'topNormaliseTypeX'.
 1731 type NormaliseStepper ev = RecTcChecker
 1732                          -> TyCon     -- tc
 1733                          -> [Type]    -- tys
 1734                          -> NormaliseStepResult ev
 1735 
 1736 -- | The result of stepping in a normalisation function.
 1737 -- See 'topNormaliseTypeX'.
 1738 data NormaliseStepResult ev
 1739   = NS_Done   -- ^ Nothing more to do
 1740   | NS_Abort  -- ^ Utter failure. The outer function should fail too.
 1741   | NS_Step RecTcChecker Type ev    -- ^ We stepped, yielding new bits;
 1742                                     -- ^ ev is evidence;
 1743                                     -- Usually a co :: old type ~ new type
 1744 
 1745 instance Outputable ev => Outputable (NormaliseStepResult ev) where
 1746   ppr NS_Done           = text "NS_Done"
 1747   ppr NS_Abort          = text "NS_Abort"
 1748   ppr (NS_Step _ ty ev) = sep [text "NS_Step", ppr ty, ppr ev]
 1749 
 1750 mapStepResult :: (ev1 -> ev2)
 1751               -> NormaliseStepResult ev1 -> NormaliseStepResult ev2
 1752 mapStepResult f (NS_Step rec_nts ty ev) = NS_Step rec_nts ty (f ev)
 1753 mapStepResult _ NS_Done                 = NS_Done
 1754 mapStepResult _ NS_Abort                = NS_Abort
 1755 
 1756 -- | Try one stepper and then try the next, if the first doesn't make
 1757 -- progress.
 1758 -- So if it returns NS_Done, it means that both steppers are satisfied
 1759 composeSteppers :: NormaliseStepper ev -> NormaliseStepper ev
 1760                 -> NormaliseStepper ev
 1761 composeSteppers step1 step2 rec_nts tc tys
 1762   = case step1 rec_nts tc tys of
 1763       success@(NS_Step {}) -> success
 1764       NS_Done              -> step2 rec_nts tc tys
 1765       NS_Abort             -> NS_Abort
 1766 
 1767 -- | A 'NormaliseStepper' that unwraps newtypes, careful not to fall into
 1768 -- a loop. If it would fall into a loop, it produces 'NS_Abort'.
 1769 unwrapNewTypeStepper :: NormaliseStepper Coercion
 1770 unwrapNewTypeStepper rec_nts tc tys
 1771   | Just (ty', co) <- instNewTyCon_maybe tc tys
 1772   = case checkRecTc rec_nts tc of
 1773       Just rec_nts' -> NS_Step rec_nts' ty' co
 1774       Nothing       -> NS_Abort
 1775 
 1776   | otherwise
 1777   = NS_Done
 1778 
 1779 -- | A general function for normalising the top-level of a type. It continues
 1780 -- to use the provided 'NormaliseStepper' until that function fails, and then
 1781 -- this function returns. The roles of the coercions produced by the
 1782 -- 'NormaliseStepper' must all be the same, which is the role returned from
 1783 -- the call to 'topNormaliseTypeX'.
 1784 --
 1785 -- Typically ev is Coercion.
 1786 --
 1787 -- If topNormaliseTypeX step plus ty = Just (ev, ty')
 1788 -- then ty ~ev1~ t1 ~ev2~ t2 ... ~evn~ ty'
 1789 -- and ev = ev1 `plus` ev2 `plus` ... `plus` evn
 1790 -- If it returns Nothing then no newtype unwrapping could happen
 1791 topNormaliseTypeX :: NormaliseStepper ev
 1792                   -> (ev -> ev -> ev)
 1793                   -> Type -> Maybe (ev, Type)
 1794 topNormaliseTypeX stepper plus ty
 1795  | Just (tc, tys) <- splitTyConApp_maybe ty
 1796  , NS_Step rec_nts ty' ev <- stepper initRecTc tc tys
 1797  = go rec_nts ev ty'
 1798  | otherwise
 1799  = Nothing
 1800  where
 1801     go rec_nts ev ty
 1802       | Just (tc, tys) <- splitTyConApp_maybe ty
 1803       = case stepper rec_nts tc tys of
 1804           NS_Step rec_nts' ty' ev' -> go rec_nts' (ev `plus` ev') ty'
 1805           NS_Done  -> Just (ev, ty)
 1806           NS_Abort -> Nothing
 1807 
 1808       | otherwise
 1809       = Just (ev, ty)
 1810 
 1811 topNormaliseNewType_maybe :: Type -> Maybe (Coercion, Type)
 1812 -- ^ Sometimes we want to look through a @newtype@ and get its associated coercion.
 1813 -- This function strips off @newtype@ layers enough to reveal something that isn't
 1814 -- a @newtype@.  Specifically, here's the invariant:
 1815 --
 1816 -- > topNormaliseNewType_maybe rec_nts ty = Just (co, ty')
 1817 --
 1818 -- then (a)  @co : ty ~ ty'@.
 1819 --      (b)  ty' is not a newtype.
 1820 --
 1821 -- The function returns @Nothing@ for non-@newtypes@,
 1822 -- or unsaturated applications
 1823 --
 1824 -- This function does *not* look through type families, because it has no access to
 1825 -- the type family environment. If you do have that at hand, consider to use
 1826 -- topNormaliseType_maybe, which should be a drop-in replacement for
 1827 -- topNormaliseNewType_maybe
 1828 -- If topNormliseNewType_maybe ty = Just (co, ty'), then co : ty ~R ty'
 1829 topNormaliseNewType_maybe ty
 1830   = topNormaliseTypeX unwrapNewTypeStepper mkTransCo ty
 1831 
 1832 {-
 1833 %************************************************************************
 1834 %*                                                                      *
 1835                    Comparison of coercions
 1836 %*                                                                      *
 1837 %************************************************************************
 1838 -}
 1839 
 1840 -- | Syntactic equality of coercions
 1841 eqCoercion :: Coercion -> Coercion -> Bool
 1842 eqCoercion = eqType `on` coercionType
 1843 
 1844 -- | Compare two 'Coercion's, with respect to an RnEnv2
 1845 eqCoercionX :: RnEnv2 -> Coercion -> Coercion -> Bool
 1846 eqCoercionX env = eqTypeX env `on` coercionType
 1847 
 1848 {-
 1849 %************************************************************************
 1850 %*                                                                      *
 1851                    "Lifting" substitution
 1852            [(TyCoVar,Coercion)] -> Type -> Coercion
 1853 %*                                                                      *
 1854 %************************************************************************
 1855 
 1856 Note [Lifting coercions over types: liftCoSubst]
 1857 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1858 The KPUSH rule deals with this situation
 1859    data T a = K (a -> Maybe a)
 1860    g :: T t1 ~ T t2
 1861    x :: t1 -> Maybe t1
 1862 
 1863    case (K @t1 x) |> g of
 1864      K (y:t2 -> Maybe t2) -> rhs
 1865 
 1866 We want to push the coercion inside the constructor application.
 1867 So we do this
 1868 
 1869    g' :: t1~t2  =  Nth 0 g
 1870 
 1871    case K @t2 (x |> g' -> Maybe g') of
 1872      K (y:t2 -> Maybe t2) -> rhs
 1873 
 1874 The crucial operation is that we
 1875   * take the type of K's argument: a -> Maybe a
 1876   * and substitute g' for a
 1877 thus giving *coercion*.  This is what liftCoSubst does.
 1878 
 1879 In the presence of kind coercions, this is a bit
 1880 of a hairy operation. So, we refer you to the paper introducing kind coercions,
 1881 available at www.cis.upenn.edu/~sweirich/papers/fckinds-extended.pdf
 1882 
 1883 Note [extendLiftingContextEx]
 1884 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1885 Consider we have datatype
 1886   K :: \/k. \/a::k. P -> T k  -- P be some type
 1887   g :: T k1 ~ T k2
 1888 
 1889   case (K @k1 @t1 x) |> g of
 1890     K y -> rhs
 1891 
 1892 We want to push the coercion inside the constructor application.
 1893 We first get the coercion mapped by the universal type variable k:
 1894    lc = k |-> Nth 0 g :: k1~k2
 1895 
 1896 Here, the important point is that the kind of a is coerced, and P might be
 1897 dependent on the existential type variable a.
 1898 Thus we first get the coercion of a's kind
 1899    g2 = liftCoSubst lc k :: k1 ~ k2
 1900 
 1901 Then we store a new mapping into the lifting context
 1902    lc2 = a |-> (t1 ~ t1 |> g2), lc
 1903 
 1904 So later when we can correctly deal with the argument type P
 1905    liftCoSubst lc2 P :: P [k|->k1][a|->t1] ~ P[k|->k2][a |-> (t1|>g2)]
 1906 
 1907 This is exactly what extendLiftingContextEx does.
 1908 * For each (tyvar:k, ty) pair, we product the mapping
 1909     tyvar |-> (ty ~ ty |> (liftCoSubst lc k))
 1910 * For each (covar:s1~s2, ty) pair, we produce the mapping
 1911     covar |-> (co ~ co')
 1912     co' = Sym (liftCoSubst lc s1) ;; covar ;; liftCoSubst lc s2 :: s1'~s2'
 1913 
 1914 This follows the lifting context extension definition in the
 1915 "FC with Explicit Kind Equality" paper.
 1916 -}
 1917 
 1918 -- ----------------------------------------------------
 1919 -- See Note [Lifting coercions over types: liftCoSubst]
 1920 -- ----------------------------------------------------
 1921 
 1922 data LiftingContext = LC TCvSubst LiftCoEnv
 1923   -- in optCoercion, we need to lift when optimizing InstCo.
 1924   -- See Note [Optimising InstCo] in GHC.Core.Coercion.Opt
 1925   -- We thus propagate the substitution from GHC.Core.Coercion.Opt here.
 1926 
 1927 instance Outputable LiftingContext where
 1928   ppr (LC _ env) = hang (text "LiftingContext:") 2 (ppr env)
 1929 
 1930 type LiftCoEnv = VarEnv Coercion
 1931      -- Maps *type variables* to *coercions*.
 1932      -- That's the whole point of this function!
 1933      -- Also maps coercion variables to ProofIrrelCos.
 1934 
 1935 -- like liftCoSubstWith, but allows for existentially-bound types as well
 1936 liftCoSubstWithEx :: Role          -- desired role for output coercion
 1937                   -> [TyVar]       -- universally quantified tyvars
 1938                   -> [Coercion]    -- coercions to substitute for those
 1939                   -> [TyCoVar]     -- existentially quantified tycovars
 1940                   -> [Type]        -- types and coercions to be bound to ex vars
 1941                   -> (Type -> Coercion, [Type]) -- (lifting function, converted ex args)
 1942 liftCoSubstWithEx role univs omegas exs rhos
 1943   = let theta = mkLiftingContext (zipEqual "liftCoSubstWithExU" univs omegas)
 1944         psi   = extendLiftingContextEx theta (zipEqual "liftCoSubstWithExX" exs rhos)
 1945     in (ty_co_subst psi role, substTys (lcSubstRight psi) (mkTyCoVarTys exs))
 1946 
 1947 liftCoSubstWith :: Role -> [TyCoVar] -> [Coercion] -> Type -> Coercion
 1948 liftCoSubstWith r tvs cos ty
 1949   = liftCoSubst r (mkLiftingContext $ zipEqual "liftCoSubstWith" tvs cos) ty
 1950 
 1951 -- | @liftCoSubst role lc ty@ produces a coercion (at role @role@)
 1952 -- that coerces between @lc_left(ty)@ and @lc_right(ty)@, where
 1953 -- @lc_left@ is a substitution mapping type variables to the left-hand
 1954 -- types of the mapped coercions in @lc@, and similar for @lc_right@.
 1955 liftCoSubst :: HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion
 1956 {-# INLINE liftCoSubst #-}
 1957 -- Inlining this function is worth 2% of allocation in T9872d,
 1958 liftCoSubst r lc@(LC subst env) ty
 1959   | isEmptyVarEnv env = mkReflCo r (substTy subst ty)
 1960   | otherwise         = ty_co_subst lc r ty
 1961 
 1962 emptyLiftingContext :: InScopeSet -> LiftingContext
 1963 emptyLiftingContext in_scope = LC (mkEmptyTCvSubst in_scope) emptyVarEnv
 1964 
 1965 mkLiftingContext :: [(TyCoVar,Coercion)] -> LiftingContext
 1966 mkLiftingContext pairs
 1967   = LC (mkEmptyTCvSubst $ mkInScopeSet $ tyCoVarsOfCos (map snd pairs))
 1968        (mkVarEnv pairs)
 1969 
 1970 mkSubstLiftingContext :: TCvSubst -> LiftingContext
 1971 mkSubstLiftingContext subst = LC subst emptyVarEnv
 1972 
 1973 -- | Extend a lifting context with a new mapping.
 1974 extendLiftingContext :: LiftingContext  -- ^ original LC
 1975                      -> TyCoVar         -- ^ new variable to map...
 1976                      -> Coercion        -- ^ ...to this lifted version
 1977                      -> LiftingContext
 1978     -- mappings to reflexive coercions are just substitutions
 1979 extendLiftingContext (LC subst env) tv arg
 1980   | Just (ty, _) <- isReflCo_maybe arg
 1981   = LC (extendTCvSubst subst tv ty) env
 1982   | otherwise
 1983   = LC subst (extendVarEnv env tv arg)
 1984 
 1985 -- | Extend a lifting context with a new mapping, and extend the in-scope set
 1986 extendLiftingContextAndInScope :: LiftingContext  -- ^ Original LC
 1987                                -> TyCoVar         -- ^ new variable to map...
 1988                                -> Coercion        -- ^ to this coercion
 1989                                -> LiftingContext
 1990 extendLiftingContextAndInScope (LC subst env) tv co
 1991   = extendLiftingContext (LC (extendTCvInScopeSet subst (tyCoVarsOfCo co)) env) tv co
 1992 
 1993 -- | Extend a lifting context with existential-variable bindings.
 1994 -- See Note [extendLiftingContextEx]
 1995 extendLiftingContextEx :: LiftingContext    -- ^ original lifting context
 1996                        -> [(TyCoVar,Type)]  -- ^ ex. var / value pairs
 1997                        -> LiftingContext
 1998 -- Note that this is more involved than extendLiftingContext. That function
 1999 -- takes a coercion to extend with, so it's assumed that the caller has taken
 2000 -- into account any of the kind-changing stuff worried about here.
 2001 extendLiftingContextEx lc [] = lc
 2002 extendLiftingContextEx lc@(LC subst env) ((v,ty):rest)
 2003 -- This function adds bindings for *Nominal* coercions. Why? Because it
 2004 -- works with existentially bound variables, which are considered to have
 2005 -- nominal roles.
 2006   | isTyVar v
 2007   = let lc' = LC (subst `extendTCvInScopeSet` tyCoVarsOfType ty)
 2008                  (extendVarEnv env v $
 2009                   mkGReflRightCo Nominal
 2010                                  ty
 2011                                  (ty_co_subst lc Nominal (tyVarKind v)))
 2012     in extendLiftingContextEx lc' rest
 2013   | CoercionTy co <- ty
 2014   = -- co      :: s1 ~r s2
 2015     -- lift_s1 :: s1 ~r s1'
 2016     -- lift_s2 :: s2 ~r s2'
 2017     -- kco     :: (s1 ~r s2) ~N (s1' ~r s2')
 2018     assert (isCoVar v) $
 2019     let (_, _, s1, s2, r) = coVarKindsTypesRole v
 2020         lift_s1 = ty_co_subst lc r s1
 2021         lift_s2 = ty_co_subst lc r s2
 2022         kco     = mkTyConAppCo Nominal (equalityTyCon r)
 2023                                [ mkKindCo lift_s1, mkKindCo lift_s2
 2024                                , lift_s1         , lift_s2          ]
 2025         lc'     = LC (subst `extendTCvInScopeSet` tyCoVarsOfCo co)
 2026                      (extendVarEnv env v
 2027                         (mkProofIrrelCo Nominal kco co $
 2028                           (mkSymCo lift_s1) `mkTransCo` co `mkTransCo` lift_s2))
 2029     in extendLiftingContextEx lc' rest
 2030   | otherwise
 2031   = pprPanic "extendLiftingContextEx" (ppr v <+> text "|->" <+> ppr ty)
 2032 
 2033 
 2034 -- | Erase the environments in a lifting context
 2035 zapLiftingContext :: LiftingContext -> LiftingContext
 2036 zapLiftingContext (LC subst _) = LC (zapTCvSubst subst) emptyVarEnv
 2037 
 2038 -- | Like 'substForAllCoBndr', but works on a lifting context
 2039 substForAllCoBndrUsingLC :: Bool
 2040                             -> (Coercion -> Coercion)
 2041                             -> LiftingContext -> TyCoVar -> Coercion
 2042                             -> (LiftingContext, TyCoVar, Coercion)
 2043 substForAllCoBndrUsingLC sym sco (LC subst lc_env) tv co
 2044   = (LC subst' lc_env, tv', co')
 2045   where
 2046     (subst', tv', co') = substForAllCoBndrUsing sym sco subst tv co
 2047 
 2048 -- | The \"lifting\" operation which substitutes coercions for type
 2049 --   variables in a type to produce a coercion.
 2050 --
 2051 --   For the inverse operation, see 'liftCoMatch'
 2052 ty_co_subst :: LiftingContext -> Role -> Type -> Coercion
 2053 ty_co_subst !lc role ty
 2054     -- !lc: making this function strict in lc allows callers to
 2055     -- pass its two components separately, rather than boxing them
 2056   = go role ty
 2057   where
 2058     go :: Role -> Type -> Coercion
 2059     go r ty                | Just ty' <- coreView ty
 2060                            = go r ty'
 2061     go Phantom ty          = lift_phantom ty
 2062     go r (TyVarTy tv)      = expectJust "ty_co_subst bad roles" $
 2063                              liftCoSubstTyVar lc r tv
 2064     go r (AppTy ty1 ty2)   = mkAppCo (go r ty1) (go Nominal ty2)
 2065     go r (TyConApp tc tys) = mkTyConAppCo r tc (zipWith go (tyConRolesX r tc) tys)
 2066     go r (FunTy _ w ty1 ty2) = mkFunCo r (go Nominal w) (go r ty1) (go r ty2)
 2067     go r t@(ForAllTy (Bndr v _) ty)
 2068        = let (lc', v', h) = liftCoSubstVarBndr lc v
 2069              body_co = ty_co_subst lc' r ty in
 2070          if isTyVar v' || almostDevoidCoVarOfCo v' body_co
 2071            -- Lifting a ForAllTy over a coercion variable could fail as ForAllCo
 2072            -- imposes an extra restriction on where a covar can appear. See last
 2073            -- wrinkle in Note [Unused coercion variable in ForAllCo].
 2074            -- We specifically check for this and panic because we know that
 2075            -- there's a hole in the type system here, and we'd rather panic than
 2076            -- fall into it.
 2077          then mkForAllCo v' h body_co
 2078          else pprPanic "ty_co_subst: covar is not almost devoid" (ppr t)
 2079     go r ty@(LitTy {})     = assert (r == Nominal) $
 2080                              mkNomReflCo ty
 2081     go r (CastTy ty co)    = castCoercionKind (go r ty) (substLeftCo lc co)
 2082                                                         (substRightCo lc co)
 2083     go r (CoercionTy co)   = mkProofIrrelCo r kco (substLeftCo lc co)
 2084                                                   (substRightCo lc co)
 2085       where kco = go Nominal (coercionType co)
 2086 
 2087     lift_phantom ty = mkPhantomCo (go Nominal (typeKind ty))
 2088                                   (substTy (lcSubstLeft  lc) ty)
 2089                                   (substTy (lcSubstRight lc) ty)
 2090 
 2091 {-
 2092 Note [liftCoSubstTyVar]
 2093 ~~~~~~~~~~~~~~~~~~~~~~~~~
 2094 This function can fail if a coercion in the environment is of too low a role.
 2095 
 2096 liftCoSubstTyVar is called from two places: in liftCoSubst (naturally), and
 2097 also in matchAxiom in GHC.Core.Coercion.Opt. From liftCoSubst, the so-called lifting
 2098 lemma guarantees that the roles work out. If we fail in this
 2099 case, we really should panic -- something is deeply wrong. But, in matchAxiom,
 2100 failing is fine. matchAxiom is trying to find a set of coercions
 2101 that match, but it may fail, and this is healthy behavior.
 2102 -}
 2103 
 2104 -- See Note [liftCoSubstTyVar]
 2105 liftCoSubstTyVar :: LiftingContext -> Role -> TyVar -> Maybe Coercion
 2106 liftCoSubstTyVar (LC subst env) r v
 2107   | Just co_arg <- lookupVarEnv env v
 2108   = downgradeRole_maybe r (coercionRole co_arg) co_arg
 2109 
 2110   | otherwise
 2111   = Just $ mkReflCo r (substTyVar subst v)
 2112 
 2113 {- Note [liftCoSubstVarBndr]
 2114 
 2115 callback:
 2116   'liftCoSubstVarBndrUsing' needs to be general enough to work in two
 2117   situations:
 2118 
 2119     - in this module, which manipulates 'Coercion's, and
 2120     - in GHC.Core.FamInstEnv, where we work with 'Reduction's, which contain
 2121       a coercion as well as a type.
 2122 
 2123   To achieve this, we require that the return type of the 'callback' function
 2124   contain a coercion within it. This is witnessed by the first argument
 2125   to 'liftCoSubstVarBndrUsing': a getter, which allows us to retrieve
 2126   the coercion inside the return type. Thus:
 2127 
 2128     - in this module, we simply pass 'id' as the getter,
 2129     - in GHC.Core.FamInstEnv, we pass 'reductionCoercion' as the getter.
 2130 
 2131 liftCoSubstTyVarBndrUsing:
 2132   Given
 2133     forall tv:k. t
 2134   We want to get
 2135     forall (tv:k1) (kind_co :: k1 ~ k2) body_co
 2136 
 2137   We lift the kind k to get the kind_co
 2138     kind_co = ty_co_subst k :: k1 ~ k2
 2139 
 2140   Now in the LiftingContext, we add the new mapping
 2141     tv |-> (tv :: k1) ~ ((tv |> kind_co) :: k2)
 2142 
 2143 liftCoSubstCoVarBndrUsing:
 2144   Given
 2145     forall cv:(s1 ~ s2). t
 2146   We want to get
 2147     forall (cv:s1'~s2') (kind_co :: (s1'~s2') ~ (t1 ~ t2)) body_co
 2148 
 2149   We lift s1 and s2 respectively to get
 2150     eta1 :: s1' ~ t1
 2151     eta2 :: s2' ~ t2
 2152   And
 2153     kind_co = TyConAppCo Nominal (~#) eta1 eta2
 2154 
 2155   Now in the liftingContext, we add the new mapping
 2156     cv |-> (cv :: s1' ~ s2') ~ ((sym eta1;cv;eta2) :: t1 ~ t2)
 2157 -}
 2158 
 2159 -- See Note [liftCoSubstVarBndr]
 2160 liftCoSubstVarBndr :: LiftingContext -> TyCoVar
 2161                    -> (LiftingContext, TyCoVar, Coercion)
 2162 liftCoSubstVarBndr lc tv
 2163   = liftCoSubstVarBndrUsing id callback lc tv
 2164   where
 2165     callback lc' ty' = ty_co_subst lc' Nominal ty'
 2166 
 2167 -- the callback must produce a nominal coercion
 2168 liftCoSubstVarBndrUsing :: (r -> CoercionN)              -- ^ coercion getter
 2169                         -> (LiftingContext -> Type -> r) -- ^ callback
 2170                         -> LiftingContext -> TyCoVar
 2171                         -> (LiftingContext, TyCoVar, r)
 2172 liftCoSubstVarBndrUsing view_co fun lc old_var
 2173   | isTyVar old_var
 2174   = liftCoSubstTyVarBndrUsing view_co fun lc old_var
 2175   | otherwise
 2176   = liftCoSubstCoVarBndrUsing view_co fun lc old_var
 2177 
 2178 -- Works for tyvar binder
 2179 liftCoSubstTyVarBndrUsing :: (r -> CoercionN)              -- ^ coercion getter
 2180                           -> (LiftingContext -> Type -> r) -- ^ callback
 2181                           -> LiftingContext -> TyVar
 2182                           -> (LiftingContext, TyVar, r)
 2183 liftCoSubstTyVarBndrUsing view_co fun lc@(LC subst cenv) old_var
 2184   = assert (isTyVar old_var) $
 2185     ( LC (subst `extendTCvInScope` new_var) new_cenv
 2186     , new_var, stuff )
 2187   where
 2188     old_kind = tyVarKind old_var
 2189     stuff    = fun lc old_kind
 2190     eta      = view_co stuff
 2191     k1       = coercionLKind eta
 2192     new_var  = uniqAway (getTCvInScope subst) (setVarType old_var k1)
 2193 
 2194     lifted   = mkGReflRightCo Nominal (TyVarTy new_var) eta
 2195                -- :: new_var ~ new_var |> eta
 2196     new_cenv = extendVarEnv cenv old_var lifted
 2197 
 2198 -- Works for covar binder
 2199 liftCoSubstCoVarBndrUsing :: (r -> CoercionN)              -- ^ coercion getter
 2200                           -> (LiftingContext -> Type -> r) -- ^ callback
 2201                           -> LiftingContext -> CoVar
 2202                           -> (LiftingContext, CoVar, r)
 2203 liftCoSubstCoVarBndrUsing view_co fun lc@(LC subst cenv) old_var
 2204   = assert (isCoVar old_var) $
 2205     ( LC (subst `extendTCvInScope` new_var) new_cenv
 2206     , new_var, stuff )
 2207   where
 2208     old_kind = coVarKind old_var
 2209     stuff    = fun lc old_kind
 2210     eta      = view_co stuff
 2211     k1       = coercionLKind eta
 2212     new_var  = uniqAway (getTCvInScope subst) (setVarType old_var k1)
 2213 
 2214     -- old_var :: s1  ~r s2
 2215     -- eta     :: (s1' ~r s2') ~N (t1 ~r t2)
 2216     -- eta1    :: s1' ~r t1
 2217     -- eta2    :: s2' ~r t2
 2218     -- co1     :: s1' ~r s2'
 2219     -- co2     :: t1  ~r t2
 2220     -- lifted  :: co1 ~N co2
 2221 
 2222     role   = coVarRole old_var
 2223     eta'   = downgradeRole role Nominal eta
 2224     eta1   = mkNthCo role 2 eta'
 2225     eta2   = mkNthCo role 3 eta'
 2226 
 2227     co1     = mkCoVarCo new_var
 2228     co2     = mkSymCo eta1 `mkTransCo` co1 `mkTransCo` eta2
 2229     lifted  = mkProofIrrelCo Nominal eta co1 co2
 2230 
 2231     new_cenv = extendVarEnv cenv old_var lifted
 2232 
 2233 -- | Is a var in the domain of a lifting context?
 2234 isMappedByLC :: TyCoVar -> LiftingContext -> Bool
 2235 isMappedByLC tv (LC _ env) = tv `elemVarEnv` env
 2236 
 2237 -- If [a |-> g] is in the substitution and g :: t1 ~ t2, substitute a for t1
 2238 -- If [a |-> (g1, g2)] is in the substitution, substitute a for g1
 2239 substLeftCo :: LiftingContext -> Coercion -> Coercion
 2240 substLeftCo lc co
 2241   = substCo (lcSubstLeft lc) co
 2242 
 2243 -- Ditto, but for t2 and g2
 2244 substRightCo :: LiftingContext -> Coercion -> Coercion
 2245 substRightCo lc co
 2246   = substCo (lcSubstRight lc) co
 2247 
 2248 -- | Apply "sym" to all coercions in a 'LiftCoEnv'
 2249 swapLiftCoEnv :: LiftCoEnv -> LiftCoEnv
 2250 swapLiftCoEnv = mapVarEnv mkSymCo
 2251 
 2252 lcSubstLeft :: LiftingContext -> TCvSubst
 2253 lcSubstLeft (LC subst lc_env) = liftEnvSubstLeft subst lc_env
 2254 
 2255 lcSubstRight :: LiftingContext -> TCvSubst
 2256 lcSubstRight (LC subst lc_env) = liftEnvSubstRight subst lc_env
 2257 
 2258 liftEnvSubstLeft :: TCvSubst -> LiftCoEnv -> TCvSubst
 2259 liftEnvSubstLeft = liftEnvSubst pFst
 2260 
 2261 liftEnvSubstRight :: TCvSubst -> LiftCoEnv -> TCvSubst
 2262 liftEnvSubstRight = liftEnvSubst pSnd
 2263 
 2264 liftEnvSubst :: (forall a. Pair a -> a) -> TCvSubst -> LiftCoEnv -> TCvSubst
 2265 liftEnvSubst selector subst lc_env
 2266   = composeTCvSubst (TCvSubst emptyInScopeSet tenv cenv) subst
 2267   where
 2268     pairs            = nonDetUFMToList lc_env
 2269                        -- It's OK to use nonDetUFMToList here because we
 2270                        -- immediately forget the ordering by creating
 2271                        -- a VarEnv
 2272     (tpairs, cpairs) = partitionWith ty_or_co pairs
 2273     tenv             = mkVarEnv_Directly tpairs
 2274     cenv             = mkVarEnv_Directly cpairs
 2275 
 2276     ty_or_co :: (Unique, Coercion) -> Either (Unique, Type) (Unique, Coercion)
 2277     ty_or_co (u, co)
 2278       | Just equality_co <- isCoercionTy_maybe equality_ty
 2279       = Right (u, equality_co)
 2280       | otherwise
 2281       = Left (u, equality_ty)
 2282       where
 2283         equality_ty = selector (coercionKind co)
 2284 
 2285 -- | Extract the underlying substitution from the LiftingContext
 2286 lcTCvSubst :: LiftingContext -> TCvSubst
 2287 lcTCvSubst (LC subst _) = subst
 2288 
 2289 -- | Get the 'InScopeSet' from a 'LiftingContext'
 2290 lcInScopeSet :: LiftingContext -> InScopeSet
 2291 lcInScopeSet (LC subst _) = getTCvInScope subst
 2292 
 2293 {-
 2294 %************************************************************************
 2295 %*                                                                      *
 2296             Sequencing on coercions
 2297 %*                                                                      *
 2298 %************************************************************************
 2299 -}
 2300 
 2301 seqMCo :: MCoercion -> ()
 2302 seqMCo MRefl    = ()
 2303 seqMCo (MCo co) = seqCo co
 2304 
 2305 seqCo :: Coercion -> ()
 2306 seqCo (Refl ty)                 = seqType ty
 2307 seqCo (GRefl r ty mco)          = r `seq` seqType ty `seq` seqMCo mco
 2308 seqCo (TyConAppCo r tc cos)     = r `seq` tc `seq` seqCos cos
 2309 seqCo (AppCo co1 co2)           = seqCo co1 `seq` seqCo co2
 2310 seqCo (ForAllCo tv k co)        = seqType (varType tv) `seq` seqCo k
 2311                                                        `seq` seqCo co
 2312 seqCo (FunCo r w co1 co2)       = r `seq` seqCo w `seq` seqCo co1 `seq` seqCo co2
 2313 seqCo (CoVarCo cv)              = cv `seq` ()
 2314 seqCo (HoleCo h)                = coHoleCoVar h `seq` ()
 2315 seqCo (AxiomInstCo con ind cos) = con `seq` ind `seq` seqCos cos
 2316 seqCo (UnivCo p r t1 t2)
 2317   = seqProv p `seq` r `seq` seqType t1 `seq` seqType t2
 2318 seqCo (SymCo co)                = seqCo co
 2319 seqCo (TransCo co1 co2)         = seqCo co1 `seq` seqCo co2
 2320 seqCo (NthCo r n co)            = r `seq` n `seq` seqCo co
 2321 seqCo (LRCo lr co)              = lr `seq` seqCo co
 2322 seqCo (InstCo co arg)           = seqCo co `seq` seqCo arg
 2323 seqCo (KindCo co)               = seqCo co
 2324 seqCo (SubCo co)                = seqCo co
 2325 seqCo (AxiomRuleCo _ cs)        = seqCos cs
 2326 
 2327 seqProv :: UnivCoProvenance -> ()
 2328 seqProv (PhantomProv co)    = seqCo co
 2329 seqProv (ProofIrrelProv co) = seqCo co
 2330 seqProv (PluginProv _)      = ()
 2331 seqProv (CorePrepProv _)    = ()
 2332 
 2333 seqCos :: [Coercion] -> ()
 2334 seqCos []       = ()
 2335 seqCos (co:cos) = seqCo co `seq` seqCos cos
 2336 
 2337 {-
 2338 %************************************************************************
 2339 %*                                                                      *
 2340              The kind of a type, and of a coercion
 2341 %*                                                                      *
 2342 %************************************************************************
 2343 -}
 2344 
 2345 -- | Apply 'coercionKind' to multiple 'Coercion's
 2346 coercionKinds :: [Coercion] -> Pair [Type]
 2347 coercionKinds tys = sequenceA $ map coercionKind tys
 2348 
 2349 -- | Get a coercion's kind and role.
 2350 coercionKindRole :: Coercion -> (Pair Type, Role)
 2351 coercionKindRole co = (coercionKind co, coercionRole co)
 2352 
 2353 coercionType :: Coercion -> Type
 2354 coercionType co = case coercionKindRole co of
 2355   (Pair ty1 ty2, r) -> mkCoercionType r ty1 ty2
 2356 
 2357 ------------------
 2358 -- | If it is the case that
 2359 --
 2360 -- > c :: (t1 ~ t2)
 2361 --
 2362 -- i.e. the kind of @c@ relates @t1@ and @t2@, then @coercionKind c = Pair t1 t2@.
 2363 
 2364 coercionKind :: Coercion -> Pair Type
 2365 coercionKind co = Pair (coercionLKind co) (coercionRKind co)
 2366 
 2367 coercionLKind :: Coercion -> Type
 2368 coercionLKind co
 2369   = go co
 2370   where
 2371     go (Refl ty)                = ty
 2372     go (GRefl _ ty _)           = ty
 2373     go (TyConAppCo _ tc cos)    = mkTyConApp tc (map go cos)
 2374     go (AppCo co1 co2)          = mkAppTy (go co1) (go co2)
 2375     go (ForAllCo tv1 _ co1)     = mkTyCoInvForAllTy tv1 (go co1)
 2376     go (FunCo _ w co1 co2)      = mkFunctionType (go w) (go co1) (go co2)
 2377     go (CoVarCo cv)             = coVarLType cv
 2378     go (HoleCo h)               = coVarLType (coHoleCoVar h)
 2379     go (UnivCo _ _ ty1 _)       = ty1
 2380     go (SymCo co)               = coercionRKind co
 2381     go (TransCo co1 _)          = go co1
 2382     go (LRCo lr co)             = pickLR lr (splitAppTy (go co))
 2383     go (InstCo aco arg)         = go_app aco [go arg]
 2384     go (KindCo co)              = typeKind (go co)
 2385     go (SubCo co)               = go co
 2386     go (NthCo _ d co)           = go_nth d (go co)
 2387     go (AxiomInstCo ax ind cos) = go_ax_inst ax ind (map go cos)
 2388     go (AxiomRuleCo ax cos)     = pFst $ expectJust "coercionKind" $
 2389                                   coaxrProves ax $ map coercionKind cos
 2390 
 2391     go_ax_inst ax ind tys
 2392       | CoAxBranch { cab_tvs = tvs, cab_cvs = cvs
 2393                    , cab_lhs = lhs } <- coAxiomNthBranch ax ind
 2394       , let (tys1, cotys1) = splitAtList tvs tys
 2395             cos1           = map stripCoercionTy cotys1
 2396       = assert (tys `equalLength` (tvs ++ cvs)) $
 2397                   -- Invariant of AxiomInstCo: cos should
 2398                   -- exactly saturate the axiom branch
 2399         substTyWith tvs tys1       $
 2400         substTyWithCoVars cvs cos1 $
 2401         mkTyConApp (coAxiomTyCon ax) lhs
 2402 
 2403     go_app :: Coercion -> [Type] -> Type
 2404     -- Collect up all the arguments and apply all at once
 2405     -- See Note [Nested InstCos]
 2406     go_app (InstCo co arg) args = go_app co (go arg:args)
 2407     go_app co              args = piResultTys (go co) args
 2408 
 2409 go_nth :: Int -> Type -> Type
 2410 go_nth d ty
 2411   | Just args <- tyConAppArgs_maybe ty
 2412   = assert (args `lengthExceeds` d) $
 2413     args `getNth` d
 2414 
 2415   | d == 0
 2416   , Just (tv,_) <- splitForAllTyCoVar_maybe ty
 2417   = tyVarKind tv
 2418 
 2419   | otherwise
 2420   = pprPanic "coercionLKind:nth" (ppr d <+> ppr ty)
 2421 
 2422 coercionRKind :: Coercion -> Type
 2423 coercionRKind co
 2424   = go co
 2425   where
 2426     go (Refl ty)                = ty
 2427     go (GRefl _ ty MRefl)       = ty
 2428     go (GRefl _ ty (MCo co1))   = mkCastTy ty co1
 2429     go (TyConAppCo _ tc cos)    = mkTyConApp tc (map go cos)
 2430     go (AppCo co1 co2)          = mkAppTy (go co1) (go co2)
 2431     go (CoVarCo cv)             = coVarRType cv
 2432     go (HoleCo h)               = coVarRType (coHoleCoVar h)
 2433     go (FunCo _ w co1 co2)      = mkFunctionType (go w) (go co1) (go co2)
 2434     go (UnivCo _ _ _ ty2)       = ty2
 2435     go (SymCo co)               = coercionLKind co
 2436     go (TransCo _ co2)          = go co2
 2437     go (LRCo lr co)             = pickLR lr (splitAppTy (go co))
 2438     go (InstCo aco arg)         = go_app aco [go arg]
 2439     go (KindCo co)              = typeKind (go co)
 2440     go (SubCo co)               = go co
 2441     go (NthCo _ d co)           = go_nth d (go co)
 2442     go (AxiomInstCo ax ind cos) = go_ax_inst ax ind (map go cos)
 2443     go (AxiomRuleCo ax cos)     = pSnd $ expectJust "coercionKind" $
 2444                                   coaxrProves ax $ map coercionKind cos
 2445 
 2446     go co@(ForAllCo tv1 k_co co1) -- works for both tyvar and covar
 2447        | isGReflCo k_co           = mkTyCoInvForAllTy tv1 (go co1)
 2448          -- kind_co always has kind @Type@, thus @isGReflCo@
 2449        | otherwise                = go_forall empty_subst co
 2450        where
 2451          empty_subst = mkEmptyTCvSubst (mkInScopeSet $ tyCoVarsOfCo co)
 2452 
 2453     go_ax_inst ax ind tys
 2454       | CoAxBranch { cab_tvs = tvs, cab_cvs = cvs
 2455                    , cab_rhs = rhs } <- coAxiomNthBranch ax ind
 2456       , let (tys2, cotys2) = splitAtList tvs tys
 2457             cos2           = map stripCoercionTy cotys2
 2458       = assert (tys `equalLength` (tvs ++ cvs)) $
 2459                   -- Invariant of AxiomInstCo: cos should
 2460                   -- exactly saturate the axiom branch
 2461         substTyWith tvs tys2 $
 2462         substTyWithCoVars cvs cos2 rhs
 2463 
 2464     go_app :: Coercion -> [Type] -> Type
 2465     -- Collect up all the arguments and apply all at once
 2466     -- See Note [Nested InstCos]
 2467     go_app (InstCo co arg) args = go_app co (go arg:args)
 2468     go_app co              args = piResultTys (go co) args
 2469 
 2470     go_forall subst (ForAllCo tv1 k_co co)
 2471       -- See Note [Nested ForAllCos]
 2472       | isTyVar tv1
 2473       = mkInfForAllTy tv2 (go_forall subst' co)
 2474       where
 2475         k2  = coercionRKind k_co
 2476         tv2 = setTyVarKind tv1 (substTy subst k2)
 2477         subst' | isGReflCo k_co = extendTCvInScope subst tv1
 2478                  -- kind_co always has kind @Type@, thus @isGReflCo@
 2479                | otherwise      = extendTvSubst (extendTCvInScope subst tv2) tv1 $
 2480                                   TyVarTy tv2 `mkCastTy` mkSymCo k_co
 2481 
 2482     go_forall subst (ForAllCo cv1 k_co co)
 2483       | isCoVar cv1
 2484       = mkTyCoInvForAllTy cv2 (go_forall subst' co)
 2485       where
 2486         k2 = coercionRKind k_co
 2487         r         = coVarRole cv1
 2488         eta1      = mkNthCo r 2 (downgradeRole r Nominal k_co)
 2489         eta2      = mkNthCo r 3 (downgradeRole r Nominal k_co)
 2490 
 2491         -- k_co :: (t1 ~r t2) ~N (s1 ~r s2)
 2492         -- k1    = t1 ~r t2
 2493         -- k2    = s1 ~r s2
 2494         -- cv1  :: t1 ~r t2
 2495         -- cv2  :: s1 ~r s2
 2496         -- eta1 :: t1 ~r s1
 2497         -- eta2 :: t2 ~r s2
 2498         -- n_subst  = (eta1 ; cv2 ; sym eta2) :: t1 ~r t2
 2499 
 2500         cv2     = setVarType cv1 (substTy subst k2)
 2501         n_subst = eta1 `mkTransCo` (mkCoVarCo cv2) `mkTransCo` (mkSymCo eta2)
 2502         subst'  | isReflCo k_co = extendTCvInScope subst cv1
 2503                 | otherwise     = extendCvSubst (extendTCvInScope subst cv2)
 2504                                                 cv1 n_subst
 2505 
 2506     go_forall subst other_co
 2507       -- when other_co is not a ForAllCo
 2508       = substTy subst (go other_co)
 2509 
 2510 {-
 2511 
 2512 Note [Nested ForAllCos]
 2513 ~~~~~~~~~~~~~~~~~~~~~~~
 2514 
 2515 Suppose we need `coercionKind (ForAllCo a1 (ForAllCo a2 ... (ForAllCo an
 2516 co)...) )`.   We do not want to perform `n` single-type-variable
 2517 substitutions over the kind of `co`; rather we want to do one substitution
 2518 which substitutes for all of `a1`, `a2` ... simultaneously.  If we do one
 2519 at a time we get the performance hole reported in #11735.
 2520 
 2521 Solution: gather up the type variables for nested `ForAllCos`, and
 2522 substitute for them all at once.  Remarkably, for #11735 this single
 2523 change reduces /total/ compile time by a factor of more than ten.
 2524 
 2525 -}
 2526 
 2527 -- | Retrieve the role from a coercion.
 2528 coercionRole :: Coercion -> Role
 2529 coercionRole = go
 2530   where
 2531     go (Refl _) = Nominal
 2532     go (GRefl r _ _) = r
 2533     go (TyConAppCo r _ _) = r
 2534     go (AppCo co1 _) = go co1
 2535     go (ForAllCo _ _ co) = go co
 2536     go (FunCo r _ _ _) = r
 2537     go (CoVarCo cv) = coVarRole cv
 2538     go (HoleCo h)   = coVarRole (coHoleCoVar h)
 2539     go (AxiomInstCo ax _ _) = coAxiomRole ax
 2540     go (UnivCo _ r _ _)  = r
 2541     go (SymCo co) = go co
 2542     go (TransCo co1 _co2) = go co1
 2543     go (NthCo r _d _co) = r
 2544     go (LRCo {}) = Nominal
 2545     go (InstCo co _) = go co
 2546     go (KindCo {}) = Nominal
 2547     go (SubCo _) = Representational
 2548     go (AxiomRuleCo ax _) = coaxrRole ax
 2549 
 2550 {-
 2551 Note [Nested InstCos]
 2552 ~~~~~~~~~~~~~~~~~~~~~
 2553 In #5631 we found that 70% of the entire compilation time was
 2554 being spent in coercionKind!  The reason was that we had
 2555    (g @ ty1 @ ty2 .. @ ty100)    -- The "@s" are InstCos
 2556 where
 2557    g :: forall a1 a2 .. a100. phi
 2558 If we deal with the InstCos one at a time, we'll do this:
 2559    1.  Find the kind of (g @ ty1 .. @ ty99) : forall a100. phi'
 2560    2.  Substitute phi'[ ty100/a100 ], a single tyvar->type subst
 2561 But this is a *quadratic* algorithm, and the blew up #5631.
 2562 So it's very important to do the substitution simultaneously;
 2563 cf Type.piResultTys (which in fact we call here).
 2564 
 2565 -}
 2566 
 2567 -- | Makes a coercion type from two types: the types whose equality
 2568 -- is proven by the relevant 'Coercion'
 2569 mkCoercionType :: Role -> Type -> Type -> Type
 2570 mkCoercionType Nominal          = mkPrimEqPred
 2571 mkCoercionType Representational = mkReprPrimEqPred
 2572 mkCoercionType Phantom          = \ty1 ty2 ->
 2573   let ki1 = typeKind ty1
 2574       ki2 = typeKind ty2
 2575   in
 2576   TyConApp eqPhantPrimTyCon [ki1, ki2, ty1, ty2]
 2577 
 2578 mkHeteroCoercionType :: Role -> Kind -> Kind -> Type -> Type -> Type
 2579 mkHeteroCoercionType Nominal          = mkHeteroPrimEqPred
 2580 mkHeteroCoercionType Representational = mkHeteroReprPrimEqPred
 2581 mkHeteroCoercionType Phantom          = panic "mkHeteroCoercionType"
 2582 
 2583 -- | Creates a primitive type equality predicate.
 2584 -- Invariant: the types are not Coercions
 2585 mkPrimEqPred :: Type -> Type -> Type
 2586 mkPrimEqPred ty1 ty2
 2587   = mkTyConApp eqPrimTyCon [k1, k2, ty1, ty2]
 2588   where
 2589     k1 = typeKind ty1
 2590     k2 = typeKind ty2
 2591 
 2592 -- | Makes a lifted equality predicate at the given role
 2593 mkPrimEqPredRole :: Role -> Type -> Type -> PredType
 2594 mkPrimEqPredRole Nominal          = mkPrimEqPred
 2595 mkPrimEqPredRole Representational = mkReprPrimEqPred
 2596 mkPrimEqPredRole Phantom          = panic "mkPrimEqPredRole phantom"
 2597 
 2598 -- | Creates a primitive type equality predicate with explicit kinds
 2599 mkHeteroPrimEqPred :: Kind -> Kind -> Type -> Type -> Type
 2600 mkHeteroPrimEqPred k1 k2 ty1 ty2 = mkTyConApp eqPrimTyCon [k1, k2, ty1, ty2]
 2601 
 2602 -- | Creates a primitive representational type equality predicate
 2603 -- with explicit kinds
 2604 mkHeteroReprPrimEqPred :: Kind -> Kind -> Type -> Type -> Type
 2605 mkHeteroReprPrimEqPred k1 k2 ty1 ty2
 2606   = mkTyConApp eqReprPrimTyCon [k1, k2, ty1, ty2]
 2607 
 2608 mkReprPrimEqPred :: Type -> Type -> Type
 2609 mkReprPrimEqPred ty1  ty2
 2610   = mkTyConApp eqReprPrimTyCon [k1, k2, ty1, ty2]
 2611   where
 2612     k1 = typeKind ty1
 2613     k2 = typeKind ty2
 2614 
 2615 -- | Assuming that two types are the same, ignoring coercions, find
 2616 -- a nominal coercion between the types. This is useful when optimizing
 2617 -- transitivity over coercion applications, where splitting two
 2618 -- AppCos might yield different kinds. See Note [EtaAppCo] in
 2619 -- "GHC.Core.Coercion.Opt".
 2620 buildCoercion :: Type -> Type -> CoercionN
 2621 buildCoercion orig_ty1 orig_ty2 = go orig_ty1 orig_ty2
 2622   where
 2623     go ty1 ty2 | Just ty1' <- coreView ty1 = go ty1' ty2
 2624                | Just ty2' <- coreView ty2 = go ty1 ty2'
 2625 
 2626     go (CastTy ty1 co) ty2
 2627       = let co' = go ty1 ty2
 2628             r = coercionRole co'
 2629         in  mkCoherenceLeftCo r ty1 co co'
 2630 
 2631     go ty1 (CastTy ty2 co)
 2632       = let co' = go ty1 ty2
 2633             r = coercionRole co'
 2634         in  mkCoherenceRightCo r ty2 co co'
 2635 
 2636     go ty1@(TyVarTy tv1) _tyvarty
 2637       = assert (case _tyvarty of
 2638                   { TyVarTy tv2 -> tv1 == tv2
 2639                   ; _           -> False      }) $
 2640         mkNomReflCo ty1
 2641 
 2642     go (FunTy { ft_mult = w1, ft_arg = arg1, ft_res = res1 })
 2643        (FunTy { ft_mult = w2, ft_arg = arg2, ft_res = res2 })
 2644       = mkFunCo Nominal (go w1 w2) (go arg1 arg2) (go res1 res2)
 2645 
 2646     go (TyConApp tc1 args1) (TyConApp tc2 args2)
 2647       = assert (tc1 == tc2) $
 2648         mkTyConAppCo Nominal tc1 (zipWith go args1 args2)
 2649 
 2650     go (AppTy ty1a ty1b) ty2
 2651       | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
 2652       = mkAppCo (go ty1a ty2a) (go ty1b ty2b)
 2653 
 2654     go ty1 (AppTy ty2a ty2b)
 2655       | Just (ty1a, ty1b) <- repSplitAppTy_maybe ty1
 2656       = mkAppCo (go ty1a ty2a) (go ty1b ty2b)
 2657 
 2658     go (ForAllTy (Bndr tv1 _flag1) ty1) (ForAllTy (Bndr tv2 _flag2) ty2)
 2659       | isTyVar tv1
 2660       = assert (isTyVar tv2) $
 2661         mkForAllCo tv1 kind_co (go ty1 ty2')
 2662       where kind_co  = go (tyVarKind tv1) (tyVarKind tv2)
 2663             in_scope = mkInScopeSet $ tyCoVarsOfType ty2 `unionVarSet` tyCoVarsOfCo kind_co
 2664             ty2'     = substTyWithInScope in_scope [tv2]
 2665                          [mkTyVarTy tv1 `mkCastTy` kind_co]
 2666                          ty2
 2667 
 2668     go (ForAllTy (Bndr cv1 _flag1) ty1) (ForAllTy (Bndr cv2 _flag2) ty2)
 2669       = assert (isCoVar cv1 && isCoVar cv2) $
 2670         mkForAllCo cv1 kind_co (go ty1 ty2')
 2671       where s1 = varType cv1
 2672             s2 = varType cv2
 2673             kind_co = go s1 s2
 2674 
 2675             -- s1 = t1 ~r t2
 2676             -- s2 = t3 ~r t4
 2677             -- kind_co :: (t1 ~r t2) ~N (t3 ~r t4)
 2678             -- eta1 :: t1 ~r t3
 2679             -- eta2 :: t2 ~r t4
 2680 
 2681             r    = coVarRole cv1
 2682             kind_co' = downgradeRole r Nominal kind_co
 2683             eta1 = mkNthCo r 2 kind_co'
 2684             eta2 = mkNthCo r 3 kind_co'
 2685 
 2686             subst = mkEmptyTCvSubst $ mkInScopeSet $
 2687                       tyCoVarsOfType ty2 `unionVarSet` tyCoVarsOfCo kind_co
 2688             ty2'  = substTy (extendCvSubst subst cv2 $ mkSymCo eta1 `mkTransCo`
 2689                                                        mkCoVarCo cv1 `mkTransCo`
 2690                                                        eta2)
 2691                             ty2
 2692 
 2693     go ty1@(LitTy lit1) _lit2
 2694       = assert (case _lit2 of
 2695                   { LitTy lit2 -> lit1 == lit2
 2696                   ; _          -> False        }) $
 2697         mkNomReflCo ty1
 2698 
 2699     go (CoercionTy co1) (CoercionTy co2)
 2700       = mkProofIrrelCo Nominal kind_co co1 co2
 2701       where
 2702         kind_co = go (coercionType co1) (coercionType co2)
 2703 
 2704     go ty1 ty2
 2705       = pprPanic "buildKindCoercion" (vcat [ ppr orig_ty1, ppr orig_ty2
 2706                                            , ppr ty1, ppr ty2 ])
 2707 
 2708 
 2709 {-
 2710 %************************************************************************
 2711 %*                                                                      *
 2712        Coercion holes
 2713 %*                                                                      *
 2714 %************************************************************************
 2715 -}
 2716 
 2717 has_co_hole_ty :: Type -> Monoid.Any
 2718 has_co_hole_co :: Coercion -> Monoid.Any
 2719 (has_co_hole_ty, _, has_co_hole_co, _)
 2720   = foldTyCo folder ()
 2721   where
 2722     folder = TyCoFolder { tcf_view  = const Nothing
 2723                         , tcf_tyvar = const2 (Monoid.Any False)
 2724                         , tcf_covar = const2 (Monoid.Any False)
 2725                         , tcf_hole  = const2 (Monoid.Any True)
 2726                         , tcf_tycobinder = const2
 2727                         }
 2728 
 2729     const2 :: a -> b -> c -> a
 2730     const2 x _ _ = x
 2731 
 2732 -- | Is there a coercion hole in this type?
 2733 hasCoercionHoleTy :: Type -> Bool
 2734 hasCoercionHoleTy = Monoid.getAny . has_co_hole_ty
 2735 
 2736 -- | Is there a coercion hole in this coercion?
 2737 hasCoercionHoleCo :: Coercion -> Bool
 2738 hasCoercionHoleCo = Monoid.getAny . has_co_hole_co
 2739 
 2740 -- | A set of 'CoercionHole's
 2741 type HoleSet = UniqSet CoercionHole
 2742 
 2743 -- | Extract out all the coercion holes from a given type
 2744 coercionHolesOfType :: Type -> UniqSet CoercionHole
 2745 coercionHolesOfCo   :: Coercion -> UniqSet CoercionHole
 2746 (coercionHolesOfType, _, coercionHolesOfCo, _) = foldTyCo folder ()
 2747   where
 2748     folder = TyCoFolder { tcf_view  = const Nothing  -- don't look through synonyms
 2749                         , tcf_tyvar = \ _ _ -> mempty
 2750                         , tcf_covar = \ _ _ -> mempty
 2751                         , tcf_hole  = const unitUniqSet
 2752                         , tcf_tycobinder = \ _ _ _ -> ()
 2753                         }