{-# LANGUAGE BangPatterns  #-}

{-# LANGUAGE DeriveFunctor #-}

{-# OPTIONS_GHC -Wno-incomplete-record-updates #-}

module GHC.Tc.Solver.Rewrite(
   rewrite, rewriteArgsNom,
   rewriteType
 ) where

import GHC.Prelude

import GHC.Core.TyCo.Ppr ( pprTyVar )
import GHC.Tc.Types ( TcGblEnv(tcg_tc_plugin_rewriters),
                      TcPluginRewriter, TcPluginRewriteResult(..),
                      RewriteEnv(..),
                      runTcPluginM )
import GHC.Tc.Types.Constraint
import GHC.Core.Predicate
import GHC.Tc.Utils.TcType
import GHC.Core.Type
import GHC.Tc.Types.Evidence
import GHC.Core.TyCon
import GHC.Core.TyCo.Rep   -- performs delicate algorithm on types
import GHC.Core.Coercion
import GHC.Core.Reduction
import GHC.Types.Unique.FM
import GHC.Types.Var
import GHC.Types.Var.Set
import GHC.Types.Var.Env
import GHC.Driver.Session
import GHC.Utils.Outputable
import GHC.Utils.Panic
import GHC.Utils.Panic.Plain
import GHC.Tc.Solver.Monad as TcS

import GHC.Utils.Misc
import GHC.Data.Maybe
import GHC.Exts (oneShot)
import Control.Monad
import Control.Applicative (liftA3)
import GHC.Builtin.Types.Prim (tYPETyCon)
import Data.List ( find )

{-
************************************************************************
*                                                                      *
*                RewriteEnv & RewriteM
*             The rewriting environment & monad
*                                                                      *
************************************************************************
-}

-- | The 'RewriteM' monad is a wrapper around 'TcS' with a 'RewriteEnv'
newtype RewriteM a
  = RewriteM { RewriteM a -> RewriteEnv -> TcS a
runRewriteM :: RewriteEnv -> TcS a }
  deriving (a -> RewriteM b -> RewriteM a
(a -> b) -> RewriteM a -> RewriteM b
(forall a b. (a -> b) -> RewriteM a -> RewriteM b)
-> (forall a b. a -> RewriteM b -> RewriteM a) -> Functor RewriteM
forall a b. a -> RewriteM b -> RewriteM a
forall a b. (a -> b) -> RewriteM a -> RewriteM b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> RewriteM b -> RewriteM a
$c<$ :: forall a b. a -> RewriteM b -> RewriteM a
fmap :: (a -> b) -> RewriteM a -> RewriteM b
$cfmap :: forall a b. (a -> b) -> RewriteM a -> RewriteM b
Functor)

-- | Smart constructor for 'RewriteM', as describe in Note [The one-shot state
-- monad trick] in "GHC.Utils.Monad".
mkRewriteM :: (RewriteEnv -> TcS a) -> RewriteM a
mkRewriteM :: (RewriteEnv -> TcS a) -> RewriteM a
mkRewriteM RewriteEnv -> TcS a
f = (RewriteEnv -> TcS a) -> RewriteM a
forall a. (RewriteEnv -> TcS a) -> RewriteM a
RewriteM ((RewriteEnv -> TcS a) -> RewriteEnv -> TcS a
oneShot RewriteEnv -> TcS a
f)
{-# INLINE mkRewriteM #-}

instance Monad RewriteM where
  RewriteM a
m >>= :: RewriteM a -> (a -> RewriteM b) -> RewriteM b
>>= a -> RewriteM b
k  = (RewriteEnv -> TcS b) -> RewriteM b
forall a. (RewriteEnv -> TcS a) -> RewriteM a
mkRewriteM ((RewriteEnv -> TcS b) -> RewriteM b)
-> (RewriteEnv -> TcS b) -> RewriteM b
forall a b. (a -> b) -> a -> b
$ \RewriteEnv
env ->
             do { a
a  <- RewriteM a -> RewriteEnv -> TcS a
forall a. RewriteM a -> RewriteEnv -> TcS a
runRewriteM RewriteM a
m RewriteEnv
env
                ; RewriteM b -> RewriteEnv -> TcS b
forall a. RewriteM a -> RewriteEnv -> TcS a
runRewriteM (a -> RewriteM b
k a
a) RewriteEnv
env }

instance Applicative RewriteM where
  pure :: a -> RewriteM a
pure a
x = (RewriteEnv -> TcS a) -> RewriteM a
forall a. (RewriteEnv -> TcS a) -> RewriteM a
mkRewriteM ((RewriteEnv -> TcS a) -> RewriteM a)
-> (RewriteEnv -> TcS a) -> RewriteM a
forall a b. (a -> b) -> a -> b
$ \RewriteEnv
_ -> a -> TcS a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x
  <*> :: RewriteM (a -> b) -> RewriteM a -> RewriteM b
(<*>) = RewriteM (a -> b) -> RewriteM a -> RewriteM b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance HasDynFlags RewriteM where
  getDynFlags :: RewriteM DynFlags
getDynFlags = TcS DynFlags -> RewriteM DynFlags
forall a. TcS a -> RewriteM a
liftTcS TcS DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags

liftTcS :: TcS a -> RewriteM a
liftTcS :: TcS a -> RewriteM a
liftTcS TcS a
thing_inside
  = (RewriteEnv -> TcS a) -> RewriteM a
forall a. (RewriteEnv -> TcS a) -> RewriteM a
mkRewriteM ((RewriteEnv -> TcS a) -> RewriteM a)
-> (RewriteEnv -> TcS a) -> RewriteM a
forall a b. (a -> b) -> a -> b
$ \RewriteEnv
_ -> TcS a
thing_inside

-- convenient wrapper when you have a CtEvidence describing
-- the rewriting operation
runRewriteCtEv :: CtEvidence -> RewriteM a -> TcS (a, RewriterSet)
runRewriteCtEv :: CtEvidence -> RewriteM a -> TcS (a, RewriterSet)
runRewriteCtEv CtEvidence
ev
  = CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS (a, RewriterSet)
forall a.
CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS (a, RewriterSet)
runRewrite (CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev) (CtEvidence -> CtFlavour
ctEvFlavour CtEvidence
ev) (CtEvidence -> EqRel
ctEvEqRel CtEvidence
ev)

-- Run thing_inside (which does the rewriting)
-- Also returns the set of Wanteds which rewrote a Wanted;
-- See Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint
runRewrite :: CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS (a, RewriterSet)
runRewrite :: CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS (a, RewriterSet)
runRewrite CtLoc
loc CtFlavour
flav EqRel
eq_rel RewriteM a
thing_inside
  = do { TcRef RewriterSet
rewriters_ref <- RewriterSet -> TcS (TcRef RewriterSet)
forall a. a -> TcS (TcRef a)
newTcRef RewriterSet
emptyRewriterSet
       ; let fmode :: RewriteEnv
fmode = RE :: CtLoc -> CtFlavour -> EqRel -> TcRef RewriterSet -> RewriteEnv
RE { re_loc :: CtLoc
re_loc  = CtLoc
loc
                        , re_flavour :: CtFlavour
re_flavour = CtFlavour
flav
                        , re_eq_rel :: EqRel
re_eq_rel = EqRel
eq_rel
                        , re_rewriters :: TcRef RewriterSet
re_rewriters = TcRef RewriterSet
rewriters_ref }
       ; a
res <- RewriteM a -> RewriteEnv -> TcS a
forall a. RewriteM a -> RewriteEnv -> TcS a
runRewriteM RewriteM a
thing_inside RewriteEnv
fmode
       ; RewriterSet
rewriters <- TcRef RewriterSet -> TcS RewriterSet
forall a. TcRef a -> TcS a
readTcRef TcRef RewriterSet
rewriters_ref
       ; (a, RewriterSet) -> TcS (a, RewriterSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
res, RewriterSet
rewriters) }

traceRewriteM :: String -> SDoc -> RewriteM ()
traceRewriteM :: String -> SDoc -> RewriteM ()
traceRewriteM String
herald SDoc
doc = TcS () -> RewriteM ()
forall a. TcS a -> RewriteM a
liftTcS (TcS () -> RewriteM ()) -> TcS () -> RewriteM ()
forall a b. (a -> b) -> a -> b
$ String -> SDoc -> TcS ()
traceTcS String
herald SDoc
doc
{-# INLINE traceRewriteM #-}  -- see Note [INLINE conditional tracing utilities]

getRewriteEnv :: RewriteM RewriteEnv
getRewriteEnv :: RewriteM RewriteEnv
getRewriteEnv
  = (RewriteEnv -> TcS RewriteEnv) -> RewriteM RewriteEnv
forall a. (RewriteEnv -> TcS a) -> RewriteM a
mkRewriteM ((RewriteEnv -> TcS RewriteEnv) -> RewriteM RewriteEnv)
-> (RewriteEnv -> TcS RewriteEnv) -> RewriteM RewriteEnv
forall a b. (a -> b) -> a -> b
$ \RewriteEnv
env -> RewriteEnv -> TcS RewriteEnv
forall (m :: * -> *) a. Monad m => a -> m a
return RewriteEnv
env

getRewriteEnvField :: (RewriteEnv -> a) -> RewriteM a
getRewriteEnvField :: (RewriteEnv -> a) -> RewriteM a
getRewriteEnvField RewriteEnv -> a
accessor
  = (RewriteEnv -> TcS a) -> RewriteM a
forall a. (RewriteEnv -> TcS a) -> RewriteM a
mkRewriteM ((RewriteEnv -> TcS a) -> RewriteM a)
-> (RewriteEnv -> TcS a) -> RewriteM a
forall a b. (a -> b) -> a -> b
$ \RewriteEnv
env -> a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (RewriteEnv -> a
accessor RewriteEnv
env)

getEqRel :: RewriteM EqRel
getEqRel :: RewriteM EqRel
getEqRel = (RewriteEnv -> EqRel) -> RewriteM EqRel
forall a. (RewriteEnv -> a) -> RewriteM a
getRewriteEnvField RewriteEnv -> EqRel
re_eq_rel

getRole :: RewriteM Role
getRole :: RewriteM Role
getRole = EqRel -> Role
eqRelRole (EqRel -> Role) -> RewriteM EqRel -> RewriteM Role
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RewriteM EqRel
getEqRel

getFlavour :: RewriteM CtFlavour
getFlavour :: RewriteM CtFlavour
getFlavour = (RewriteEnv -> CtFlavour) -> RewriteM CtFlavour
forall a. (RewriteEnv -> a) -> RewriteM a
getRewriteEnvField RewriteEnv -> CtFlavour
re_flavour

getFlavourRole :: RewriteM CtFlavourRole
getFlavourRole :: RewriteM CtFlavourRole
getFlavourRole
  = do { CtFlavour
flavour <- RewriteM CtFlavour
getFlavour
       ; EqRel
eq_rel <- RewriteM EqRel
getEqRel
       ; CtFlavourRole -> RewriteM CtFlavourRole
forall (m :: * -> *) a. Monad m => a -> m a
return (CtFlavour
flavour, EqRel
eq_rel) }

getLoc :: RewriteM CtLoc
getLoc :: RewriteM CtLoc
getLoc = (RewriteEnv -> CtLoc) -> RewriteM CtLoc
forall a. (RewriteEnv -> a) -> RewriteM a
getRewriteEnvField RewriteEnv -> CtLoc
re_loc

checkStackDepth :: Type -> RewriteM ()
checkStackDepth :: Type -> RewriteM ()
checkStackDepth Type
ty
  = do { CtLoc
loc <- RewriteM CtLoc
getLoc
       ; TcS () -> RewriteM ()
forall a. TcS a -> RewriteM a
liftTcS (TcS () -> RewriteM ()) -> TcS () -> RewriteM ()
forall a b. (a -> b) -> a -> b
$ CtLoc -> Type -> TcS ()
checkReductionDepth CtLoc
loc Type
ty }

-- | Change the 'EqRel' in a 'RewriteM'.
setEqRel :: EqRel -> RewriteM a -> RewriteM a
setEqRel :: EqRel -> RewriteM a -> RewriteM a
setEqRel EqRel
new_eq_rel RewriteM a
thing_inside
  = (RewriteEnv -> TcS a) -> RewriteM a
forall a. (RewriteEnv -> TcS a) -> RewriteM a
mkRewriteM ((RewriteEnv -> TcS a) -> RewriteM a)
-> (RewriteEnv -> TcS a) -> RewriteM a
forall a b. (a -> b) -> a -> b
$ \RewriteEnv
env ->
    if EqRel
new_eq_rel EqRel -> EqRel -> Bool
forall a. Eq a => a -> a -> Bool
== RewriteEnv -> EqRel
re_eq_rel RewriteEnv
env
    then RewriteM a -> RewriteEnv -> TcS a
forall a. RewriteM a -> RewriteEnv -> TcS a
runRewriteM RewriteM a
thing_inside RewriteEnv
env
    else RewriteM a -> RewriteEnv -> TcS a
forall a. RewriteM a -> RewriteEnv -> TcS a
runRewriteM RewriteM a
thing_inside (RewriteEnv
env { re_eq_rel :: EqRel
re_eq_rel = EqRel
new_eq_rel })
{-# INLINE setEqRel #-}

bumpDepth :: RewriteM a -> RewriteM a
bumpDepth :: RewriteM a -> RewriteM a
bumpDepth (RewriteM RewriteEnv -> TcS a
thing_inside)
  = (RewriteEnv -> TcS a) -> RewriteM a
forall a. (RewriteEnv -> TcS a) -> RewriteM a
mkRewriteM ((RewriteEnv -> TcS a) -> RewriteM a)
-> (RewriteEnv -> TcS a) -> RewriteM a
forall a b. (a -> b) -> a -> b
$ \RewriteEnv
env -> do
      -- bumpDepth can be called a lot during rewriting so we force the
      -- new env to avoid accumulating thunks.
      { let !env' :: RewriteEnv
env' = RewriteEnv
env { re_loc :: CtLoc
re_loc = CtLoc -> CtLoc
bumpCtLocDepth (RewriteEnv -> CtLoc
re_loc RewriteEnv
env) }
      ; RewriteEnv -> TcS a
thing_inside RewriteEnv
env' }

-- See Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint
-- Precondition: the CtEvidence is a CtWanted of an equality
recordRewriter :: CtEvidence -> RewriteM ()
recordRewriter :: CtEvidence -> RewriteM ()
recordRewriter (CtWanted { ctev_dest :: CtEvidence -> TcEvDest
ctev_dest = HoleDest CoercionHole
hole })
  = (RewriteEnv -> TcS ()) -> RewriteM ()
forall a. (RewriteEnv -> TcS a) -> RewriteM a
RewriteM ((RewriteEnv -> TcS ()) -> RewriteM ())
-> (RewriteEnv -> TcS ()) -> RewriteM ()
forall a b. (a -> b) -> a -> b
$ \RewriteEnv
env -> TcRef RewriterSet -> (RewriterSet -> RewriterSet) -> TcS ()
forall a. TcRef a -> (a -> a) -> TcS ()
updTcRef (RewriteEnv -> TcRef RewriterSet
re_rewriters RewriteEnv
env) (RewriterSet -> CoercionHole -> RewriterSet
`addRewriterSet` CoercionHole
hole)
recordRewriter CtEvidence
other = String -> SDoc -> RewriteM ()
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"recordRewriter" (CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
other)

{-
Note [Rewriter EqRels]
~~~~~~~~~~~~~~~~~~~~~~~
When rewriting, we need to know which equality relation -- nominal
or representation -- we should be respecting. The only difference is
that we rewrite variables by representational equalities when re_eq_rel
is ReprEq, and that we unwrap newtypes when rewriting w.r.t.
representational equality.

Note [Rewriter CtLoc]
~~~~~~~~~~~~~~~~~~~~~~
The rewriter does eager type-family reduction.
Type families might loop, and we
don't want GHC to do so. A natural solution is to have a bounded depth
to these processes. A central difficulty is that such a solution isn't
quite compositional. For example, say it takes F Int 10 steps to get to Bool.
How many steps does it take to get from F Int -> F Int to Bool -> Bool?
10? 20? What about getting from Const Char (F Int) to Char? 11? 1? Hard to
know and hard to track. So, we punt, essentially. We store a CtLoc in
the RewriteEnv and just update the environment when recurring. In the
TyConApp case, where there may be multiple type families to rewrite,
we just copy the current CtLoc into each branch. If any branch hits the
stack limit, then the whole thing fails.

A consequence of this is that setting the stack limits appropriately
will be essentially impossible. So, the official recommendation if a
stack limit is hit is to disable the check entirely. Otherwise, there
will be baffling, unpredictable errors.

Note [Phantoms in the rewriter]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have

data Proxy p = Proxy

and we're rewriting (Proxy ty) w.r.t. ReprEq. Then, we know that `ty`
is really irrelevant -- it will be ignored when solving for representational
equality later on. So, we omit rewriting `ty` entirely. This may
violate the expectation of "xi"s for a bit, but the canonicaliser will
soon throw out the phantoms when decomposing a TyConApp. (Or, the
canonicaliser will emit an insoluble, in which case we get
a better error message anyway.)

-}

{- *********************************************************************
*                                                                      *
*      Externally callable rewriting functions                         *
*                                                                      *
************************************************************************
-}

-- | See Note [Rewriting].
-- If (xi, co, rewriters) <- rewrite mode ev ty, then co :: xi ~r ty
-- where r is the role in @ev@.
-- rewriters is the set of coercion holes that have been used to rewrite
-- See Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint
rewrite :: CtEvidence -> TcType
        -> TcS (Reduction, RewriterSet)
rewrite :: CtEvidence -> Type -> TcS (Reduction, RewriterSet)
rewrite CtEvidence
ev Type
ty
  = do { String -> SDoc -> TcS ()
traceTcS String
"rewrite {" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)
       ; result :: (Reduction, RewriterSet)
result@(Reduction
redn, RewriterSet
_) <- CtEvidence -> RewriteM Reduction -> TcS (Reduction, RewriterSet)
forall a. CtEvidence -> RewriteM a -> TcS (a, RewriterSet)
runRewriteCtEv CtEvidence
ev (Type -> RewriteM Reduction
rewrite_one Type
ty)
       ; String -> SDoc -> TcS ()
traceTcS String
"rewrite }" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Type -> SDoc) -> Type -> SDoc
forall a b. (a -> b) -> a -> b
$ Reduction -> Type
reductionReducedType Reduction
redn)
       ; (Reduction, RewriterSet) -> TcS (Reduction, RewriterSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction, RewriterSet)
result }

-- See Note [Rewriting]
rewriteArgsNom :: CtEvidence -> TyCon -> [TcType]
               -> TcS (Reductions, RewriterSet)
-- Externally-callable, hence runRewrite
-- Rewrite a vector of types all at once; in fact they are
-- always the arguments of type family or class, so
--      ctEvFlavour ev = Nominal
-- and we want to rewrite all at nominal role
-- The kind passed in is the kind of the type family or class, call it T
-- The kind of T args must be constant (i.e. not depend on the args)
--
-- Final return value returned which Wanteds rewrote another Wanted
-- See Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint
rewriteArgsNom :: CtEvidence -> TyCon -> [Type] -> TcS (Reductions, RewriterSet)
rewriteArgsNom CtEvidence
ev TyCon
tc [Type]
tys
  = do { String -> SDoc -> TcS ()
traceTcS String
"rewrite_args {" ([SDoc] -> SDoc
vcat ((Type -> SDoc) -> [Type] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys))
       ; (ArgsReductions redns :: Reductions
redns@(Reductions [Coercion]
_ [Type]
tys') MCoercionN
kind_co, RewriterSet
rewriters)
           <- CtEvidence
-> RewriteM ArgsReductions -> TcS (ArgsReductions, RewriterSet)
forall a. CtEvidence -> RewriteM a -> TcS (a, RewriterSet)
runRewriteCtEv CtEvidence
ev (TyCon -> Maybe [Role] -> [Type] -> RewriteM ArgsReductions
rewrite_args_tc TyCon
tc Maybe [Role]
forall a. Maybe a
Nothing [Type]
tys)
       ; Bool -> TcS ()
forall (m :: * -> *). (HasCallStack, Applicative m) => Bool -> m ()
massert (MCoercionN -> Bool
isReflMCo MCoercionN
kind_co)
       ; String -> SDoc -> TcS ()
traceTcS String
"rewrite }" ([SDoc] -> SDoc
vcat ((Type -> SDoc) -> [Type] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys'))
       ; (Reductions, RewriterSet) -> TcS (Reductions, RewriterSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Reductions
redns, RewriterSet
rewriters) }

-- | Rewrite a type w.r.t. nominal equality. This is useful to rewrite
-- a type w.r.t. any givens. It does not do type-family reduction. This
-- will never emit new constraints. Call this when the inert set contains
-- only givens.
rewriteType :: CtLoc -> TcType -> TcS TcType
rewriteType :: CtLoc -> Type -> TcS Type
rewriteType CtLoc
loc Type
ty
  = do { (Reduction
redn, RewriterSet
_) <- CtLoc
-> CtFlavour
-> EqRel
-> RewriteM Reduction
-> TcS (Reduction, RewriterSet)
forall a.
CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS (a, RewriterSet)
runRewrite CtLoc
loc CtFlavour
Given EqRel
NomEq (RewriteM Reduction -> TcS (Reduction, RewriterSet))
-> RewriteM Reduction -> TcS (Reduction, RewriterSet)
forall a b. (a -> b) -> a -> b
$
                       Type -> RewriteM Reduction
rewrite_one Type
ty
                     -- use Given flavor so that it is rewritten
                     -- only w.r.t. Givens, never Wanteds
                     -- (Shouldn't matter, if only Givens are present
                     -- anyway)
       ; Type -> TcS Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TcS Type) -> Type -> TcS Type
forall a b. (a -> b) -> a -> b
$ Reduction -> Type
reductionReducedType Reduction
redn }

{- *********************************************************************
*                                                                      *
*           The main rewriting functions
*                                                                      *
********************************************************************* -}

{- Note [Rewriting]
~~~~~~~~~~~~~~~~~~~~
  rewrite ty  ==>  Reduction co xi
    where
      xi has no reducible type functions
         has no skolems that are mapped in the inert set
         has no filled-in metavariables
      co :: ty ~ xi (coercions in reductions are always left-to-right)

Key invariants:
  (F0) co :: zonk(ty') ~ xi   where zonk(ty') ~ zonk(ty)
  (F1) tcTypeKind(xi) succeeds and returns a fully zonked kind
  (F2) tcTypeKind(xi) `eqType` zonk(tcTypeKind(ty))

Note that it is rewrite's job to try to reduce *every type function it sees*.

Rewriting also:
  * zonks, removing any metavariables, and
  * applies the substitution embodied in the inert set

Because rewriting zonks and the returned coercion ("co" above) is also
zonked, it's possible that (co :: ty ~ xi) isn't quite true. So, instead,
we can rely on this fact:

  (F0) co :: zonk(ty') ~ xi, where zonk(ty') ~ zonk(ty)

Note that the right-hand type of co is *always* precisely xi. The left-hand
type may or may not be ty, however: if ty has unzonked filled-in metavariables,
then the left-hand type of co will be the zonk-equal to ty.
It is for this reason that we occasionally have to explicitly zonk,
when (co :: ty ~ xi) is important even before we zonk the whole program.
For example, see the RTRNotFollowed case in rewriteTyVar.

Why have these invariants on rewriting? Because we sometimes use tcTypeKind
during canonicalisation, and we want this kind to be zonked (e.g., see
GHC.Tc.Solver.Canonical.canEqCanLHS).

Rewriting is always homogeneous. That is, the kind of the result of rewriting is
always the same as the kind of the input, modulo zonking. More formally:

  (F2) zonk(tcTypeKind(ty)) `eqType` tcTypeKind(xi)

This invariant means that the kind of a rewritten type might not itself be rewritten.

Note that we prefer to leave type synonyms unexpanded when possible,
so when the rewriter encounters one, it first asks whether its
transitive expansion contains any type function applications or is
forgetful -- that is, omits one or more type variables in its RHS.  If so,
it expands the synonym and proceeds; if not, it simply returns the
unexpanded synonym. See also Note [Rewriting synonyms].

Where do we actually perform rewriting within a type? See Note [Rewritable] in
GHC.Tc.Solver.InertSet.

Note [rewrite_args performance]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In programs with lots of type-level evaluation, rewrite_args becomes
part of a tight loop. For example, see test perf/compiler/T9872a, which
calls rewrite_args a whopping 7,106,808 times. It is thus important
that rewrite_args be efficient.

Performance testing showed that the current implementation is indeed
efficient. It's critically important that zipWithAndUnzipM be
specialized to TcS, and it's also quite helpful to actually `inline`
it. On test T9872a, here are the allocation stats (Dec 16, 2014):

 * Unspecialized, uninlined:     8,472,613,440 bytes allocated in the heap
 * Specialized, uninlined:       6,639,253,488 bytes allocated in the heap
 * Specialized, inlined:         6,281,539,792 bytes allocated in the heap

To improve performance even further, rewrite_args_nom is split off
from rewrite_args, as nominal equality is the common case. This would
be natural to write using mapAndUnzipM, but even inlined, that function
is not as performant as a hand-written loop.

 * mapAndUnzipM, inlined:        7,463,047,432 bytes allocated in the heap
 * hand-written recursion:       5,848,602,848 bytes allocated in the heap

If you make any change here, pay close attention to the T9872{a,b,c} tests
and T5321Fun.

If we need to make this yet more performant, a possible way forward is to
duplicate the rewriter code for the nominal case, and make that case
faster. This doesn't seem quite worth it, yet.

Note [rewrite_exact_fam_app performance]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Once we've got a rewritten rhs, we extend the famapp-cache to record
the result. Doing so can save lots of work when the same redex shows up more
than once. Note that we record the link from the redex all the way to its
*final* value, not just the single step reduction.

If we can reduce the family application right away (the first call
to try_to_reduce), we do *not* add to the cache. There are two possibilities
here: 1) we just read the result from the cache, or 2) we used one type
family instance. In either case, recording the result in the cache doesn't
save much effort the next time around. And adding to the cache here is
actually disastrous: it more than doubles the allocations for T9872a. So
we skip adding to the cache here.
-}

{-# INLINE rewrite_args_tc #-}
rewrite_args_tc
  :: TyCon         -- T
  -> Maybe [Role]  -- Nothing: ambient role is Nominal; all args are Nominal
                   -- Otherwise: no assumptions; use roles provided
  -> [Type]
  -> RewriteM ArgsReductions -- See the commentary on rewrite_args
rewrite_args_tc :: TyCon -> Maybe [Role] -> [Type] -> RewriteM ArgsReductions
rewrite_args_tc TyCon
tc = [TyCoBinder]
-> Bool
-> Type
-> TcTyCoVarSet
-> Maybe [Role]
-> [Type]
-> RewriteM ArgsReductions
rewrite_args [TyCoBinder]
all_bndrs Bool
any_named_bndrs Type
inner_ki TcTyCoVarSet
emptyVarSet
  -- NB: TyCon kinds are always closed
  where
  -- There are many bang patterns in here. It's been observed that they
  -- greatly improve performance of an optimized build.
  -- The T9872 test cases are good witnesses of this fact.

    ([TyCoBinder]
bndrs, Bool
named)
      = [TyConBinder] -> ([TyCoBinder], Bool)
ty_con_binders_ty_binders' (TyCon -> [TyConBinder]
tyConBinders TyCon
tc)
    -- it's possible that the result kind has arrows (for, e.g., a type family)
    -- so we must split it
    ([TyCoBinder]
inner_bndrs, Type
inner_ki, Bool
inner_named) = Type -> ([TyCoBinder], Type, Bool)
split_pi_tys' (TyCon -> Type
tyConResKind TyCon
tc)
    !all_bndrs :: [TyCoBinder]
all_bndrs                           = [TyCoBinder]
bndrs [TyCoBinder] -> [TyCoBinder] -> [TyCoBinder]
forall a. [a] -> [a] -> [a]
`chkAppend` [TyCoBinder]
inner_bndrs
    !any_named_bndrs :: Bool
any_named_bndrs                     = Bool
named Bool -> Bool -> Bool
|| Bool
inner_named
    -- NB: Those bangs there drop allocations in T9872{a,c,d} by 8%.

{-# INLINE rewrite_args #-}
rewrite_args :: [TyCoBinder] -> Bool -- Binders, and True iff any of them are
                                     -- named.
             -> Kind -> TcTyCoVarSet -- function kind; kind's free vars
             -> Maybe [Role] -> [Type]    -- these are in 1-to-1 correspondence
                                          -- Nothing: use all Nominal
             -> RewriteM ArgsReductions
-- This function returns ArgsReductions (Reductions cos xis) res_co
--   coercions: co_i :: ty_i ~ xi_i, at roles given
--   types:     xi_i
--   coercion:  res_co :: tcTypeKind(fun tys) ~N tcTypeKind(fun xis)
-- That is, the result coercion relates the kind of some function (whose kind is
-- passed as the first parameter) instantiated at tys to the kind of that
-- function instantiated at the xis. This is useful in keeping rewriting
-- homogeneous. The list of roles must be at least as long as the list of
-- types.
rewrite_args :: [TyCoBinder]
-> Bool
-> Type
-> TcTyCoVarSet
-> Maybe [Role]
-> [Type]
-> RewriteM ArgsReductions
rewrite_args [TyCoBinder]
orig_binders
             Bool
any_named_bndrs
             Type
orig_inner_ki
             TcTyCoVarSet
orig_fvs
             Maybe [Role]
orig_m_roles
             [Type]
orig_tys
  = case (Maybe [Role]
orig_m_roles, Bool
any_named_bndrs) of
      (Maybe [Role]
Nothing, Bool
False) -> [Type] -> RewriteM ArgsReductions
rewrite_args_fast [Type]
orig_tys
      (Maybe [Role], Bool)
_ -> [TyCoBinder]
-> Type
-> TcTyCoVarSet
-> [Role]
-> [Type]
-> RewriteM ArgsReductions
rewrite_args_slow [TyCoBinder]
orig_binders Type
orig_inner_ki TcTyCoVarSet
orig_fvs [Role]
orig_roles [Type]
orig_tys
        where orig_roles :: [Role]
orig_roles = [Role] -> Maybe [Role] -> [Role]
forall a. a -> Maybe a -> a
fromMaybe (Role -> [Role]
forall a. a -> [a]
repeat Role
Nominal) Maybe [Role]
orig_m_roles

{-# INLINE rewrite_args_fast #-}
-- | fast path rewrite_args, in which none of the binders are named and
-- therefore we can avoid tracking a lifting context.
rewrite_args_fast :: [Type] -> RewriteM ArgsReductions
rewrite_args_fast :: [Type] -> RewriteM ArgsReductions
rewrite_args_fast [Type]
orig_tys
  = (Reductions -> ArgsReductions)
-> RewriteM Reductions -> RewriteM ArgsReductions
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Reductions -> ArgsReductions
finish ([Type] -> RewriteM Reductions
iterate [Type]
orig_tys)
  where

    iterate :: [Type] -> RewriteM Reductions
    iterate :: [Type] -> RewriteM Reductions
iterate (Type
ty : [Type]
tys) = do
      Reduction  Coercion
co  Type
xi  <- Type -> RewriteM Reduction
rewrite_one Type
ty
      Reductions [Coercion]
cos [Type]
xis <- [Type] -> RewriteM Reductions
iterate [Type]
tys
      Reductions -> RewriteM Reductions
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Reductions -> RewriteM Reductions)
-> Reductions -> RewriteM Reductions
forall a b. (a -> b) -> a -> b
$ [Coercion] -> [Type] -> Reductions
Reductions (Coercion
co Coercion -> [Coercion] -> [Coercion]
forall a. a -> [a] -> [a]
: [Coercion]
cos) (Type
xi Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type]
xis)
    iterate [] = Reductions -> RewriteM Reductions
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Reductions -> RewriteM Reductions)
-> Reductions -> RewriteM Reductions
forall a b. (a -> b) -> a -> b
$ [Coercion] -> [Type] -> Reductions
Reductions [] []

    {-# INLINE finish #-}
    finish :: Reductions -> ArgsReductions
    finish :: Reductions -> ArgsReductions
finish Reductions
redns = Reductions -> MCoercionN -> ArgsReductions
ArgsReductions Reductions
redns MCoercionN
MRefl

{-# INLINE rewrite_args_slow #-}
-- | Slow path, compared to rewrite_args_fast, because this one must track
-- a lifting context.
rewrite_args_slow :: [TyCoBinder] -> Kind -> TcTyCoVarSet
                  -> [Role] -> [Type]
                  -> RewriteM ArgsReductions
rewrite_args_slow :: [TyCoBinder]
-> Type
-> TcTyCoVarSet
-> [Role]
-> [Type]
-> RewriteM ArgsReductions
rewrite_args_slow [TyCoBinder]
binders Type
inner_ki TcTyCoVarSet
fvs [Role]
roles [Type]
tys
  = do { [Reduction]
rewritten_args <- (Role -> Type -> RewriteM Reduction)
-> [Role] -> [Type] -> RewriteM [Reduction]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Role -> Type -> RewriteM Reduction
rw [Role]
roles [Type]
tys
       ; ArgsReductions -> RewriteM ArgsReductions
forall (m :: * -> *) a. Monad m => a -> m a
return ([TyCoBinder]
-> Type -> TcTyCoVarSet -> [Role] -> [Reduction] -> ArgsReductions
HasDebugCallStack =>
[TyCoBinder]
-> Type -> TcTyCoVarSet -> [Role] -> [Reduction] -> ArgsReductions
simplifyArgsWorker [TyCoBinder]
binders Type
inner_ki TcTyCoVarSet
fvs [Role]
roles [Reduction]
rewritten_args) }
  where
    {-# INLINE rw #-}
    rw :: Role -> Type -> RewriteM Reduction
    rw :: Role -> Type -> RewriteM Reduction
rw Role
Nominal Type
ty
      = EqRel -> RewriteM Reduction -> RewriteM Reduction
forall a. EqRel -> RewriteM a -> RewriteM a
setEqRel EqRel
NomEq (RewriteM Reduction -> RewriteM Reduction)
-> RewriteM Reduction -> RewriteM Reduction
forall a b. (a -> b) -> a -> b
$
        Type -> RewriteM Reduction
rewrite_one Type
ty

    rw Role
Representational Type
ty
      = EqRel -> RewriteM Reduction -> RewriteM Reduction
forall a. EqRel -> RewriteM a -> RewriteM a
setEqRel EqRel
ReprEq (RewriteM Reduction -> RewriteM Reduction)
-> RewriteM Reduction -> RewriteM Reduction
forall a b. (a -> b) -> a -> b
$
        Type -> RewriteM Reduction
rewrite_one Type
ty

    rw Role
Phantom Type
ty
    -- See Note [Phantoms in the rewriter]
      = do { Type
ty <- TcS Type -> RewriteM Type
forall a. TcS a -> RewriteM a
liftTcS (TcS Type -> RewriteM Type) -> TcS Type -> RewriteM Type
forall a b. (a -> b) -> a -> b
$ Type -> TcS Type
zonkTcType Type
ty
           ; Reduction -> RewriteM Reduction
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> RewriteM Reduction)
-> Reduction -> RewriteM Reduction
forall a b. (a -> b) -> a -> b
$ Role -> Type -> Reduction
mkReflRedn Role
Phantom Type
ty }

------------------
rewrite_one :: TcType -> RewriteM Reduction
-- Rewrite a type to get rid of type function applications, returning
-- the new type-function-free type, and a collection of new equality
-- constraints.  See Note [Rewriting] for more detail.
--
-- Postcondition:
-- the role on the result coercion matches the EqRel in the RewriteEnv

rewrite_one :: Type -> RewriteM Reduction
rewrite_one Type
ty
  | Just Type
ty' <- Type -> Maybe Type
rewriterView Type
ty  -- See Note [Rewriting synonyms]
  = Type -> RewriteM Reduction
rewrite_one Type
ty'

rewrite_one xi :: Type
xi@(LitTy {})
  = do { Role
role <- RewriteM Role
getRole
       ; Reduction -> RewriteM Reduction
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> RewriteM Reduction)
-> Reduction -> RewriteM Reduction
forall a b. (a -> b) -> a -> b
$ Role -> Type -> Reduction
mkReflRedn Role
role Type
xi }

rewrite_one (TyVarTy Var
tv)
  = Var -> RewriteM Reduction
rewriteTyVar Var
tv

rewrite_one (AppTy Type
ty1 Type
ty2)
  = Type -> [Type] -> RewriteM Reduction
rewrite_app_tys Type
ty1 [Type
ty2]

rewrite_one (TyConApp TyCon
tc [Type]
tys)
  -- If it's a type family application, try to reduce it
  | TyCon -> Bool
isTypeFamilyTyCon TyCon
tc
  = TyCon -> [Type] -> RewriteM Reduction
rewrite_fam_app TyCon
tc [Type]
tys

  -- For * a normal data type application
  --     * data family application
  -- we just recursively rewrite the arguments.
  | Bool
otherwise
  = TyCon -> [Type] -> RewriteM Reduction
rewrite_ty_con_app TyCon
tc [Type]
tys

rewrite_one (FunTy { ft_af :: Type -> AnonArgFlag
ft_af = AnonArgFlag
vis, ft_mult :: Type -> Type
ft_mult = Type
mult, ft_arg :: Type -> Type
ft_arg = Type
ty1, ft_res :: Type -> Type
ft_res = Type
ty2 })
  = do { Reduction
arg_redn <- Type -> RewriteM Reduction
rewrite_one Type
ty1
       ; Reduction
res_redn <- Type -> RewriteM Reduction
rewrite_one Type
ty2

        -- Important: look at the *reduced* type, so that any unzonked variables
        -- in kinds are gone and the getRuntimeRep succeeds.
        -- cf. Note [Decomposing FunTy] in GHC.Tc.Solver.Canonical.
       ; let arg_rep :: Type
arg_rep = HasDebugCallStack => Type -> Type
Type -> Type
getRuntimeRep (Reduction -> Type
reductionReducedType Reduction
arg_redn)
             res_rep :: Type
res_rep = HasDebugCallStack => Type -> Type
Type -> Type
getRuntimeRep (Reduction -> Type
reductionReducedType Reduction
res_redn)

       ; (Reduction
w_redn, Reduction
arg_rep_redn, Reduction
res_rep_redn) <- EqRel
-> RewriteM (Reduction, Reduction, Reduction)
-> RewriteM (Reduction, Reduction, Reduction)
forall a. EqRel -> RewriteM a -> RewriteM a
setEqRel EqRel
NomEq (RewriteM (Reduction, Reduction, Reduction)
 -> RewriteM (Reduction, Reduction, Reduction))
-> RewriteM (Reduction, Reduction, Reduction)
-> RewriteM (Reduction, Reduction, Reduction)
forall a b. (a -> b) -> a -> b
$
           (Reduction
 -> Reduction -> Reduction -> (Reduction, Reduction, Reduction))
-> RewriteM Reduction
-> RewriteM Reduction
-> RewriteM Reduction
-> RewriteM (Reduction, Reduction, Reduction)
forall (f :: * -> *) a b c d.
Applicative f =>
(a -> b -> c -> d) -> f a -> f b -> f c -> f d
liftA3 (,,) (Type -> RewriteM Reduction
rewrite_one Type
mult)
                       (Type -> RewriteM Reduction
rewrite_one Type
arg_rep)
                       (Type -> RewriteM Reduction
rewrite_one Type
res_rep)
       ; Role
role <- RewriteM Role
getRole

       ; let arg_rep_co :: Coercion
arg_rep_co = Reduction -> Coercion
reductionCoercion Reduction
arg_rep_redn
                -- :: arg_rep ~ arg_rep_xi
             arg_ki_co :: Coercion
arg_ki_co  = HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
Nominal TyCon
tYPETyCon [Coercion
arg_rep_co]
                -- :: TYPE arg_rep ~ TYPE arg_rep_xi
             casted_arg_redn :: Reduction
casted_arg_redn = Role -> Reduction -> Coercion -> Reduction
mkCoherenceRightRedn Role
role Reduction
arg_redn Coercion
arg_ki_co
                -- :: ty1 ~> arg_xi |> arg_ki_co

             res_rep_co :: Coercion
res_rep_co = Reduction -> Coercion
reductionCoercion Reduction
res_rep_redn
             res_ki_co :: Coercion
res_ki_co  = HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
Nominal TyCon
tYPETyCon [Coercion
res_rep_co]
             casted_res_redn :: Reduction
casted_res_redn = Role -> Reduction -> Coercion -> Reduction
mkCoherenceRightRedn Role
role Reduction
res_redn Coercion
res_ki_co

          -- We must rewrite the representations, because that's what would
          -- be done if we used TyConApp instead of FunTy. These rewritten
          -- representations are seen only in casts of the arg and res, below.
          -- Forgetting this caused #19677.
       ; Reduction -> RewriteM Reduction
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> RewriteM Reduction)
-> Reduction -> RewriteM Reduction
forall a b. (a -> b) -> a -> b
$ Role
-> AnonArgFlag -> Reduction -> Reduction -> Reduction -> Reduction
mkFunRedn Role
role AnonArgFlag
vis Reduction
w_redn Reduction
casted_arg_redn Reduction
casted_res_redn }

rewrite_one ty :: Type
ty@(ForAllTy {})
-- TODO (RAE): This is inadequate, as it doesn't rewrite the kind of
-- the bound tyvar. Doing so will require carrying around a substitution
-- and the usual substTyVarBndr-like silliness. Argh.

-- We allow for-alls when, but only when, no type function
-- applications inside the forall involve the bound type variables.
  = do { let ([TyVarBinder]
bndrs, Type
rho) = Type -> ([TyVarBinder], Type)
tcSplitForAllTyVarBinders Type
ty
       ; Reduction
redn <- Type -> RewriteM Reduction
rewrite_one Type
rho
       ; Reduction -> RewriteM Reduction
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> RewriteM Reduction)
-> Reduction -> RewriteM Reduction
forall a b. (a -> b) -> a -> b
$ [TyVarBinder] -> Reduction -> Reduction
mkHomoForAllRedn [TyVarBinder]
bndrs Reduction
redn }

rewrite_one (CastTy Type
ty Coercion
g)
  = do { Reduction
redn <- Type -> RewriteM Reduction
rewrite_one Type
ty
       ; Coercion
g'   <- Coercion -> RewriteM Coercion
rewrite_co Coercion
g
       ; Role
role <- RewriteM Role
getRole
       ; Reduction -> RewriteM Reduction
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> RewriteM Reduction)
-> Reduction -> RewriteM Reduction
forall a b. (a -> b) -> a -> b
$ Role -> Type -> Coercion -> Reduction -> Reduction
mkCastRedn1 Role
role Type
ty Coercion
g' Reduction
redn }
      -- This calls castCoercionKind1.
      -- It makes a /big/ difference to call castCoercionKind1 not
      -- the more general castCoercionKind2.
      -- See Note [castCoercionKind1] in GHC.Core.Coercion

