{-# LANGUAGE BangPatterns  #-}
{-# LANGUAGE CPP           #-}
{-# LANGUAGE DeriveFunctor #-}

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

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

#include "HsVersions.h"

import GHC.Prelude

import GHC.Core.TyCo.Ppr ( pprTyVar )
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.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.Tc.Solver.Monad as TcS

import GHC.Utils.Misc
import GHC.Data.Maybe
import GHC.Exts (oneShot)
import Control.Monad
import GHC.Utils.Monad ( zipWith3M )
import Data.List.NonEmpty ( NonEmpty(..) )

import Control.Arrow ( first )

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

data RewriteEnv
  = FE { RewriteEnv -> CtLoc
fe_loc     :: !CtLoc             -- See Note [Rewriter CtLoc]
       , RewriteEnv -> CtFlavour
fe_flavour :: !CtFlavour
       , RewriteEnv -> EqRel
fe_eq_rel  :: !EqRel             -- See Note [Rewriter EqRels]
       }

-- | The 'RewriteM' monad is a wrapper around 'TcS' with a 'RewriteEnv'
newtype RewriteM a
  = RewriteM { forall a. RewriteM a -> RewriteEnv -> TcS a
runRewriteM :: RewriteEnv -> TcS a }
  deriving ((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
<$ :: forall a b. a -> RewriteM b -> RewriteM a
$c<$ :: forall a b. a -> RewriteM b -> RewriteM a
fmap :: forall a b. (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 :: forall a. (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 >>= :: forall a b. 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 :: forall a. 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
  <*> :: forall a b. 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 :: forall a. 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
runRewriteCtEv :: forall a. CtEvidence -> RewriteM a -> TcS a
runRewriteCtEv CtEvidence
ev
  = CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS a
forall a. CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS a
runRewrite (CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev) (CtEvidence -> CtFlavour
ctEvFlavour CtEvidence
ev) (CtEvidence -> EqRel
ctEvEqRel CtEvidence
ev)

-- Run thing_inside (which does the rewriting)
runRewrite :: CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS a
runRewrite :: forall a. CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS a
runRewrite CtLoc
loc CtFlavour
flav EqRel
eq_rel RewriteM a
thing_inside
  = RewriteM a -> RewriteEnv -> TcS a
forall a. RewriteM a -> RewriteEnv -> TcS a
runRewriteM RewriteM a
thing_inside RewriteEnv
fmode
  where
    fmode :: RewriteEnv
fmode = FE { fe_loc :: CtLoc
fe_loc  = CtLoc
loc
               , fe_flavour :: CtFlavour
fe_flavour = CtFlavour
flav
               , fe_eq_rel :: EqRel
fe_eq_rel = EqRel
eq_rel }

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]

getRewriteEnvField :: (RewriteEnv -> a) -> RewriteM a
getRewriteEnvField :: forall a. (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
fe_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
fe_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
fe_loc

checkStackDepth :: Type -> RewriteM ()
checkStackDepth :: Xi -> RewriteM ()
checkStackDepth Xi
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 -> Xi -> TcS ()
checkReductionDepth CtLoc
loc Xi
ty }

-- | Change the 'EqRel' in a 'RewriteM'.
setEqRel :: EqRel -> RewriteM a -> RewriteM a
setEqRel :: forall a. 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
fe_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 { fe_eq_rel :: EqRel
fe_eq_rel = EqRel
new_eq_rel })
{-# INLINE setEqRel #-}

-- | Make sure that rewriting actually produces a coercion (in other
-- words, make sure our flavour is not Derived)
-- Note [No derived kind equalities]
noBogusCoercions :: RewriteM a -> RewriteM a
noBogusCoercions :: forall a. RewriteM a -> RewriteM a
noBogusCoercions 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 ->
    -- No new thunk is made if the flavour hasn't changed (note the bang).
    let !env' :: RewriteEnv
env' = case RewriteEnv -> CtFlavour
fe_flavour RewriteEnv
env of
          CtFlavour
Derived -> RewriteEnv
env { fe_flavour :: CtFlavour
fe_flavour = ShadowInfo -> CtFlavour
Wanted ShadowInfo
WDeriv }
          CtFlavour
_       -> RewriteEnv
env
    in
    RewriteM a -> RewriteEnv -> TcS a
forall a. RewriteM a -> RewriteEnv -> TcS a
runRewriteM RewriteM a
thing_inside RewriteEnv
env'

bumpDepth :: RewriteM a -> RewriteM a
bumpDepth :: forall a. 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 { fe_loc :: CtLoc
fe_loc = CtLoc -> CtLoc
bumpCtLocDepth (RewriteEnv -> CtLoc
fe_loc RewriteEnv
env) }
      ; RewriteEnv -> TcS a
thing_inside RewriteEnv
env' }

{-
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 fe_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.)

Note [No derived kind equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
A kind-level coercion can appear in types, via mkCastTy. So, whenever
we are generating a coercion in a dependent context (in other words,
in a kind) we need to make sure that our flavour is never Derived
(as Derived constraints have no evidence). The noBogusCoercions function
changes the flavour from Derived just for this purpose.

-}

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

-- | See Note [Rewriting].
-- If (xi, co) <- rewrite mode ev ty, then co :: xi ~r ty
-- where r is the role in @ev@.
rewrite :: CtEvidence -> TcType
        -> TcS (Xi, TcCoercion)
rewrite :: CtEvidence -> Xi -> TcS (Xi, TcCoercionN)
rewrite CtEvidence
ev Xi
ty
  = do { String -> SDoc -> TcS ()
traceTcS String
"rewrite {" (Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr Xi
ty)
       ; (Xi
ty', TcCoercionN
co) <- CtEvidence -> RewriteM (Xi, TcCoercionN) -> TcS (Xi, TcCoercionN)
forall a. CtEvidence -> RewriteM a -> TcS a
runRewriteCtEv CtEvidence
ev (Xi -> RewriteM (Xi, TcCoercionN)
rewrite_one Xi
ty)
       ; String -> SDoc -> TcS ()
traceTcS String
"rewrite }" (Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr Xi
ty')
       ; (Xi, TcCoercionN) -> TcS (Xi, TcCoercionN)
forall (m :: * -> *) a. Monad m => a -> m a
return (Xi
ty', TcCoercionN
co) }

-- specialized to rewriting kinds: never Derived, always Nominal
-- See Note [No derived kind equalities]
-- See Note [Rewriting]
rewriteKind :: CtLoc -> CtFlavour -> TcType -> TcS (Xi, TcCoercionN)
rewriteKind :: CtLoc -> CtFlavour -> Xi -> TcS (Xi, TcCoercionN)
rewriteKind CtLoc
loc CtFlavour
flav Xi
ty
  = do { String -> SDoc -> TcS ()
traceTcS String
"rewriteKind {" (CtFlavour -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtFlavour
flav SDoc -> SDoc -> SDoc
<+> Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr Xi
ty)
       ; let flav' :: CtFlavour
flav' = case CtFlavour
flav of
                       CtFlavour
Derived -> ShadowInfo -> CtFlavour
Wanted ShadowInfo
WDeriv  -- the WDeriv/WOnly choice matters not
                       CtFlavour
_       -> CtFlavour
flav
       ; (Xi
ty', TcCoercionN
co) <- CtLoc
-> CtFlavour
-> EqRel
-> RewriteM (Xi, TcCoercionN)
-> TcS (Xi, TcCoercionN)
forall a. CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS a
runRewrite CtLoc
loc CtFlavour
flav' EqRel
NomEq (Xi -> RewriteM (Xi, TcCoercionN)
rewrite_one Xi
ty)
       ; String -> SDoc -> TcS ()
traceTcS String
"rewriteKind }" (Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr Xi
ty' SDoc -> SDoc -> SDoc
$$ TcCoercionN -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcCoercionN
co) -- co is never a panic
       ; (Xi, TcCoercionN) -> TcS (Xi, TcCoercionN)
forall (m :: * -> *) a. Monad m => a -> m a
return (Xi
ty', TcCoercionN
co) }

-- See Note [Rewriting]
rewriteArgsNom :: CtEvidence -> TyCon -> [TcType] -> TcS ([Xi], [TcCoercion])
-- 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)
--
-- For Derived constraints the returned coercion may be undefined
-- because rewriting may use a Derived equality ([D] a ~ ty)
rewriteArgsNom :: CtEvidence -> TyCon -> [Xi] -> TcS ([Xi], [TcCoercionN])
rewriteArgsNom CtEvidence
ev TyCon
tc [Xi]
tys
  = do { String -> SDoc -> TcS ()
traceTcS String
"rewrite_args {" ([SDoc] -> SDoc
vcat ((Xi -> SDoc) -> [Xi] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Xi]
tys))
       ; ([Xi]
tys', [TcCoercionN]
cos, MCoercionN
kind_co)
           <- CtEvidence
-> RewriteM ([Xi], [TcCoercionN], MCoercionN)
-> TcS ([Xi], [TcCoercionN], MCoercionN)
forall a. CtEvidence -> RewriteM a -> TcS a
runRewriteCtEv CtEvidence
ev (TyCon
-> Maybe [Role]
-> [Xi]
-> RewriteM ([Xi], [TcCoercionN], MCoercionN)
rewrite_args_tc TyCon
tc Maybe [Role]
forall a. Maybe a
Nothing [Xi]
tys)
       ; MASSERT( isReflMCo kind_co )
       ; String -> SDoc -> TcS ()
traceTcS String
"rewrite }" ([SDoc] -> SDoc
vcat ((Xi -> SDoc) -> [Xi] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Xi]
tys'))
       ; ([Xi], [TcCoercionN]) -> TcS ([Xi], [TcCoercionN])
forall (m :: * -> *) a. Monad m => a -> m a
return ([Xi]
tys', [TcCoercionN]
cos) }

-- | 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 -> Xi -> TcS Xi
rewriteType CtLoc
loc Xi
ty
  = do { (Xi
xi, TcCoercionN
_) <- CtLoc
-> CtFlavour
-> EqRel
-> RewriteM (Xi, TcCoercionN)
-> TcS (Xi, TcCoercionN)
forall a. CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS a
runRewrite CtLoc
loc CtFlavour
Given EqRel
NomEq (RewriteM (Xi, TcCoercionN) -> TcS (Xi, TcCoercionN))
-> RewriteM (Xi, TcCoercionN) -> TcS (Xi, TcCoercionN)
forall a b. (a -> b) -> a -> b
$
                    Xi -> RewriteM (Xi, TcCoercionN)
rewrite_one Xi
ty
                     -- use Given flavor so that it is rewritten
                     -- only w.r.t. Givens, never Wanteds/Deriveds
                     -- (Shouldn't matter, if only Givens are present
                     -- anyway)
       ; Xi -> TcS Xi
forall (m :: * -> *) a. Monad m => a -> m a
return Xi
xi }

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

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

Key invariants:
  (F0) co :: xi ~ zonk(ty')    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 :: xi ~ ty) isn't quite true. So, instead,
we can rely on this fact:

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

Note that the left-hand type of co is *always* precisely xi. The right-hand
type may or may not be ty, however: if ty has unzonked filled-in metavariables,
then the right-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 :: xi ~ ty) 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) tcTypeKind(xi) `eqType` zonk(tcTypeKind(ty))

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.Monad.

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]        -- Arg types [t1,..,tn]
  -> RewriteM ( [Xi]  -- List of rewritten args [x1,..,xn]
                   -- 1-1 corresp with [t1,..,tn]
           , [Coercion]  -- List of arg coercions [co1,..,con]
                         -- 1-1 corresp with [t1,..,tn]
                         --    coi :: xi ~r ti
           , MCoercionN) -- Result coercion, rco
                         --    rco : (T t1..tn) ~N (T (x1 |> co1) .. (xn |> con))
rewrite_args_tc :: TyCon
-> Maybe [Role]
-> [Xi]
-> RewriteM ([Xi], [TcCoercionN], MCoercionN)
rewrite_args_tc TyCon
tc = [TyCoBinder]
-> Bool
-> Xi
-> TcTyCoVarSet
-> Maybe [Role]
-> [Xi]
-> RewriteM ([Xi], [TcCoercionN], MCoercionN)
rewrite_args [TyCoBinder]
all_bndrs Bool
any_named_bndrs Xi
inner_ki TcTyCoVarSet
emptyVarSet
  -- NB: TyCon kinds are always closed
  where
    ([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, Xi
inner_ki, Bool
inner_named) = Xi -> ([TyCoBinder], Xi, Bool)
split_pi_tys' (TyCon -> Xi
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 ([Xi], [Coercion], MCoercionN)
-- Coercions :: Xi ~ Type, at roles given
-- Third coercion :: tcTypeKind(fun xis) ~N tcTypeKind(fun tys)
-- That is, the third coercion relates the kind of some function (whose kind is
-- passed as the first parameter) instantiated at xis to the kind of that
-- function instantiated at the tys. This is useful in keeping rewriting
-- homoegeneous. The list of roles must be at least as long as the list of
-- types.
rewrite_args :: [TyCoBinder]
-> Bool
-> Xi
-> TcTyCoVarSet
-> Maybe [Role]
-> [Xi]
-> RewriteM ([Xi], [TcCoercionN], MCoercionN)
rewrite_args [TyCoBinder]
orig_binders
             Bool
any_named_bndrs
             Xi
orig_inner_ki
             TcTyCoVarSet
orig_fvs
             Maybe [Role]
orig_m_roles
             [Xi]
orig_tys
  = case (Maybe [Role]
orig_m_roles, Bool
any_named_bndrs) of
      (Maybe [Role]
Nothing, Bool
False) -> [Xi] -> RewriteM ([Xi], [TcCoercionN], MCoercionN)
rewrite_args_fast [Xi]
orig_tys
      (Maybe [Role], Bool)
_ -> [TyCoBinder]
-> Xi
-> TcTyCoVarSet
-> [Role]
-> [Xi]
-> RewriteM ([Xi], [TcCoercionN], MCoercionN)
rewrite_args_slow [TyCoBinder]
orig_binders Xi
orig_inner_ki TcTyCoVarSet
orig_fvs [Role]
orig_roles [Xi]
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.
-- 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.
rewrite_args_fast :: [Type]
                  -> RewriteM ([Xi], [Coercion], MCoercionN)
rewrite_args_fast :: [Xi] -> RewriteM ([Xi], [TcCoercionN], MCoercionN)
rewrite_args_fast [Xi]
orig_tys
  = (([Xi], [TcCoercionN]) -> ([Xi], [TcCoercionN], MCoercionN))
-> RewriteM ([Xi], [TcCoercionN])
-> RewriteM ([Xi], [TcCoercionN], MCoercionN)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Xi], [TcCoercionN]) -> ([Xi], [TcCoercionN], MCoercionN)
finish ([Xi] -> RewriteM ([Xi], [TcCoercionN])
iterate [Xi]
orig_tys)
  where

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

    {-# INLINE finish #-}
    finish :: ([Xi], [Coercion]) -> ([Xi], [Coercion], MCoercionN)
    finish :: ([Xi], [TcCoercionN]) -> ([Xi], [TcCoercionN], MCoercionN)
finish ([Xi]
xis, [TcCoercionN]
cos) = ([Xi]
xis, [TcCoercionN]
cos, 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 ([Xi], [Coercion], MCoercionN)
rewrite_args_slow :: [TyCoBinder]
-> Xi
-> TcTyCoVarSet
-> [Role]
-> [Xi]
-> RewriteM ([Xi], [TcCoercionN], MCoercionN)
rewrite_args_slow [TyCoBinder]
binders Xi
inner_ki TcTyCoVarSet
fvs [Role]
roles [Xi]
tys
-- Arguments used dependently must be rewritten with proper coercions, but
-- we're not guaranteed to get a proper coercion when rewriting with the
-- "Derived" flavour. So we must call noBogusCoercions when rewriting arguments
-- corresponding to binders that are dependent. However, we might legitimately
-- have *more* arguments than binders, in the case that the inner_ki is a variable
-- that gets instantiated with a Π-type. We conservatively choose not to produce
-- bogus coercions for these, too. Note that this might miss an opportunity for
-- a Derived rewriting a Derived. The solution would be to generate evidence for
-- Deriveds, thus avoiding this whole noBogusCoercions idea. See also
-- Note [No derived kind equalities]
  = do { [(Xi, TcCoercionN)]
rewritten_args <- (Bool -> Role -> Xi -> RewriteM (Xi, TcCoercionN))
-> [Bool] -> [Role] -> [Xi] -> RewriteM [(Xi, TcCoercionN)]
forall (m :: * -> *) a b c d.
Monad m =>
(a -> b -> c -> m d) -> [a] -> [b] -> [c] -> m [d]
zipWith3M Bool -> Role -> Xi -> RewriteM (Xi, TcCoercionN)
fl ((TyCoBinder -> Bool) -> [TyCoBinder] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map TyCoBinder -> Bool
isNamedBinder [TyCoBinder]
binders [Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++ Bool -> [Bool]
forall a. a -> [a]
repeat Bool
True)
                                        [Role]
roles [Xi]
tys
       ; ([Xi], [TcCoercionN], MCoercionN)
-> RewriteM ([Xi], [TcCoercionN], MCoercionN)
forall (m :: * -> *) a. Monad m => a -> m a
return ([TyCoBinder]
-> Xi
-> TcTyCoVarSet
-> [Role]
-> [(Xi, TcCoercionN)]
-> ([Xi], [TcCoercionN], MCoercionN)
simplifyArgsWorker [TyCoBinder]
binders Xi
inner_ki TcTyCoVarSet
fvs [Role]
roles [(Xi, TcCoercionN)]
rewritten_args) }
  where
    {-# INLINE fl #-}
    fl :: Bool   -- must we ensure to produce a real coercion here?
                  -- see comment at top of function
       -> Role -> Type -> RewriteM (Xi, Coercion)
    fl :: Bool -> Role -> Xi -> RewriteM (Xi, TcCoercionN)
fl Bool
True  Role
r Xi
ty = RewriteM (Xi, TcCoercionN) -> RewriteM (Xi, TcCoercionN)
forall a. RewriteM a -> RewriteM a
noBogusCoercions (RewriteM (Xi, TcCoercionN) -> RewriteM (Xi, TcCoercionN))
-> RewriteM (Xi, TcCoercionN) -> RewriteM (Xi, TcCoercionN)
forall a b. (a -> b) -> a -> b
$ Role -> Xi -> RewriteM (Xi, TcCoercionN)
fl1 Role
r Xi
ty
    fl Bool
False Role
r Xi
ty =                    Role -> Xi -> RewriteM (Xi, TcCoercionN)
fl1 Role
r Xi
ty

    {-# INLINE fl1 #-}
    fl1 :: Role -> Type -> RewriteM (Xi, Coercion)
    fl1 :: Role -> Xi -> RewriteM (Xi, TcCoercionN)
fl1 Role
Nominal Xi
ty
      = EqRel -> RewriteM (Xi, TcCoercionN) -> RewriteM (Xi, TcCoercionN)
forall a. EqRel -> RewriteM a -> RewriteM a
setEqRel EqRel
NomEq (RewriteM (Xi, TcCoercionN) -> RewriteM (Xi, TcCoercionN))
-> RewriteM (Xi, TcCoercionN) -> RewriteM (Xi, TcCoercionN)
forall a b. (a -> b) -> a -> b
$
        Xi -> RewriteM (Xi, TcCoercionN)
rewrite_one Xi
ty

    fl1 Role
Representational Xi
ty
      = EqRel -> RewriteM (Xi, TcCoercionN) -> RewriteM (Xi, TcCoercionN)
forall a. EqRel -> RewriteM a -> RewriteM a
setEqRel EqRel
ReprEq (RewriteM (Xi, TcCoercionN) -> RewriteM (Xi, TcCoercionN))
-> RewriteM (Xi, TcCoercionN) -> RewriteM (Xi, TcCoercionN)
forall a b. (a -> b) -> a -> b
$
        Xi -> RewriteM (Xi, TcCoercionN)
rewrite_one Xi
ty

    fl1 Role
Phantom Xi
ty
    -- See Note [Phantoms in the rewriter]
      = do { Xi
ty <- TcS Xi -> RewriteM Xi
forall a. TcS a -> RewriteM a
liftTcS (TcS Xi -> RewriteM Xi) -> TcS Xi -> RewriteM Xi
forall a b. (a -> b) -> a -> b
$ Xi -> TcS Xi
zonkTcType Xi
ty
           ; (Xi, TcCoercionN) -> RewriteM (Xi, TcCoercionN)
forall (m :: * -> *) a. Monad m => a -> m a
return (Xi
ty, Role -> Xi -> TcCoercionN
mkReflCo Role
Phantom Xi
ty) }

------------------
rewrite_one :: TcType -> RewriteM (Xi, Coercion)
-- 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: Coercion :: Xi ~ TcType
-- The role on the result coercion matches the EqRel in the RewriteEnv

rewrite_one :: Xi -> RewriteM (Xi, TcCoercionN)
rewrite_one Xi
ty
  | Just Xi
ty' <- Xi -> Maybe Xi
rewriterView Xi
ty  -- See Note [Rewriting synonyms]
  = Xi -> RewriteM (Xi, TcCoercionN)
rewrite_one Xi
ty'

rewrite_one xi :: Xi
xi@(LitTy {})
  = do { Role
role <- RewriteM Role
getRole
       ; (Xi, TcCoercionN) -> RewriteM (Xi, TcCoercionN)
forall (m :: * -> *) a. Monad m => a -> m a
return (Xi
xi, Role -> Xi -> TcCoercionN
mkReflCo Role
role Xi
xi) }

rewrite_one (TyVarTy TcTyVar
tv)
  = TcTyVar -> RewriteM (Xi, TcCoercionN)
rewriteTyVar TcTyVar
tv

rewrite_one (AppTy Xi
ty1 Xi
ty2)
  = Xi -> [Xi] -> RewriteM (Xi, TcCoercionN)
rewrite_app_tys Xi
ty1 [Xi
ty2]

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

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

rewrite_one ty :: Xi
ty@(FunTy { ft_mult :: Xi -> Xi
ft_mult = Xi
mult, ft_arg :: Xi -> Xi
ft_arg = Xi
ty1, ft_res :: Xi -> Xi
ft_res = Xi
ty2 })
  = do { (Xi
xi1,TcCoercionN
co1) <- Xi -> RewriteM (Xi, TcCoercionN)
rewrite_one Xi
ty1
       ; (Xi
xi2,TcCoercionN
co2) <- Xi -> RewriteM (Xi, TcCoercionN)
rewrite_one Xi
ty2
       ; (Xi
xi3,TcCoercionN
co3) <- EqRel -> RewriteM (Xi, TcCoercionN) -> RewriteM (Xi, TcCoercionN)
forall a. EqRel -> RewriteM a -> RewriteM a
setEqRel EqRel
NomEq (RewriteM (Xi, TcCoercionN) -> RewriteM (Xi, TcCoercionN))
-> RewriteM (Xi, TcCoercionN) -> RewriteM (Xi, TcCoercionN)
forall a b. (a -> b) -> a -> b
$ Xi -> RewriteM (Xi, TcCoercionN)
rewrite_one Xi
mult
       ; Role
role <- RewriteM Role
getRole
       ; (Xi, TcCoercionN) -> RewriteM (Xi, TcCoercionN)
forall (m :: * -> *) a. Monad m => a -> m a
return (Xi
ty { ft_mult :: Xi
ft_mult = Xi
xi3, ft_arg :: Xi
ft_arg = Xi
xi1, ft_res :: Xi
ft_res = Xi
xi2 }
                , Role -> TcCoercionN -> TcCoercionN -> TcCoercionN -> TcCoercionN
mkFunCo Role
role TcCoercionN
co3 TcCoercionN
co1 TcCoercionN
co2) }

rewrite_one ty :: Xi
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, Xi
rho) = Xi -> ([TyVarBinder], Xi)
tcSplitForAllTyVarBinders Xi
ty
             tvs :: [TcTyVar]
tvs           = [TyVarBinder] -> [TcTyVar]
forall tv argf. [VarBndr tv argf] -> [tv]
binderVars [TyVarBinder]
bndrs
       ; (Xi
rho', TcCoercionN
co) <- Xi -> RewriteM (Xi, TcCoercionN)
rewrite_one Xi
rho
       ; (Xi, TcCoercionN) -> RewriteM (Xi, TcCoercionN)
forall (m :: * -> *) a. Monad m => a -> m a
return ([TyVarBinder] -> Xi -> Xi
mkForAllTys [TyVarBinder]
bndrs Xi
rho', [TcTyVar] -> TcCoercionN -> TcCoercionN
mkHomoForAllCos [TcTyVar]
tvs TcCoercionN
co) }

rewrite_one (CastTy Xi
ty TcCoercionN
g)
  = do { (Xi
xi, TcCoercionN
co) <- Xi -> RewriteM (Xi, TcCoercionN)
rewrite_one Xi
ty
       ; (TcCoercionN
g', TcCoercionN
_)  <- TcCoercionN -> RewriteM (TcCoercionN, TcCoercionN)
rewrite_co TcCoercionN
g
       ; Role
role <- RewriteM Role
getRole
       ; (Xi, TcCoercionN) -> RewriteM (Xi, TcCoercionN)
forall (m :: * -> *) a. Monad m => a -> m a
return (Xi -> TcCoercionN -> Xi
mkCastTy Xi
xi TcCoercionN
g', TcCoercionN -> Role -> Xi -> Xi -> TcCoercionN -> TcCoercionN
castCoercionKind1 TcCoercionN
co Role
role Xi
xi Xi
ty TcCoercionN
g') }
         -- It makes a /big/ difference to call castCoercionKind1 not
         -- the more general castCoercionKind2.
         -- See Note [castCoercionKind1] in GHC.Core.Coercion

rewrite_one (CoercionTy TcCoercionN
co) = (TcCoercionN -> Xi)
-> (TcCoercionN, TcCoercionN) -> (Xi, TcCoercionN)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first TcCoercionN -> Xi
mkCoercionTy ((TcCoercionN, TcCoercionN) -> (Xi, TcCoercionN))
-> RewriteM (TcCoercionN, TcCoercionN)
-> RewriteM (Xi, TcCoercionN)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcCoercionN -> RewriteM (TcCoercionN, TcCoercionN)
rewrite_co TcCoercionN
co

-- | "Rewrite" a coercion. Really, just zonk it so we can uphold
-- (F1) of Note [Rewriting]
rewrite_co :: Coercion -> RewriteM (Coercion, Coercion)
rewrite_co :: TcCoercionN -> RewriteM (TcCoercionN, TcCoercionN)
rewrite_co TcCoercionN
co
  = do { TcCoercionN
co <- TcS TcCoercionN -> RewriteM TcCoercionN
forall a. TcS a -> RewriteM a
liftTcS (TcS TcCoercionN -> RewriteM TcCoercionN)
-> TcS TcCoercionN -> RewriteM TcCoercionN
forall a b. (a -> b) -> a -> b
$ TcCoercionN -> TcS TcCoercionN
zonkCo TcCoercionN
co
       ; Role
env_role <- RewriteM Role
getRole
       ; let co' :: TcCoercionN
co' = Role -> Xi -> TcCoercionN
mkTcReflCo Role
env_role (TcCoercionN -> Xi
mkCoercionTy TcCoercionN
co)
       ; (TcCoercionN, TcCoercionN) -> RewriteM (TcCoercionN, TcCoercionN)
forall (m :: * -> *) a. Monad m => a -> m a
return (TcCoercionN
co, TcCoercionN
co') }

-- rewrite (nested) AppTys
rewrite_app_tys :: Type -> [Type] -> RewriteM (Xi, Coercion)
-- 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 :: Xi -> [Xi] -> RewriteM (Xi, TcCoercionN)
rewrite_app_tys (AppTy Xi
ty1 Xi
ty2) [Xi]
tys = Xi -> [Xi] -> RewriteM (Xi, TcCoercionN)
rewrite_app_tys Xi
ty1 (Xi
ty2Xi -> [Xi] -> [Xi]
forall a. a -> [a] -> [a]
:[Xi]
tys)
rewrite_app_tys Xi
fun_ty [Xi]
arg_tys
  = do { (Xi
fun_xi, TcCoercionN
fun_co) <- Xi -> RewriteM (Xi, TcCoercionN)
rewrite_one Xi
fun_ty
       ; Xi -> TcCoercionN -> [Xi] -> RewriteM (Xi, TcCoercionN)
rewrite_app_ty_args Xi
fun_xi TcCoercionN
fun_co [Xi]
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 regeressions in allocations.
rewrite_app_ty_args :: Xi -> Coercion -> [Type] -> RewriteM (Xi, Coercion)
rewrite_app_ty_args :: Xi -> TcCoercionN -> [Xi] -> RewriteM (Xi, TcCoercionN)
rewrite_app_ty_args Xi
fun_xi TcCoercionN
fun_co []
  -- this will be a common case when called from rewrite_fam_app, so shortcut
  = (Xi, TcCoercionN) -> RewriteM (Xi, TcCoercionN)
forall (m :: * -> *) a. Monad m => a -> m a
return (Xi
fun_xi, TcCoercionN
fun_co)
rewrite_app_ty_args Xi
fun_xi TcCoercionN
fun_co [Xi]
arg_tys
  = do { (Xi
xi, TcCoercionN
co, MCoercionN
kind_co) <- case HasCallStack => Xi -> Maybe (TyCon, [Xi])
Xi -> Maybe (TyCon, [Xi])
tcSplitTyConApp_maybe Xi
fun_xi of
           Just (TyCon
tc, [Xi]
xis) ->
             do { let tc_roles :: [Role]
tc_roles  = TyCon -> [Role]
tyConRolesRepresentational TyCon
tc
                      arg_roles :: [Role]
arg_roles = [Xi] -> [Role] -> [Role]
forall b a. [b] -> [a] -> [a]
dropList [Xi]
xis [Role]
tc_roles
                ; ([Xi]
arg_xis, [TcCoercionN]
arg_cos, MCoercionN
kind_co)
                    <- Xi -> [Role] -> [Xi] -> RewriteM ([Xi], [TcCoercionN], MCoercionN)
rewrite_vector (HasDebugCallStack => Xi -> Xi
Xi -> Xi
tcTypeKind Xi
fun_xi) [Role]
arg_roles [Xi]
arg_tys

                  -- Here, we have fun_co :: T xi1 xi2 ~ ty
                  -- and 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:
                  -- T <xi1> <xi2> arg_cos ;; fun_co <arg_tys>
                ; EqRel
eq_rel <- RewriteM EqRel
getEqRel
                ; let app_xi :: Xi
app_xi = TyCon -> [Xi] -> Xi
mkTyConApp TyCon
tc ([Xi]
xis [Xi] -> [Xi] -> [Xi]
forall a. [a] -> [a] -> [a]
++ [Xi]
arg_xis)
                      app_co :: TcCoercionN
app_co = case EqRel
eq_rel of
                        EqRel
NomEq  -> TcCoercionN -> [TcCoercionN] -> TcCoercionN
mkAppCos TcCoercionN
fun_co [TcCoercionN]
arg_cos
                        EqRel
ReprEq -> Role -> TyCon -> [TcCoercionN] -> TcCoercionN
mkTcTyConAppCo Role
Representational TyCon
tc
                                    ((Role -> Xi -> TcCoercionN) -> [Role] -> [Xi] -> [TcCoercionN]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Role -> Xi -> TcCoercionN
mkReflCo [Role]
tc_roles [Xi]
xis [TcCoercionN] -> [TcCoercionN] -> [TcCoercionN]
forall a. [a] -> [a] -> [a]
++ [TcCoercionN]
arg_cos)
                                  TcCoercionN -> TcCoercionN -> TcCoercionN
`mkTcTransCo`
                                  TcCoercionN -> [TcCoercionN] -> TcCoercionN
mkAppCos TcCoercionN
fun_co ((Xi -> TcCoercionN) -> [Xi] -> [TcCoercionN]
forall a b. (a -> b) -> [a] -> [b]
map Xi -> TcCoercionN
mkNomReflCo [Xi]
arg_tys)
                ; (Xi, TcCoercionN, MCoercionN)
-> RewriteM (Xi, TcCoercionN, MCoercionN)
forall (m :: * -> *) a. Monad m => a -> m a
return (Xi
app_xi, TcCoercionN
app_co, MCoercionN
kind_co) }
           Maybe (TyCon, [Xi])
Nothing ->
             do { ([Xi]
arg_xis, [TcCoercionN]
arg_cos, MCoercionN
kind_co)
                    <- Xi -> [Role] -> [Xi] -> RewriteM ([Xi], [TcCoercionN], MCoercionN)
rewrite_vector (HasDebugCallStack => Xi -> Xi
Xi -> Xi
tcTypeKind Xi
fun_xi) (Role -> [Role]
forall a. a -> [a]
repeat Role
Nominal) [Xi]
arg_tys
                ; let arg_xi :: Xi
arg_xi = Xi -> [Xi] -> Xi
mkAppTys Xi
fun_xi [Xi]
arg_xis
                      arg_co :: TcCoercionN
arg_co = TcCoercionN -> [TcCoercionN] -> TcCoercionN
mkAppCos TcCoercionN
fun_co [TcCoercionN]
arg_cos
                ; (Xi, TcCoercionN, MCoercionN)
-> RewriteM (Xi, TcCoercionN, MCoercionN)
forall (m :: * -> *) a. Monad m => a -> m a
return (Xi
arg_xi, TcCoercionN
arg_co, MCoercionN
kind_co) }

       ; Role
role <- RewriteM Role
getRole
       ; (Xi, TcCoercionN) -> RewriteM (Xi, TcCoercionN)
forall (m :: * -> *) a. Monad m => a -> m a
return (Xi -> TcCoercionN -> Role -> MCoercionN -> (Xi, TcCoercionN)
homogenise_result Xi
xi TcCoercionN
co Role
role MCoercionN
kind_co) }

rewrite_ty_con_app :: TyCon -> [TcType] -> RewriteM (Xi, Coercion)
rewrite_ty_con_app :: TyCon -> [Xi] -> RewriteM (Xi, TcCoercionN)
rewrite_ty_con_app TyCon
tc [Xi]
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
       ; ([Xi]
xis, [TcCoercionN]
cos, MCoercionN
kind_co) <- TyCon
-> Maybe [Role]
-> [Xi]
-> RewriteM ([Xi], [TcCoercionN], MCoercionN)
rewrite_args_tc TyCon
tc Maybe [Role]
m_roles [Xi]
tys
       ; let tyconapp_xi :: Xi
tyconapp_xi = TyCon -> [Xi] -> Xi
mkTyConApp TyCon
tc [Xi]
xis
             tyconapp_co :: TcCoercionN
tyconapp_co = HasDebugCallStack => Role -> TyCon -> [TcCoercionN] -> TcCoercionN
Role -> TyCon -> [TcCoercionN] -> TcCoercionN
mkTyConAppCo Role
role TyCon
tc [TcCoercionN]
cos
       ; (Xi, TcCoercionN) -> RewriteM (Xi, TcCoercionN)
forall (m :: * -> *) a. Monad m => a -> m a
return (Xi -> TcCoercionN -> Role -> MCoercionN -> (Xi, TcCoercionN)
homogenise_result Xi
tyconapp_xi TcCoercionN
tyconapp_co Role
role MCoercionN
kind_co) }

-- Make the result of rewriting homogeneous (Note [Rewriting] (F2))
homogenise_result :: Xi              -- a rewritten type
                  -> Coercion        -- :: xi ~r original ty
                  -> Role            -- r
                  -> MCoercionN      -- kind_co :: tcTypeKind(xi) ~N tcTypeKind(ty)
                  -> (Xi, Coercion)  -- (xi |> kind_co, (xi |> kind_co)
                                     --   ~r original ty)
homogenise_result :: Xi -> TcCoercionN -> Role -> MCoercionN -> (Xi, TcCoercionN)
homogenise_result Xi
xi TcCoercionN
co Role
_ MCoercionN
MRefl = (Xi
xi, TcCoercionN
co)
homogenise_result Xi
xi TcCoercionN
co Role
r mco :: MCoercionN
mco@(MCo TcCoercionN
kind_co)
  = (Xi
xi Xi -> TcCoercionN -> Xi
`mkCastTy` TcCoercionN
kind_co, (TcCoercionN -> TcCoercionN
mkSymCo (TcCoercionN -> TcCoercionN) -> TcCoercionN -> TcCoercionN
forall a b. (a -> b) -> a -> b
$ Role -> Xi -> MCoercionN -> TcCoercionN
GRefl Role
r Xi
xi MCoercionN
mco) TcCoercionN -> TcCoercionN -> TcCoercionN
`mkTransCo` TcCoercionN
co)
{-# INLINE homogenise_result #-}

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

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

STEP 2. Try top-level instances. Note that 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 3. Rewrite all arguments. This might expose more information so that we
  can use a top-level instance.

  Continue to the next step.

STEP 4. 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.

STEP 5. Try the famapp-cache again. Now that we've revealed more information
  in the arguments, the cache might be helpful.

  If we get a cache hit, jump to FINISH.

STEP 6. Try top-level instances, which might trigger now that we know more
  about the argumnents.

  If an instance is found, jump to FINISH.

STEP 7. No progress to be made. Return what we have. (Do not do 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/2 and STEP 5/6 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/2. So `finish`
is inlined in that case, and only FINISH 1 is performed.

-}

rewrite_fam_app :: TyCon -> [TcType] -> RewriteM (Xi, Coercion)
  --   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 -> [Xi] -> RewriteM (Xi, TcCoercionN)
rewrite_fam_app TyCon
tc [Xi]
tys  -- Can be over-saturated
    = ASSERT2( tys `lengthAtLeast` tyConArity tc
             , ppr tc $$ ppr (tyConArity tc) $$ ppr tys)

                 -- 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 ([Xi]
tys1, [Xi]
tys_rest) = Arity -> [Xi] -> ([Xi], [Xi])
forall a. Arity -> [a] -> ([a], [a])
splitAt (TyCon -> Arity
tyConArity TyCon
tc) [Xi]
tys
         ; (Xi
xi1, TcCoercionN
co1) <- TyCon -> [Xi] -> RewriteM (Xi, TcCoercionN)
rewrite_exact_fam_app TyCon
tc [Xi]
tys1
               -- co1 :: xi1 ~ F tys1

         ; Xi -> TcCoercionN -> [Xi] -> RewriteM (Xi, TcCoercionN)
rewrite_app_ty_args Xi
xi1 TcCoercionN
co1 [Xi]
tys_rest }

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

       -- STEP 1/2. Try to reduce without reducing arguments first.
       ; Maybe (TcCoercionN, Xi)
result1 <- TyCon -> [Xi] -> RewriteM (Maybe (TcCoercionN, Xi))
try_to_reduce TyCon
tc [Xi]
tys
       ; case Maybe (TcCoercionN, Xi)
result1 of
             -- Don't use the cache;
             -- See Note [rewrite_exact_fam_app performance]
         { Just (TcCoercionN
co, Xi
xi) -> Bool -> (Xi, TcCoercionN) -> RewriteM (Xi, TcCoercionN)
finish Bool
False (Xi
xi, TcCoercionN
co)
         ; Maybe (TcCoercionN, Xi)
Nothing ->

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

       ; let role :: Role
role    = EqRel -> Role
eqRelRole EqRel
eq_rel
             args_co :: TcCoercionN
args_co = HasDebugCallStack => Role -> TyCon -> [TcCoercionN] -> TcCoercionN
Role -> TyCon -> [TcCoercionN] -> TcCoercionN
mkTyConAppCo Role
role TyCon
tc [TcCoercionN]
cos
           -- args_co :: F xis ~r F tys

             homogenise :: TcType -> TcCoercion -> (TcType, TcCoercion)
               -- in (xi', co') = homogenise xi co
               --   assume co :: xi ~r F xis, co is homogeneous
               --   then xi' :: tcTypeKind(F tys)
               --   and co' :: xi' ~r F tys, which is homogeneous
             homogenise :: Xi -> TcCoercionN -> (Xi, TcCoercionN)
homogenise Xi
xi TcCoercionN
co = Xi -> TcCoercionN -> Role -> MCoercionN -> (Xi, TcCoercionN)
homogenise_result Xi
xi (TcCoercionN
co TcCoercionN -> TcCoercionN -> TcCoercionN
`mkTcTransCo` TcCoercionN
args_co) Role
role MCoercionN
kind_co

         -- STEP 4: try the inerts
       ; Maybe (TcCoercionN, Xi, CtFlavourRole)
result2 <- TcS (Maybe (TcCoercionN, Xi, CtFlavourRole))
-> RewriteM (Maybe (TcCoercionN, Xi, CtFlavourRole))
forall a. TcS a -> RewriteM a
liftTcS (TcS (Maybe (TcCoercionN, Xi, CtFlavourRole))
 -> RewriteM (Maybe (TcCoercionN, Xi, CtFlavourRole)))
-> TcS (Maybe (TcCoercionN, Xi, CtFlavourRole))
-> RewriteM (Maybe (TcCoercionN, Xi, CtFlavourRole))
forall a b. (a -> b) -> a -> b
$ TyCon -> [Xi] -> TcS (Maybe (TcCoercionN, Xi, CtFlavourRole))
lookupFamAppInert TyCon
tc [Xi]
xis
       ; CtFlavour
flavour <- RewriteM CtFlavour
getFlavour
       ; case Maybe (TcCoercionN, Xi, CtFlavourRole)
result2 of
         { Just (TcCoercionN
co, Xi
xi, fr :: CtFlavourRole
fr@(CtFlavour
_, EqRel
inert_eq_rel))
             -- co :: F xis ~ir xi

             | CtFlavourRole
fr CtFlavourRole -> CtFlavourRole -> Bool
`eqCanRewriteFR` (CtFlavour
flavour, EqRel
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
<+> [Xi] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Xi]
xis SDoc -> SDoc -> SDoc
$$ Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr Xi
xi)
                    ; Bool -> (Xi, TcCoercionN) -> RewriteM (Xi, TcCoercionN)
finish Bool
True (Xi -> TcCoercionN -> (Xi, TcCoercionN)
homogenise Xi
xi TcCoercionN
downgraded_co) }
               -- 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_co :: TcCoercionN
downgraded_co = Role -> Role -> TcCoercionN -> TcCoercionN
tcDowngradeRole Role
role Role
inert_role (TcCoercionN -> TcCoercionN
mkTcSymCo TcCoercionN
co)
                 -- downgraded_co :: xi ~r F xis

         ; Maybe (TcCoercionN, Xi, CtFlavourRole)
_ ->

         -- inert didn't work. Try to reduce again, in STEP 5/6.
    do { Maybe (TcCoercionN, Xi)
result3 <- TyCon -> [Xi] -> RewriteM (Maybe (TcCoercionN, Xi))
try_to_reduce TyCon
tc [Xi]
xis
       ; case Maybe (TcCoercionN, Xi)
result3 of
           Just (TcCoercionN
co, Xi
xi) -> Bool -> (Xi, TcCoercionN) -> RewriteM (Xi, TcCoercionN)
finish Bool
True (Xi -> TcCoercionN -> (Xi, TcCoercionN)
homogenise Xi
xi TcCoercionN
co)
           Maybe (TcCoercionN, Xi)
Nothing       -> -- we have made no progress at all: STEP 7.
                            (Xi, TcCoercionN) -> RewriteM (Xi, TcCoercionN)
forall (m :: * -> *) a. Monad m => a -> m a
return (Xi -> TcCoercionN -> (Xi, TcCoercionN)
homogenise Xi
reduced (Role -> Xi -> TcCoercionN
mkTcReflCo Role
role Xi
reduced))
             where
               reduced :: Xi
reduced = TyCon -> [Xi] -> Xi
mkTyConApp TyCon
tc [Xi]
xis }}}}}
  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?
           -> (Xi, Coercion) -> RewriteM (Xi, Coercion)
    finish :: Bool -> (Xi, TcCoercionN) -> RewriteM (Xi, TcCoercionN)
finish Bool
use_cache (Xi
xi, TcCoercionN
co)
      = do { -- rewrite the result: FINISH 1
             (Xi
fully, TcCoercionN
fully_co) <- RewriteM (Xi, TcCoercionN) -> RewriteM (Xi, TcCoercionN)
forall a. RewriteM a -> RewriteM a
bumpDepth (RewriteM (Xi, TcCoercionN) -> RewriteM (Xi, TcCoercionN))
-> RewriteM (Xi, TcCoercionN) -> RewriteM (Xi, TcCoercionN)
forall a b. (a -> b) -> a -> b
$ Xi -> RewriteM (Xi, TcCoercionN)
rewrite_one Xi
xi
           ; let final_co :: TcCoercionN
final_co = TcCoercionN
fully_co TcCoercionN -> TcCoercionN -> TcCoercionN
`mkTcTransCo` TcCoercionN
co
           ; EqRel
eq_rel <- RewriteM EqRel
getEqRel
           ; CtFlavour
flavour <- RewriteM CtFlavour
getFlavour

             -- 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 Bool -> Bool -> Bool
&& CtFlavour
flavour CtFlavour -> CtFlavour -> Bool
forall a. Eq a => a -> a -> Bool
/= CtFlavour
Derived) (RewriteM () -> RewriteM ()) -> RewriteM () -> RewriteM ()
forall a b. (a -> b) -> a -> b
$
             -- the cache only wants Nominal eqs
             -- and Wanteds can rewrite Deriveds; the cache
             -- has only Givens
             TcS () -> RewriteM ()
forall a. TcS a -> RewriteM a
liftTcS (TcS () -> RewriteM ()) -> TcS () -> RewriteM ()
forall a b. (a -> b) -> a -> b
$ TyCon -> [Xi] -> (TcCoercionN, Xi) -> TcS ()
extendFamAppCache TyCon
tc [Xi]
tys (TcCoercionN
final_co, Xi
fully)
           ; (Xi, TcCoercionN) -> RewriteM (Xi, TcCoercionN)
forall (m :: * -> *) a. Monad m => a -> m a
return (Xi
fully, TcCoercionN
final_co) }
    {-# INLINE finish #-}

-- Returned coercion is output ~r input, where r is the role in the RewriteM monad
-- See Note [How to normalise a family application]
try_to_reduce :: TyCon -> [TcType] -> RewriteM (Maybe (TcCoercion, TcType))
try_to_reduce :: TyCon -> [Xi] -> RewriteM (Maybe (TcCoercionN, Xi))
try_to_reduce TyCon
tc [Xi]
tys
  = do { Maybe (TcCoercionN, Xi)
result <- TcS (Maybe (TcCoercionN, Xi)) -> RewriteM (Maybe (TcCoercionN, Xi))
forall a. TcS a -> RewriteM a
liftTcS (TcS (Maybe (TcCoercionN, Xi))
 -> RewriteM (Maybe (TcCoercionN, Xi)))
-> TcS (Maybe (TcCoercionN, Xi))
-> RewriteM (Maybe (TcCoercionN, Xi))
forall a b. (a -> b) -> a -> b
$ [TcS (Maybe (TcCoercionN, Xi))] -> TcS (Maybe (TcCoercionN, Xi))
forall (m :: * -> *) (f :: * -> *) a.
(Monad m, Foldable f) =>
f (m (Maybe a)) -> m (Maybe a)
firstJustsM [ TyCon -> [Xi] -> TcS (Maybe (TcCoercionN, Xi))
lookupFamAppCache TyCon
tc [Xi]
tys  -- STEP 5
                                         , TyCon -> [Xi] -> TcS (Maybe (TcCoercionN, Xi))
matchFam TyCon
tc [Xi]
tys ]         -- STEP 6
       ; Maybe (TcCoercionN, Xi) -> RewriteM (Maybe (TcCoercionN, Xi))
downgrade Maybe (TcCoercionN, Xi)
result }
  where
    -- The result above is always Nominal. We might want a Representational
    -- coercion; this downgrades (and prints, out of convenience).
    downgrade :: Maybe (TcCoercionN, TcType) -> RewriteM (Maybe (TcCoercion, TcType))
    downgrade :: Maybe (TcCoercionN, Xi) -> RewriteM (Maybe (TcCoercionN, Xi))
downgrade Maybe (TcCoercionN, Xi)
Nothing = Maybe (TcCoercionN, Xi) -> RewriteM (Maybe (TcCoercionN, Xi))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (TcCoercionN, Xi)
forall a. Maybe a
Nothing
    downgrade result :: Maybe (TcCoercionN, Xi)
result@(Just (TcCoercionN
co, Xi
xi))
      = 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, [Xi] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Xi]
tys, Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr Xi
xi
                  , TcCoercionN -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcCoercionN
co SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> Pair Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TcCoercionN -> Pair Xi
coercionKind TcCoercionN
co)
                  ]
           ; 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  -> Maybe (TcCoercionN, Xi) -> RewriteM (Maybe (TcCoercionN, Xi))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (TcCoercionN, Xi)
result
               EqRel
ReprEq -> Maybe (TcCoercionN, Xi) -> RewriteM (Maybe (TcCoercionN, Xi))
forall (m :: * -> *) a. Monad m => a -> m a
return ((TcCoercionN, Xi) -> Maybe (TcCoercionN, Xi)
forall a. a -> Maybe a
Just (HasDebugCallStack => TcCoercionN -> TcCoercionN
TcCoercionN -> TcCoercionN
mkSubCo TcCoercionN
co, Xi
xi)) }

{-
************************************************************************
*                                                                      *
             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 TcType Coercion
      -- ^ The tyvar rewrites to a not-necessarily rewritten other type.
      -- co :: new type ~r old type, where 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 (Xi, Coercion)
rewriteTyVar :: TcTyVar -> RewriteM (Xi, TcCoercionN)
rewriteTyVar TcTyVar
tv
  = do { RewriteTvResult
mb_yes <- TcTyVar -> RewriteM RewriteTvResult
rewrite_tyvar1 TcTyVar
tv
       ; case RewriteTvResult
mb_yes of
           RTRFollowed Xi
ty1 TcCoercionN
co1  -- Recur
             -> do { (Xi
ty2, TcCoercionN
co2) <- Xi -> RewriteM (Xi, TcCoercionN)
rewrite_one Xi
ty1
                   -- ; traceRewriteM "rewriteTyVar2" (ppr tv $$ ppr ty2)
                   ; (Xi, TcCoercionN) -> RewriteM (Xi, TcCoercionN)
forall (m :: * -> *) a. Monad m => a -> m a
return (Xi
ty2, TcCoercionN
co2 TcCoercionN -> TcCoercionN -> TcCoercionN
`mkTransCo` TcCoercionN
co1) }

           RewriteTvResult
RTRNotFollowed   -- Done, but make sure the kind is zonked
                            -- Note [Rewriting] invariant (F0) and (F1)
             -> do { TcTyVar
tv' <- TcS TcTyVar -> RewriteM TcTyVar
forall a. TcS a -> RewriteM a
liftTcS (TcS TcTyVar -> RewriteM TcTyVar)
-> TcS TcTyVar -> RewriteM TcTyVar
forall a b. (a -> b) -> a -> b
$ (Xi -> TcS Xi) -> TcTyVar -> TcS TcTyVar
forall (m :: * -> *).
Monad m =>
(Xi -> m Xi) -> TcTyVar -> m TcTyVar
updateTyVarKindM Xi -> TcS Xi
zonkTcType TcTyVar
tv
                   ; Role
role <- RewriteM Role
getRole
                   ; let ty' :: Xi
ty' = TcTyVar -> Xi
mkTyVarTy TcTyVar
tv'
                   ; (Xi, TcCoercionN) -> RewriteM (Xi, TcCoercionN)
forall (m :: * -> *) a. Monad m => a -> m a
return (Xi
ty', Role -> Xi -> TcCoercionN
mkTcReflCo Role
role Xi
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 :: TcTyVar -> RewriteM RewriteTvResult
rewrite_tyvar1 TcTyVar
tv
  = do { Maybe Xi
mb_ty <- TcS (Maybe Xi) -> RewriteM (Maybe Xi)
forall a. TcS a -> RewriteM a
liftTcS (TcS (Maybe Xi) -> RewriteM (Maybe Xi))
-> TcS (Maybe Xi) -> RewriteM (Maybe Xi)
forall a b. (a -> b) -> a -> b
$ TcTyVar -> TcS (Maybe Xi)
isFilledMetaTyVar_maybe TcTyVar
tv
       ; case Maybe Xi
mb_ty of
           Just Xi
ty -> do { String -> SDoc -> RewriteM ()
traceRewriteM String
"Following filled tyvar"
                             (TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
tv SDoc -> SDoc -> SDoc
<+> SDoc
equals SDoc -> SDoc -> SDoc
<+> Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr Xi
ty)
                         ; Role
role <- RewriteM Role
getRole
                         ; RewriteTvResult -> RewriteM RewriteTvResult
forall (m :: * -> *) a. Monad m => a -> m a
return (Xi -> TcCoercionN -> RewriteTvResult
RTRFollowed Xi
ty (Role -> Xi -> TcCoercionN
mkReflCo Role
role Xi
ty)) } ;
           Maybe Xi
Nothing -> do { String -> SDoc -> RewriteM ()
traceRewriteM String
"Unfilled tyvar" (TcTyVar -> SDoc
pprTyVar TcTyVar
tv)
                         ; CtFlavourRole
fr <- RewriteM CtFlavourRole
getFlavourRole
                         ; TcTyVar -> CtFlavourRole -> RewriteM RewriteTvResult
rewrite_tyvar2 TcTyVar
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 :: TcTyVar -> CtFlavourRole -> RewriteM RewriteTvResult
rewrite_tyvar2 TcTyVar
tv fr :: CtFlavourRole
fr@(CtFlavour
_, EqRel
eq_rel)
  = do { DTyVarEnv EqualCtList
ieqs <- TcS (DTyVarEnv EqualCtList) -> RewriteM (DTyVarEnv EqualCtList)
forall a. TcS a -> RewriteM a
liftTcS (TcS (DTyVarEnv EqualCtList) -> RewriteM (DTyVarEnv EqualCtList))
-> TcS (DTyVarEnv EqualCtList) -> RewriteM (DTyVarEnv EqualCtList)
forall a b. (a -> b) -> a -> b
$ TcS (DTyVarEnv EqualCtList)
getInertEqs
       ; case DTyVarEnv EqualCtList -> TcTyVar -> Maybe EqualCtList
forall a. DVarEnv a -> TcTyVar -> Maybe a
lookupDVarEnv DTyVarEnv EqualCtList
ieqs TcTyVar
tv of
           Just (EqualCtList (Ct
ct :| [Ct]
_))   -- If the first doesn't work,
                                          -- the subsequent ones won't either
             | CEqCan { cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
ctev, cc_lhs :: Ct -> CanEqLHS
cc_lhs = TyVarLHS TcTyVar
tv
                      , cc_rhs :: Ct -> Xi
cc_rhs = Xi
rhs_ty, cc_eq_rel :: Ct -> EqRel
cc_eq_rel = EqRel
ct_eq_rel } <- Ct
ct
             , let ct_fr :: CtFlavourRole
ct_fr = (CtEvidence -> CtFlavour
ctEvFlavour CtEvidence
ctev, EqRel
ct_eq_rel)
             , CtFlavourRole
ct_fr CtFlavourRole -> CtFlavourRole -> Bool
`eqCanRewriteFR` CtFlavourRole
fr  -- This is THE key call of eqCanRewriteFR
             -> do { String -> SDoc -> RewriteM ()
traceRewriteM String
"Following inert tyvar"
                        (TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
tv SDoc -> SDoc -> SDoc
<+>
                         SDoc
equals SDoc -> SDoc -> SDoc
<+>
                         Xi -> SDoc
forall a. Outputable a => a -> SDoc
ppr Xi
rhs_ty SDoc -> SDoc -> SDoc
$$ CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ctev)
                    ; let rewrite_co1 :: TcCoercionN
rewrite_co1 = TcCoercionN -> TcCoercionN
mkSymCo (HasDebugCallStack => CtEvidence -> TcCoercionN
CtEvidence -> TcCoercionN
ctEvCoercion CtEvidence
ctev)
                          rewrite_co :: TcCoercionN
rewrite_co  = case (EqRel
ct_eq_rel, EqRel
eq_rel) of
                            (EqRel
ReprEq, EqRel
_rel)  -> ASSERT( _rel == ReprEq )
                                    -- if this ASSERT fails, then
                                    -- eqCanRewriteFR answered incorrectly
                                               TcCoercionN
rewrite_co1
                            (EqRel
NomEq, EqRel
NomEq)  -> TcCoercionN
rewrite_co1
                            (EqRel
NomEq, EqRel
ReprEq) -> HasDebugCallStack => TcCoercionN -> TcCoercionN
TcCoercionN -> TcCoercionN
mkSubCo TcCoercionN
rewrite_co1

                    ; RewriteTvResult -> RewriteM RewriteTvResult
forall (m :: * -> *) a. Monad m => a -> m a
return (Xi -> TcCoercionN -> RewriteTvResult
RTRFollowed Xi
rhs_ty TcCoercionN
rewrite_co) }
                    -- NB: ct is Derived then fmode must be also, hence
                    -- we are not going to touch the returned coercion
                    -- so ctEvCoercion is fine.

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

{-
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' :: Xi -> ([TyCoBinder], Xi, Bool)
split_pi_tys' Xi
ty = Xi -> Xi -> ([TyCoBinder], Xi, Bool)
split Xi
ty Xi
ty
  where
     -- put common cases first
  split :: Xi -> Xi -> ([TyCoBinder], Xi, Bool)
split Xi
_       (ForAllTy TyVarBinder
b Xi
res) = let -- This bang is necessary lest we see rather
                                       -- terrible reboxing, as noted in #19102.
                                       !([TyCoBinder]
bs, Xi
ty, Bool
_) = Xi -> Xi -> ([TyCoBinder], Xi, Bool)
split Xi
res Xi
res
                                   in  (TyVarBinder -> TyCoBinder
Named TyVarBinder
b TyCoBinder -> [TyCoBinder] -> [TyCoBinder]
forall a. a -> [a] -> [a]
: [TyCoBinder]
bs, Xi
ty, Bool
True)
  split Xi
_       (FunTy { ft_af :: Xi -> AnonArgFlag
ft_af = AnonArgFlag
af, ft_mult :: Xi -> Xi
ft_mult = Xi
w, ft_arg :: Xi -> Xi
ft_arg = Xi
arg, ft_res :: Xi -> Xi
ft_res = Xi
res })
                                 = let -- See #19102
                                       !([TyCoBinder]
bs, Xi
ty, Bool
named) = Xi -> Xi -> ([TyCoBinder], Xi, Bool)
split Xi
res Xi
res
                                   in  (AnonArgFlag -> Scaled Xi -> TyCoBinder
Anon AnonArgFlag
af (Xi -> Xi -> Scaled Xi
forall a. Xi -> a -> Scaled a
mkScaled Xi
w Xi
arg) TyCoBinder -> [TyCoBinder] -> [TyCoBinder]
forall a. a -> [a] -> [a]
: [TyCoBinder]
bs, Xi
ty, Bool
named)

  split Xi
orig_ty Xi
ty | Just Xi
ty' <- Xi -> Maybe Xi
coreView Xi
ty = Xi -> Xi -> ([TyCoBinder], Xi, Bool)
split Xi
orig_ty Xi
ty'
  split Xi
orig_ty Xi
_                = ([], Xi
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 TcTyVar
tv (NamedTCB ArgFlag
vis)) ([TyCoBinder]
bndrs, Bool
_)
      = (TyVarBinder -> TyCoBinder
Named (TcTyVar -> ArgFlag -> TyVarBinder
forall var argf. var -> argf -> VarBndr var argf
Bndr TcTyVar
tv ArgFlag
vis) TyCoBinder -> [TyCoBinder] -> [TyCoBinder]
forall a. a -> [a] -> [a]
: [TyCoBinder]
bndrs, Bool
True)
    go (Bndr TcTyVar
tv (AnonTCB AnonArgFlag
af))   ([TyCoBinder]
bndrs, Bool
n)
      = (AnonArgFlag -> Scaled Xi -> TyCoBinder
Anon AnonArgFlag
af (Xi -> Scaled Xi
forall a. a -> Scaled a
tymult (TcTyVar -> Xi
tyVarKind TcTyVar
tv)) TyCoBinder -> [TyCoBinder] -> [TyCoBinder]
forall a. a -> [a] -> [a]
: [TyCoBinder]
bndrs, Bool
n)
    {-# INLINE go #-}
{-# INLINE ty_con_binders_ty_binders' #-}