rewrite_one (CoercionTy Coercion
co)
  = do { Coercion
co' <- Coercion -> RewriteM Coercion
rewrite_co Coercion
co
       ; Role
role <- RewriteM Role
getRole
       ; Reduction -> RewriteM Reduction
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> RewriteM Reduction)
-> Reduction -> RewriteM Reduction
forall a b. (a -> b) -> a -> b
$ Role -> Coercion -> Reduction
mkReflCoRedn Role
role Coercion
co' }

-- | "Rewrite" a coercion. Really, just zonk it so we can uphold
-- (F1) of Note [Rewriting]
rewrite_co :: Coercion -> RewriteM Coercion
rewrite_co :: Coercion -> RewriteM Coercion
rewrite_co Coercion
co = TcS Coercion -> RewriteM Coercion
forall a. TcS a -> RewriteM a
liftTcS (TcS Coercion -> RewriteM Coercion)
-> TcS Coercion -> RewriteM Coercion
forall a b. (a -> b) -> a -> b
$ Coercion -> TcS Coercion
zonkCo Coercion
co

-- | Rewrite a reduction, composing the resulting coercions.
rewrite_reduction :: Reduction -> RewriteM Reduction
rewrite_reduction :: Reduction -> RewriteM Reduction
rewrite_reduction (Reduction Coercion
co Type
xi)
  = do { Reduction
redn <- RewriteM Reduction -> RewriteM Reduction
forall a. RewriteM a -> RewriteM a
bumpDepth (RewriteM Reduction -> RewriteM Reduction)
-> RewriteM Reduction -> RewriteM Reduction
forall a b. (a -> b) -> a -> b
$ Type -> RewriteM Reduction
rewrite_one Type
xi
       ; Reduction -> RewriteM Reduction
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> RewriteM Reduction)
-> Reduction -> RewriteM Reduction
forall a b. (a -> b) -> a -> b
$ Coercion
co Coercion -> Reduction -> Reduction
`mkTransRedn` Reduction
redn }

-- rewrite (nested) AppTys
rewrite_app_tys :: Type -> [Type] -> RewriteM Reduction
-- commoning up nested applications allows us to look up the function's kind
-- only once. Without commoning up like this, we would spend a quadratic amount
-- of time looking up functions' types
rewrite_app_tys :: Type -> [Type] -> RewriteM Reduction
rewrite_app_tys (AppTy Type
ty1 Type
ty2) [Type]
tys = Type -> [Type] -> RewriteM Reduction
rewrite_app_tys Type
ty1 (Type
ty2Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
tys)
rewrite_app_tys Type
fun_ty [Type]
arg_tys
  = do { Reduction
redn <- Type -> RewriteM Reduction
rewrite_one Type
fun_ty
       ; Reduction -> [Type] -> RewriteM Reduction
rewrite_app_ty_args Reduction
redn [Type]
arg_tys }

-- Given a rewritten function (with the coercion produced by rewriting) and
-- a bunch of unrewritten arguments, rewrite the arguments and apply.
-- The coercion argument's role matches the role stored in the RewriteM monad.
--
-- The bang patterns used here were observed to improve performance. If you
-- wish to remove them, be sure to check for regressions in allocations.
rewrite_app_ty_args :: Reduction -> [Type] -> RewriteM Reduction
rewrite_app_ty_args :: Reduction -> [Type] -> RewriteM Reduction
rewrite_app_ty_args Reduction
redn []
  -- this will be a common case when called from rewrite_fam_app, so shortcut
  = Reduction -> RewriteM Reduction
forall (m :: * -> *) a. Monad m => a -> m a
return Reduction
redn
rewrite_app_ty_args fun_redn :: Reduction
fun_redn@(Reduction Coercion
fun_co Type
fun_xi) [Type]
arg_tys
  = do { HetReduction
het_redn <- case HasCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
tcSplitTyConApp_maybe Type
fun_xi of
           Just (TyCon
tc, [Type]
xis) ->
             do { let tc_roles :: [Role]
tc_roles  = TyCon -> [Role]
tyConRolesRepresentational TyCon
tc
                      arg_roles :: [Role]
arg_roles = [Type] -> [Role] -> [Role]
forall b a. [b] -> [a] -> [a]
dropList [Type]
xis [Role]
tc_roles
                ; ArgsReductions (Reductions [Coercion]
arg_cos [Type]
arg_xis) MCoercionN
kind_co
                    <- Type -> [Role] -> [Type] -> RewriteM ArgsReductions
rewrite_vector (HasDebugCallStack => Type -> Type
Type -> Type
tcTypeKind Type
fun_xi) [Role]
arg_roles [Type]
arg_tys

                  -- We start with a reduction of the form
                  --   fun_co :: ty ~ T xi_1 ... xi_n
                  -- and further arguments a_1, ..., a_m.
                  -- We rewrite these arguments, and obtain coercions:
                  --   arg_co_i :: a_i ~ zeta_i
                  -- Now, we need to apply fun_co to the arg_cos. The problem is
                  -- that using mkAppCo is wrong because that function expects
                  -- its second coercion to be Nominal, and the arg_cos might
                  -- not be. The solution is to use transitivity:
                  -- fun_co <a_1> ... <a_m> ;; T <xi_1> .. <xi_n> arg_co_1 ... arg_co_m
                ; EqRel
eq_rel <- RewriteM EqRel
getEqRel
                ; let app_xi :: Type
app_xi = TyCon -> [Type] -> Type
mkTyConApp TyCon
tc ([Type]
xis [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
arg_xis)
                      app_co :: Coercion
app_co = case EqRel
eq_rel of
                        EqRel
NomEq  -> Coercion -> [Coercion] -> Coercion
mkAppCos Coercion
fun_co [Coercion]
arg_cos
                        EqRel
ReprEq -> Coercion -> [Coercion] -> Coercion
mkAppCos Coercion
fun_co ((Type -> Coercion) -> [Type] -> [Coercion]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Coercion
mkNomReflCo [Type]
arg_tys)
                                  Coercion -> Coercion -> Coercion
`mkTcTransCo`
                                  Role -> TyCon -> [Coercion] -> Coercion
mkTcTyConAppCo Role
Representational TyCon
tc
                                    ((Role -> Type -> Coercion) -> [Role] -> [Type] -> [Coercion]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Role -> Type -> Coercion
mkReflCo [Role]
tc_roles [Type]
xis [Coercion] -> [Coercion] -> [Coercion]
forall a. [a] -> [a] -> [a]
++ [Coercion]
arg_cos)

                ; HetReduction -> RewriteM HetReduction
forall (m :: * -> *) a. Monad m => a -> m a
return (HetReduction -> RewriteM HetReduction)
-> HetReduction -> RewriteM HetReduction
forall a b. (a -> b) -> a -> b
$
                    Reduction -> MCoercionN -> HetReduction
mkHetReduction
                      (Coercion -> Type -> Reduction
mkReduction Coercion
app_co Type
app_xi )
                      MCoercionN
kind_co }
           Maybe (TyCon, [Type])
Nothing ->
             do { ArgsReductions Reductions
redns MCoercionN
kind_co
                    <- Type -> [Role] -> [Type] -> RewriteM ArgsReductions
rewrite_vector (HasDebugCallStack => Type -> Type
Type -> Type
tcTypeKind Type
fun_xi) (Role -> [Role]
forall a. a -> [a]
repeat Role
Nominal) [Type]
arg_tys
                ; HetReduction -> RewriteM HetReduction
forall (m :: * -> *) a. Monad m => a -> m a
return (HetReduction -> RewriteM HetReduction)
-> HetReduction -> RewriteM HetReduction
forall a b. (a -> b) -> a -> b
$ Reduction -> MCoercionN -> HetReduction
mkHetReduction (Reduction -> Reductions -> Reduction
mkAppRedns Reduction
fun_redn Reductions
redns) MCoercionN
kind_co }

       ; Role
role <- RewriteM Role
getRole
       ; Reduction -> RewriteM Reduction
forall (m :: * -> *) a. Monad m => a -> m a
return (Role -> HetReduction -> Reduction
homogeniseHetRedn Role
role HetReduction
het_redn) }

rewrite_ty_con_app :: TyCon -> [TcType] -> RewriteM Reduction
rewrite_ty_con_app :: TyCon -> [Type] -> RewriteM Reduction
rewrite_ty_con_app TyCon
tc [Type]
tys
  = do { Role
role <- RewriteM Role
getRole
       ; let m_roles :: Maybe [Role]
m_roles | Role
Nominal <- Role
role = Maybe [Role]
forall a. Maybe a
Nothing
                     | Bool
otherwise       = [Role] -> Maybe [Role]
forall a. a -> Maybe a
Just ([Role] -> Maybe [Role]) -> [Role] -> Maybe [Role]
forall a b. (a -> b) -> a -> b
$ Role -> TyCon -> [Role]
tyConRolesX Role
role TyCon
tc
       ; ArgsReductions Reductions
redns MCoercionN
kind_co <- TyCon -> Maybe [Role] -> [Type] -> RewriteM ArgsReductions
rewrite_args_tc TyCon
tc Maybe [Role]
m_roles [Type]
tys
       ; let tyconapp_redn :: HetReduction
tyconapp_redn
                = Reduction -> MCoercionN -> HetReduction
mkHetReduction
                    (Role -> TyCon -> Reductions -> Reduction
mkTyConAppRedn Role
role TyCon
tc Reductions
redns)
                    MCoercionN
kind_co
       ; Reduction -> RewriteM Reduction
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> RewriteM Reduction)
-> Reduction -> RewriteM Reduction
forall a b. (a -> b) -> a -> b
$ Role -> HetReduction -> Reduction
homogeniseHetRedn Role
role HetReduction
tyconapp_redn }

-- Rewrite a vector (list of arguments).
rewrite_vector :: Kind   -- of the function being applied to these arguments
               -> [Role] -- If we're rewriting w.r.t. ReprEq, what roles do the
                         -- args have?
               -> [Type] -- the args to rewrite
               -> RewriteM ArgsReductions
rewrite_vector :: Type -> [Role] -> [Type] -> RewriteM ArgsReductions
rewrite_vector Type
ki [Role]
roles [Type]
tys
  = do { EqRel
eq_rel <- RewriteM EqRel
getEqRel
       ; let mb_roles :: Maybe [Role]
mb_roles = case EqRel
eq_rel of { EqRel
NomEq -> Maybe [Role]
forall a. Maybe a
Nothing; EqRel
ReprEq -> [Role] -> Maybe [Role]
forall a. a -> Maybe a
Just [Role]
roles }
       ; [TyCoBinder]
-> Bool
-> Type
-> TcTyCoVarSet
-> Maybe [Role]
-> [Type]
-> RewriteM ArgsReductions
rewrite_args [TyCoBinder]
bndrs Bool
any_named_bndrs Type
inner_ki TcTyCoVarSet
fvs Maybe [Role]
mb_roles [Type]
tys
       }
  where
    ([TyCoBinder]
bndrs, Type
inner_ki, Bool
any_named_bndrs) = Type -> ([TyCoBinder], Type, Bool)
split_pi_tys' Type
ki
    fvs :: TcTyCoVarSet
fvs                                = Type -> TcTyCoVarSet
tyCoVarsOfType Type
ki
{-# INLINE rewrite_vector #-}

{-
Note [Rewriting synonyms]
~~~~~~~~~~~~~~~~~~~~~~~~~~
Not expanding synonyms aggressively improves error messages, and
keeps types smaller. But we need to take care.

Suppose
   type Syn a = Int
   type instance F Bool = Syn (F Bool)
   [G] F Bool ~ Syn (F Bool)

If we don't expand the synonym, we'll get a spurious occurs-check
failure. This is normally what occCheckExpand takes care of, but
the LHS is a type family application, and occCheckExpand (already
complex enough as it is) does not know how to expand to avoid
a type family application.

In addition, expanding the forgetful synonym like this
will generally yield a *smaller* type. To wit, if we spot
S ( ... F tys ... ), where S is forgetful, we don't want to bother
doing hard work simplifying (F tys). We thus expand forgetful
synonyms, but not others.

isForgetfulSynTyCon returns True more often than it needs to, so
we err on the side of more expansion.

We also, of course, must expand type synonyms that mention type families,
so those families can get reduced.

************************************************************************
*                                                                      *
             Rewriting a type-family application
*                                                                      *
************************************************************************

Note [How to normalise a family application]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Given an exactly saturated family application, how should we normalise it?
This Note spells out the algorithm and its reasoning.

First, we attempt to directly rewrite the type family application,
without simplifying any of the arguments first, in an attempt to avoid
doing unnecessary work.

STEP 1a. Call the rewriting plugins. If any plugin rewrites the type family
application, jump to FINISH.

STEP 1b. Try the famapp-cache. If we get a cache hit, jump to FINISH.

STEP 1c. Try top-level instances. Remember: we haven't simplified the arguments
  yet. Example:
    type instance F (Maybe a) = Int
    target: F (Maybe (G Bool))
  Instead of first trying to simplify (G Bool), we use the instance first. This
  avoids the work of simplifying G Bool.

  If an instance is found, jump to FINISH.

STEP 2: At this point we rewrite all arguments. This might expose more
  information, which might allow plugins to make progress, or allow us to
  pick up a top-level instance.

STEP 3. Try the inerts. Note that we try the inerts *after* rewriting the
  arguments, because the inerts will have rewritten LHSs.

  If an inert is found, jump to FINISH.

Next, we try STEP 1 again, as we might be able to make further progress after
having rewritten the arguments:

STEP 4a. Query the rewriting plugins again.

  If any plugin supplies a rewriting, jump to FINISH.

STEP 4b. Try the famapp-cache again.

  If we get a cache hit, jump to FINISH.

STEP 4c. Try top-level instances again.

  If an instance is found, jump to FINISH.

STEP 5: GIVEUP. No progress to be made. Return what we have. (Do not FINISH.)

FINISH 1. We've made a reduction, but the new type may still have more
  work to do. So rewrite the new type.

FINISH 2. Add the result to the famapp-cache, connecting the type we started
  with to the one we ended with.

Because STEP 1{a,b,c} and STEP 4{a,b,c} happen the same way, they are abstracted into
try_to_reduce.

FINISH is naturally implemented in `finish`. But, Note [rewrite_exact_fam_app performance]
tells us that we should not add to the famapp-cache after STEP 1. So `finish`
is inlined in that case, and only FINISH 1 is performed.

-}

rewrite_fam_app :: TyCon -> [TcType] -> RewriteM Reduction
  --   rewrite_fam_app            can be over-saturated
  --   rewrite_exact_fam_app      lifts out the application to top level
  -- Postcondition: Coercion :: Xi ~ F tys
rewrite_fam_app :: TyCon -> [Type] -> RewriteM Reduction
rewrite_fam_app TyCon
tc [Type]
tys  -- Can be over-saturated
    = Bool -> SDoc -> RewriteM Reduction -> RewriteM Reduction
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr ([Type]
tys [Type] -> Int -> Bool
forall a. [a] -> Int -> Bool
`lengthAtLeast` TyCon -> Int
tyConArity TyCon
tc)
                (TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc SDoc -> SDoc -> SDoc
$$ Int -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TyCon -> Int
tyConArity TyCon
tc) SDoc -> SDoc -> SDoc
$$ [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys) (RewriteM Reduction -> RewriteM Reduction)
-> RewriteM Reduction -> RewriteM Reduction
forall a b. (a -> b) -> a -> b
$

                 -- Type functions are saturated
                 -- The type function might be *over* saturated
                 -- in which case the remaining arguments should
                 -- be dealt with by AppTys
      do { let ([Type]
tys1, [Type]
tys_rest) = Int -> [Type] -> ([Type], [Type])
forall a. Int -> [a] -> ([a], [a])
splitAt (TyCon -> Int
tyConArity TyCon
tc) [Type]
tys
         ; Reduction
redn <- TyCon -> [Type] -> RewriteM Reduction
rewrite_exact_fam_app TyCon
tc [Type]
tys1
         ; Reduction -> [Type] -> RewriteM Reduction
rewrite_app_ty_args Reduction
redn [Type]
tys_rest }

-- the [TcType] exactly saturate the TyCon
-- See Note [How to normalise a family application]
rewrite_exact_fam_app :: TyCon -> [TcType] -> RewriteM Reduction
rewrite_exact_fam_app :: TyCon -> [Type] -> RewriteM Reduction
rewrite_exact_fam_app TyCon
tc [Type]
tys
  = do { Type -> RewriteM ()
checkStackDepth (TyCon -> [Type] -> Type
mkTyConApp TyCon
tc [Type]
tys)

       -- Query the typechecking plugins for all their rewriting functions
       -- which apply to a type family application headed by the TyCon 'tc'.
       ; [TcPluginRewriter]
tc_rewriters <- TyCon -> RewriteM [TcPluginRewriter]
getTcPluginRewritersForTyCon TyCon
tc

       -- STEP 1. Try to reduce without reducing arguments first.
       ; Maybe Reduction
result1 <- TyCon -> [Type] -> [TcPluginRewriter] -> RewriteM (Maybe Reduction)
try_to_reduce TyCon
tc [Type]
tys [TcPluginRewriter]
tc_rewriters
       ; case Maybe Reduction
result1 of
             -- Don't use the cache;
             -- See Note [rewrite_exact_fam_app performance]
         { Just Reduction
redn -> Bool -> Reduction -> RewriteM Reduction
finish Bool
False Reduction
redn
         ; Maybe Reduction
Nothing ->

        -- That didn't work. So reduce the arguments, in STEP 2.
    do { EqRel
eq_rel <- RewriteM EqRel
getEqRel
          -- checking eq_rel == NomEq saves ~0.5% in T9872a
       ; ArgsReductions (Reductions [Coercion]
cos [Type]
xis) MCoercionN
kind_co <-
            if EqRel
eq_rel EqRel -> EqRel -> Bool
forall a. Eq a => a -> a -> Bool
== EqRel
NomEq
            then TyCon -> Maybe [Role] -> [Type] -> RewriteM ArgsReductions
rewrite_args_tc TyCon
tc Maybe [Role]
forall a. Maybe a
Nothing [Type]
tys
            else EqRel -> RewriteM ArgsReductions -> RewriteM ArgsReductions
forall a. EqRel -> RewriteM a -> RewriteM a
setEqRel EqRel
NomEq (RewriteM ArgsReductions -> RewriteM ArgsReductions)
-> RewriteM ArgsReductions -> RewriteM ArgsReductions
forall a b. (a -> b) -> a -> b
$
                 TyCon -> Maybe [Role] -> [Type] -> RewriteM ArgsReductions
rewrite_args_tc TyCon
tc Maybe [Role]
forall a. Maybe a
Nothing [Type]
tys

         -- If we manage to rewrite the type family application after
         -- rewriting the arguments, we will need to compose these
         -- reductions.
         --
         -- We have:
         --
         --   arg_co_i :: ty_i ~ xi_i
         --   fam_co :: F xi_1 ... xi_n ~ zeta
         --
         -- The full reduction is obtained as a composite:
         --
         --   full_co :: F ty_1 ... ty_n ~ zeta
         --   full_co = F co_1 ... co_n ;; fam_co
       ; let
           role :: Role
role    = EqRel -> Role
eqRelRole EqRel
eq_rel
           args_co :: Coercion
args_co = HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
role TyCon
tc [Coercion]
cos
       ;  let homogenise :: Reduction -> Reduction
              homogenise :: Reduction -> Reduction
homogenise Reduction
redn
                = Role -> HetReduction -> Reduction
homogeniseHetRedn Role
role
                (HetReduction -> Reduction) -> HetReduction -> Reduction
forall a b. (a -> b) -> a -> b
$ Reduction -> MCoercionN -> HetReduction
mkHetReduction
                    (Coercion
args_co Coercion -> Reduction -> Reduction
`mkTransRedn` Reduction
redn)
                    MCoercionN
kind_co

              give_up :: Reduction
              give_up :: Reduction
give_up = Reduction -> Reduction
homogenise (Reduction -> Reduction) -> Reduction -> Reduction
forall a b. (a -> b) -> a -> b
$ Role -> Type -> Reduction
mkReflRedn Role
role Type
reduced
                where reduced :: Type
reduced = TyCon -> [Type] -> Type
mkTyConApp TyCon
tc [Type]
xis

         -- STEP 3: try the inerts
       ; CtFlavour
flavour <- RewriteM CtFlavour
getFlavour
       ; Maybe (Reduction, CtFlavourRole)
result2 <- TcS (Maybe (Reduction, CtFlavourRole))
-> RewriteM (Maybe (Reduction, CtFlavourRole))
forall a. TcS a -> RewriteM a
liftTcS (TcS (Maybe (Reduction, CtFlavourRole))
 -> RewriteM (Maybe (Reduction, CtFlavourRole)))
-> TcS (Maybe (Reduction, CtFlavourRole))
-> RewriteM (Maybe (Reduction, CtFlavourRole))
forall a b. (a -> b) -> a -> b
$ (CtFlavourRole -> Bool)
-> TyCon -> [Type] -> TcS (Maybe (Reduction, CtFlavourRole))
lookupFamAppInert (CtFlavourRole -> CtFlavourRole -> Bool
`eqCanRewriteFR` (CtFlavour
flavour, EqRel
eq_rel)) TyCon
tc [Type]
xis
       ; case Maybe (Reduction, CtFlavourRole)
result2 of
         { Just (Reduction
redn, (CtFlavour
inert_flavour, EqRel
inert_eq_rel))
             -> do { String -> SDoc -> RewriteM ()
traceRewriteM String
"rewrite family application with inert"
                                (TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc SDoc -> SDoc -> SDoc
<+> [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
xis SDoc -> SDoc -> SDoc
$$ Reduction -> SDoc
forall a. Outputable a => a -> SDoc
ppr Reduction
redn)
                   ; Bool -> Reduction -> RewriteM Reduction
finish (CtFlavour
inert_flavour CtFlavour -> CtFlavour -> Bool
forall a. Eq a => a -> a -> Bool
== CtFlavour
Given) (Reduction -> Reduction
homogenise Reduction
downgraded_redn) }
               -- this will sometimes duplicate an inert in the cache,
               -- but avoiding doing so had no impact on performance, and
               -- it seems easier not to weed out that special case
             where
               inert_role :: Role
inert_role      = EqRel -> Role
eqRelRole EqRel
inert_eq_rel
               role :: Role
role            = EqRel -> Role
eqRelRole EqRel
eq_rel
               downgraded_redn :: Reduction
downgraded_redn = Role -> Role -> Reduction -> Reduction
downgradeRedn Role
role Role
inert_role Reduction
redn

         ; Maybe (Reduction, CtFlavourRole)
_ ->

         -- inerts didn't work. Try to reduce again, in STEP 4.
    do { Maybe Reduction
result3 <- TyCon -> [Type] -> [TcPluginRewriter] -> RewriteM (Maybe Reduction)
try_to_reduce TyCon
tc [Type]
xis [TcPluginRewriter]
tc_rewriters
       ; case Maybe Reduction
result3 of
           Just Reduction
redn -> Bool -> Reduction -> RewriteM Reduction
finish Bool
True (Reduction -> Reduction
homogenise Reduction
redn)
           -- we have made no progress at all: STEP 5 (GIVEUP).
           Maybe Reduction
_         -> Reduction -> RewriteM Reduction
forall (m :: * -> *) a. Monad m => a -> m a
return Reduction
give_up }}}}}
  where
      -- call this if the above attempts made progress.
      -- This recursively rewrites the result and then adds to the cache
    finish :: Bool  -- add to the cache?
                    -- Precondition: True ==> input coercion has
                    --                        no coercion holes
           -> Reduction -> RewriteM Reduction
    finish :: Bool -> Reduction -> RewriteM Reduction
finish Bool
use_cache Reduction
redn
      = do { -- rewrite the result: FINISH 1
             Reduction
final_redn <- Reduction -> RewriteM Reduction
rewrite_reduction Reduction
redn
           ; EqRel
eq_rel <- RewriteM EqRel
getEqRel

             -- extend the cache: FINISH 2
           ; Bool -> RewriteM () -> RewriteM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
use_cache Bool -> Bool -> Bool
&& EqRel
eq_rel EqRel -> EqRel -> Bool
forall a. Eq a => a -> a -> Bool
== EqRel
NomEq) (RewriteM () -> RewriteM ()) -> RewriteM () -> RewriteM ()
forall a b. (a -> b) -> a -> b
$
             -- the cache only wants Nominal eqs
             TcS () -> RewriteM ()
forall a. TcS a -> RewriteM a
liftTcS (TcS () -> RewriteM ()) -> TcS () -> RewriteM ()
forall a b. (a -> b) -> a -> b
$ TyCon -> [Type] -> Reduction -> TcS ()
extendFamAppCache TyCon
tc [Type]
tys Reduction
final_redn
           ; Reduction -> RewriteM Reduction
forall (m :: * -> *) a. Monad m => a -> m a
return Reduction
final_redn }
    {-# INLINE finish #-}

-- Returned coercion is input ~r output, where r is the role in the RewriteM monad
-- See Note [How to normalise a family application]
try_to_reduce :: TyCon -> [TcType] -> [TcPluginRewriter]
              -> RewriteM (Maybe Reduction)
try_to_reduce :: TyCon -> [Type] -> [TcPluginRewriter] -> RewriteM (Maybe Reduction)
try_to_reduce TyCon
tc [Type]
tys [TcPluginRewriter]
tc_rewriters
  = do { RewriteEnv
rewrite_env <- RewriteM RewriteEnv
getRewriteEnv
       ; Maybe Reduction
result <-
            TcS (Maybe Reduction) -> RewriteM (Maybe Reduction)
forall a. TcS a -> RewriteM a
liftTcS (TcS (Maybe Reduction) -> RewriteM (Maybe Reduction))
-> TcS (Maybe Reduction) -> RewriteM (Maybe Reduction)
forall a b. (a -> b) -> a -> b
$ [TcS (Maybe Reduction)] -> TcS (Maybe Reduction)
forall (m :: * -> *) (f :: * -> *) a.
(Monad m, Foldable f) =>
f (m (Maybe a)) -> m (Maybe a)
firstJustsM
              [ RewriteEnv -> [TcPluginRewriter] -> [Type] -> TcS (Maybe Reduction)
runTcPluginRewriters RewriteEnv
rewrite_env [TcPluginRewriter]
tc_rewriters [Type]
tys -- STEP 1a & STEP 4a
              , TyCon -> [Type] -> TcS (Maybe Reduction)
lookupFamAppCache TyCon
tc [Type]
tys                          -- STEP 1b & STEP 4b
              , TyCon -> [Type] -> TcS (Maybe Reduction)
matchFam TyCon
tc [Type]
tys ]                                 -- STEP 1c & STEP 4c
       ; (Reduction -> RewriteM Reduction)
-> Maybe Reduction -> RewriteM (Maybe Reduction)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Reduction -> RewriteM Reduction
downgrade Maybe Reduction
result }
  where
    -- The result above is always Nominal. We might want a Representational
    -- coercion; this downgrades (and prints, out of convenience).
    downgrade :: Reduction -> RewriteM Reduction
    downgrade :: Reduction -> RewriteM Reduction
downgrade Reduction
redn
      = do { String -> SDoc -> RewriteM ()
traceRewriteM String
"Eager T.F. reduction success" (SDoc -> RewriteM ()) -> SDoc -> RewriteM ()
forall a b. (a -> b) -> a -> b
$
             [SDoc] -> SDoc
vcat [ TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc
                  , [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys
                  , Reduction -> SDoc
forall a. Outputable a => a -> SDoc
ppr Reduction
redn
                  ]
           ; EqRel
eq_rel <- RewriteM EqRel
getEqRel
              -- manually doing it this way avoids allocation in the vastly
              -- common NomEq case
           ; case EqRel
eq_rel of
               EqRel
NomEq  -> Reduction -> RewriteM Reduction
forall (m :: * -> *) a. Monad m => a -> m a
return Reduction
redn
               EqRel
ReprEq -> Reduction -> RewriteM Reduction
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> RewriteM Reduction)
-> Reduction -> RewriteM Reduction
forall a b. (a -> b) -> a -> b
$ Reduction -> Reduction
mkSubRedn Reduction
redn }

-- Retrieve all type-checking plugins that can rewrite a (saturated) type-family application
-- headed by the given 'TyCon`.
getTcPluginRewritersForTyCon :: TyCon -> RewriteM [TcPluginRewriter]
getTcPluginRewritersForTyCon :: TyCon -> RewriteM [TcPluginRewriter]
getTcPluginRewritersForTyCon TyCon
tc
  = TcS [TcPluginRewriter] -> RewriteM [TcPluginRewriter]
forall a. TcS a -> RewriteM a
liftTcS (TcS [TcPluginRewriter] -> RewriteM [TcPluginRewriter])
-> TcS [TcPluginRewriter] -> RewriteM [TcPluginRewriter]
forall a b. (a -> b) -> a -> b
$ do { UniqFM TyCon [TcPluginRewriter]
rewriters <- TcGblEnv -> UniqFM TyCon [TcPluginRewriter]
tcg_tc_plugin_rewriters (TcGblEnv -> UniqFM TyCon [TcPluginRewriter])
-> TcS TcGblEnv -> TcS (UniqFM TyCon [TcPluginRewriter])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcS TcGblEnv
getGblEnv
                 ; [TcPluginRewriter] -> TcS [TcPluginRewriter]
forall (m :: * -> *) a. Monad m => a -> m a
return (UniqFM TyCon [TcPluginRewriter]
-> [TcPluginRewriter] -> TyCon -> [TcPluginRewriter]
forall key elt.
Uniquable key =>
UniqFM key elt -> elt -> key -> elt
lookupWithDefaultUFM UniqFM TyCon [TcPluginRewriter]
rewriters [] TyCon
tc) }

-- Run a collection of rewriting functions obtained from type-checking plugins,
-- querying in sequence if any plugin wants to rewrite the type family
-- applied to the given arguments.
--
-- Note that the 'TcPluginRewriter's provided all pertain to the same type family
-- (the 'TyCon' of which has been obtained ahead of calling this function).
runTcPluginRewriters :: RewriteEnv
                     -> [TcPluginRewriter]
                     -> [TcType]
                     -> TcS (Maybe Reduction)
runTcPluginRewriters :: RewriteEnv -> [TcPluginRewriter] -> [Type] -> TcS (Maybe Reduction)
runTcPluginRewriters RewriteEnv
rewriteEnv [TcPluginRewriter]
rewriterFunctions [Type]
tys
  | [TcPluginRewriter] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcPluginRewriter]
rewriterFunctions
  = Maybe Reduction -> TcS (Maybe Reduction)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Reduction
forall a. Maybe a
Nothing -- short-circuit for common case
  | Bool
otherwise
  = do { [Ct]
givens <- TcS [Ct]
getInertGivens
       ; [Ct] -> [TcPluginRewriter] -> TcS (Maybe Reduction)
runRewriters [Ct]
givens [TcPluginRewriter]
rewriterFunctions }
  where
  runRewriters :: [Ct] -> [TcPluginRewriter] -> TcS (Maybe Reduction)
  runRewriters :: [Ct] -> [TcPluginRewriter] -> TcS (Maybe Reduction)
runRewriters [Ct]
_ []
    = Maybe Reduction -> TcS (Maybe Reduction)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Reduction
forall a. Maybe a
Nothing
  runRewriters [Ct]
givens (TcPluginRewriter
rewriter:[TcPluginRewriter]
rewriters)
    = do
        TcPluginRewriteResult
rewriteResult <- TcM TcPluginRewriteResult -> TcS TcPluginRewriteResult
forall a. TcM a -> TcS a
wrapTcS (TcM TcPluginRewriteResult -> TcS TcPluginRewriteResult)
-> (TcPluginM TcPluginRewriteResult -> TcM TcPluginRewriteResult)
-> TcPluginM TcPluginRewriteResult
-> TcS TcPluginRewriteResult
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcPluginM TcPluginRewriteResult -> TcM TcPluginRewriteResult
forall a. TcPluginM a -> TcM a
runTcPluginM (TcPluginM TcPluginRewriteResult -> TcS TcPluginRewriteResult)
-> TcPluginM TcPluginRewriteResult -> TcS TcPluginRewriteResult
forall a b. (a -> b) -> a -> b
$ TcPluginRewriter
rewriter RewriteEnv
rewriteEnv [Ct]
givens [Type]
tys
        case TcPluginRewriteResult
rewriteResult of
           TcPluginRewriteTo
             { tcPluginReduction :: TcPluginRewriteResult -> Reduction
tcPluginReduction    = Reduction
redn
             , tcRewriterNewWanteds :: TcPluginRewriteResult -> [Ct]
tcRewriterNewWanteds = [Ct]
wanteds
             } -> do { [Ct] -> TcS ()
emitWork [Ct]
wanteds; Maybe Reduction -> TcS (Maybe Reduction)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Reduction -> TcS (Maybe Reduction))
-> Maybe Reduction -> TcS (Maybe Reduction)
forall a b. (a -> b) -> a -> b
$ Reduction -> Maybe Reduction
forall a. a -> Maybe a
Just Reduction
redn }
           TcPluginNoRewrite {} -> [Ct] -> [TcPluginRewriter] -> TcS (Maybe Reduction)
runRewriters [Ct]
givens [TcPluginRewriter]
rewriters

{-
************************************************************************
*                                                                      *
             Rewriting a type variable
*                                                                      *
********************************************************************* -}

-- | The result of rewriting a tyvar "one step".
data RewriteTvResult
  = RTRNotFollowed
      -- ^ The inert set doesn't make the tyvar equal to anything else

  | RTRFollowed !Reduction
      -- ^ The tyvar rewrites to a not-necessarily rewritten other type.
      -- The role is determined by the RewriteEnv.
      --
      -- With Quick Look, the returned TcType can be a polytype;
      -- that is, in the constraint solver, a unification variable
      -- can contain a polytype.  See GHC.Tc.Gen.App
      -- Note [Instantiation variables are short lived]

rewriteTyVar :: TyVar -> RewriteM Reduction
rewriteTyVar :: Var -> RewriteM Reduction
rewriteTyVar Var
tv
  = do { RewriteTvResult
mb_yes <- Var -> RewriteM RewriteTvResult
rewrite_tyvar1 Var
tv
       ; case RewriteTvResult
mb_yes of
           RTRFollowed Reduction
redn -> Reduction -> RewriteM Reduction
rewrite_reduction Reduction
redn

           RewriteTvResult
RTRNotFollowed   -- Done, but make sure the kind is zonked
                            -- Note [Rewriting] invariant (F0) and (F1)
             -> do { Var
tv' <- TcS Var -> RewriteM Var
forall a. TcS a -> RewriteM a
liftTcS (TcS Var -> RewriteM Var) -> TcS Var -> RewriteM Var
forall a b. (a -> b) -> a -> b
$ (Type -> TcS Type) -> Var -> TcS Var
forall (m :: * -> *). Monad m => (Type -> m Type) -> Var -> m Var
updateTyVarKindM Type -> TcS Type
zonkTcType Var
tv
                   ; Role
role <- RewriteM Role
getRole
                   ; let ty' :: Type
ty' = Var -> Type
mkTyVarTy Var
tv'
                   ; Reduction -> RewriteM Reduction
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> RewriteM Reduction)
-> Reduction -> RewriteM Reduction
forall a b. (a -> b) -> a -> b
$ Role -> Type -> Reduction
mkReflRedn Role
role Type
ty' } }

rewrite_tyvar1 :: TcTyVar -> RewriteM RewriteTvResult
-- "Rewriting" a type variable means to apply the substitution to it
-- Specifically, look up the tyvar in
--   * the internal MetaTyVar box
--   * the inerts
-- See also the documentation for RewriteTvResult

rewrite_tyvar1 :: Var -> RewriteM RewriteTvResult
rewrite_tyvar1 Var
tv
  = do { Maybe Type
mb_ty <- TcS (Maybe Type) -> RewriteM (Maybe Type)
forall a. TcS a -> RewriteM a
liftTcS (TcS (Maybe Type) -> RewriteM (Maybe Type))
-> TcS (Maybe Type) -> RewriteM (Maybe Type)
forall a b. (a -> b) -> a -> b
$ Var -> TcS (Maybe Type)
isFilledMetaTyVar_maybe Var
tv
       ; case Maybe Type
mb_ty of
           Just Type
ty -> do { String -> SDoc -> RewriteM ()
traceRewriteM String
"Following filled tyvar"
                             (Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
tv SDoc -> SDoc -> SDoc
<+> SDoc
equals SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)
                         ; Role
role <- RewriteM Role
getRole
                         ; RewriteTvResult -> RewriteM RewriteTvResult
forall (m :: * -> *) a. Monad m => a -> m a
return (RewriteTvResult -> RewriteM RewriteTvResult)
-> RewriteTvResult -> RewriteM RewriteTvResult
forall a b. (a -> b) -> a -> b
$ Reduction -> RewriteTvResult
RTRFollowed (Reduction -> RewriteTvResult) -> Reduction -> RewriteTvResult
forall a b. (a -> b) -> a -> b
$
                             Role -> Type -> Reduction
mkReflRedn Role
role Type
ty }
           Maybe Type
Nothing -> do { String -> SDoc -> RewriteM ()
traceRewriteM String
"Unfilled tyvar" (Var -> SDoc
pprTyVar Var
tv)
                         ; CtFlavourRole
fr <- RewriteM CtFlavourRole
getFlavourRole
                         ; Var -> CtFlavourRole -> RewriteM RewriteTvResult
rewrite_tyvar2 Var
tv CtFlavourRole
fr } }

rewrite_tyvar2 :: TcTyVar -> CtFlavourRole -> RewriteM RewriteTvResult
-- The tyvar is not a filled-in meta-tyvar
-- Try in the inert equalities
-- See Definition [Applying a generalised substitution] in GHC.Tc.Solver.Monad
-- See Note [Stability of rewriting] in GHC.Tc.Solver.Monad

rewrite_tyvar2 :: Var -> CtFlavourRole -> RewriteM RewriteTvResult
rewrite_tyvar2 Var
tv fr :: CtFlavourRole
fr@(CtFlavour
_, EqRel
eq_rel)
  = do { InertEqs
ieqs <- TcS InertEqs -> RewriteM InertEqs
forall a. TcS a -> RewriteM a
liftTcS (TcS InertEqs -> RewriteM InertEqs)
-> TcS InertEqs -> RewriteM InertEqs
forall a b. (a -> b) -> a -> b
$ TcS InertEqs
getInertEqs
       ; case InertEqs -> Var -> Maybe [Ct]
forall a. DVarEnv a -> Var -> Maybe a
lookupDVarEnv InertEqs
ieqs Var
tv of
           Just [Ct]
equal_ct_list
             | Just Ct
ct <- (Ct -> Bool) -> [Ct] -> Maybe Ct
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find Ct -> Bool
can_rewrite [Ct]
equal_ct_list
             , CEqCan { cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
ctev, cc_lhs :: Ct -> CanEqLHS
cc_lhs = TyVarLHS Var
tv
                      , cc_rhs :: Ct -> Type
cc_rhs = Type
rhs_ty, cc_eq_rel :: Ct -> EqRel
cc_eq_rel = EqRel
ct_eq_rel } <- Ct
ct
             -> do { let wrw :: Bool
wrw = Ct -> Bool
isWantedCt Ct
ct
                   ; String -> SDoc -> RewriteM ()
traceRewriteM String
"Following inert tyvar" (SDoc -> RewriteM ()) -> SDoc -> RewriteM ()
forall a b. (a -> b) -> a -> b
$
                        [SDoc] -> SDoc
vcat [ Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
tv SDoc -> SDoc -> SDoc
<+> SDoc
equals SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
rhs_ty
                             , CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ctev
                             , String -> SDoc
text String
"wanted_rewrite_wanted:" SDoc -> SDoc -> SDoc
<+> Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bool
wrw ]
                   ; Bool -> RewriteM () -> RewriteM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
wrw (RewriteM () -> RewriteM ()) -> RewriteM () -> RewriteM ()
forall a b. (a -> b) -> a -> b
$ CtEvidence -> RewriteM ()
recordRewriter CtEvidence
ctev

                   ; let rewriting_co1 :: Coercion
rewriting_co1 = HasDebugCallStack => CtEvidence -> Coercion
CtEvidence -> Coercion
ctEvCoercion CtEvidence
ctev
                         rewriting_co :: Coercion
rewriting_co  = case (EqRel
ct_eq_rel, EqRel
eq_rel) of
                            (EqRel
ReprEq, EqRel
_rel)  -> Bool -> Coercion -> Coercion
forall a. HasCallStack => Bool -> a -> a
assert (EqRel
_rel EqRel -> EqRel -> Bool
forall a. Eq a => a -> a -> Bool
== EqRel
ReprEq)
                                    -- if this assert fails, then
                                    -- eqCanRewriteFR answered incorrectly
                                               Coercion
rewriting_co1
                            (EqRel
NomEq, EqRel
NomEq)  -> Coercion
rewriting_co1
                            (EqRel
NomEq, EqRel
ReprEq) -> HasDebugCallStack => Coercion -> Coercion
Coercion -> Coercion
mkSubCo Coercion
rewriting_co1

                   ; RewriteTvResult -> RewriteM RewriteTvResult
forall (m :: * -> *) a. Monad m => a -> m a
return (RewriteTvResult -> RewriteM RewriteTvResult)
-> RewriteTvResult -> RewriteM RewriteTvResult
forall a b. (a -> b) -> a -> b
$ Reduction -> RewriteTvResult
RTRFollowed (Reduction -> RewriteTvResult) -> Reduction -> RewriteTvResult
forall a b. (a -> b) -> a -> b
$ Coercion -> Type -> Reduction
mkReduction Coercion
rewriting_co Type
rhs_ty }

           Maybe [Ct]
_other -> RewriteTvResult -> RewriteM RewriteTvResult
forall (m :: * -> *) a. Monad m => a -> m a
return RewriteTvResult
RTRNotFollowed }

  where
    can_rewrite :: Ct -> Bool
    can_rewrite :: Ct -> Bool
can_rewrite Ct
ct = Ct -> CtFlavourRole
ctFlavourRole Ct
ct CtFlavourRole -> CtFlavourRole -> Bool
`eqCanRewriteFR` CtFlavourRole
fr
      -- This is THE key call of eqCanRewriteFR

{-
Note [An alternative story for the inert substitution]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
(This entire note is just background, left here in case we ever want
 to return the previous state of affairs)

We used (GHC 7.8) to have this story for the inert substitution inert_eqs

 * 'a' is not in fvs(ty)
 * They are *inert* in the weaker sense that there is no infinite chain of
   (i1 `eqCanRewrite` i2), (i2 `eqCanRewrite` i3), etc

This means that rewriting must be recursive, but it does allow
  [G] a ~ [b]
  [G] b ~ Maybe c

This avoids "saturating" the Givens, which can save a modest amount of work.
It is easy to implement, in GHC.Tc.Solver.Interact.kick_out, by only kicking out an inert
only if (a) the work item can rewrite the inert AND
        (b) the inert cannot rewrite the work item

This is significantly harder to think about. It can save a LOT of work
in occurs-check cases, but we don't care about them much.  #5837
is an example, but it causes trouble only with the old (pre-Fall 2020)
rewriting story. It is unclear if there is any gain w.r.t. to
the new story.

-}

--------------------------------------
-- Utilities

-- | Like 'splitPiTys'' but comes with a 'Bool' which is 'True' iff there is at
-- least one named binder.
split_pi_tys' :: Type -> ([TyCoBinder], Type, Bool)
split_pi_tys' :: Type -> ([TyCoBinder], Type, Bool)
split_pi_tys' Type
ty = Type -> Type -> ([TyCoBinder], Type, Bool)
split Type
ty Type
ty
  where
     -- put common cases first
  split :: Type -> Type -> ([TyCoBinder], Type, Bool)
split Type
_       (ForAllTy TyVarBinder
b Type
res) = let -- This bang is necessary lest we see rather
                                       -- terrible reboxing, as noted in #19102.
                                       !([TyCoBinder]
bs, Type
ty, Bool
_) = Type -> Type -> ([TyCoBinder], Type, Bool)
split Type
res Type
res
                                   in  (TyVarBinder -> TyCoBinder
Named TyVarBinder
b TyCoBinder -> [TyCoBinder] -> [TyCoBinder]
forall a. a -> [a] -> [a]
: [TyCoBinder]
bs, Type
ty, Bool
True)
  split Type
_       (FunTy { ft_af :: Type -> AnonArgFlag
ft_af = AnonArgFlag
af, ft_mult :: Type -> Type
ft_mult = Type
w, ft_arg :: Type -> Type
ft_arg = Type
arg, ft_res :: Type -> Type
ft_res = Type
res })
                                 = let -- See #19102
                                       !([TyCoBinder]
bs, Type
ty, Bool
named) = Type -> Type -> ([TyCoBinder], Type, Bool)
split Type
res Type
res
                                   in  (AnonArgFlag -> Scaled Type -> TyCoBinder
Anon AnonArgFlag
af (Type -> Type -> Scaled Type
forall a. Type -> a -> Scaled a
mkScaled Type
w Type
arg) TyCoBinder -> [TyCoBinder] -> [TyCoBinder]
forall a. a -> [a] -> [a]
: [TyCoBinder]
bs, Type
ty, Bool
named)

  split Type
orig_ty Type
ty | Just Type
ty' <- Type -> Maybe Type
coreView Type
ty = Type -> Type -> ([TyCoBinder], Type, Bool)
split Type
orig_ty Type
ty'
  split Type
orig_ty Type
_                = ([], Type
orig_ty, Bool
False)
{-# INLINE split_pi_tys' #-}

-- | Like 'tyConBindersTyCoBinders' but you also get a 'Bool' which is true iff
-- there is at least one named binder.
ty_con_binders_ty_binders' :: [TyConBinder] -> ([TyCoBinder], Bool)
ty_con_binders_ty_binders' :: [TyConBinder] -> ([TyCoBinder], Bool)
ty_con_binders_ty_binders' = (TyConBinder -> ([TyCoBinder], Bool) -> ([TyCoBinder], Bool))
-> ([TyCoBinder], Bool) -> [TyConBinder] -> ([TyCoBinder], Bool)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TyConBinder -> ([TyCoBinder], Bool) -> ([TyCoBinder], Bool)
go ([], Bool
False)
  where
    go :: TyConBinder -> ([TyCoBinder], Bool) -> ([TyCoBinder], Bool)
go (Bndr Var
tv (NamedTCB ArgFlag
vis)) ([TyCoBinder]
bndrs, Bool
_)
      = (TyVarBinder -> TyCoBinder
Named (Var -> ArgFlag -> TyVarBinder
forall var argf. var -> argf -> VarBndr var argf
Bndr Var
tv ArgFlag
vis) TyCoBinder -> [TyCoBinder] -> [TyCoBinder]
forall a. a -> [a] -> [a]
: [TyCoBinder]
bndrs, Bool
True)
    go (Bndr Var
tv (AnonTCB AnonArgFlag
af))   ([TyCoBinder]
bndrs, Bool
n)
      = (AnonArgFlag -> Scaled Type -> TyCoBinder
Anon AnonArgFlag
af (Type -> Scaled Type
forall a. a -> Scaled a
tymult (Var -> Type
tyVarKind Var
tv)) TyCoBinder -> [TyCoBinder] -> [TyCoBinder]
forall a. a -> [a] -> [a]
: [TyCoBinder]
bndrs, Bool
n)
    {-# INLINE go #-}
{-# INLINE ty_con_binders_ty_binders' #-}