{-# OPTIONS_GHC -Wno-incomplete-uni-patterns   #-}

-- | Tidying types and coercions for printing in error messages.
module GHC.Core.TyCo.Tidy
  (
        -- * Tidying type related things up for printing
        tidyType, tidyTypes,
        tidyCo,   tidyCos,
        tidyTopType,

        tidyOpenType,  tidyOpenTypes,
        tidyOpenTypeX, tidyOpenTypesX,
        tidyFreeTyCoVars, tidyFreeTyCoVarX, tidyFreeTyCoVarsX,

        tidyAvoiding,
        tidyVarBndr, tidyVarBndrs, avoidNameClashes,
        tidyForAllTyBinder, tidyForAllTyBinders,
        tidyTyCoVarOcc
  ) where

import GHC.Prelude
import GHC.Data.FastString

import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.FVs
import GHC.Types.Name hiding (varName)
import GHC.Types.Var
import GHC.Types.Var.Env
import GHC.Utils.Misc (strictMap)

import Data.List (mapAccumL)

{- **********************************************************************

                  TidyType

********************************************************************** -}

{- Note [Tidying open types]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When tidying some open types [t1,..,tn], we find their free vars, and tidy them first.

But (tricky point) we restrict the occ_env part of inner_env to just the /free/
vars of [t1..tn], so that we don't gratuitously rename the /bound/ variables.

Example: assume the TidyEnv
      ({"a1","b"} , [a_4 :-> a1, b_7 :-> b])
and call tidyOpenTypes on
      [a_1, forall a_2. Maybe (a_2,a_4), forall b. (b,a_1)]
All the a's have the same OccName, but different uniques.

The TidyOccEnv binding for "b" relates b_7, which doesn't appear free in the
these types at all, so we don't want that to mess up the tidying for the
(forall b...).

So we proceed as follows:
  1. Find the free vars.
     In our example:the free vars are a_1 and a_4:

  2. Use tidyFreeTyCoVars to tidy them (workhorse: `tidyFreeCoVarX`)
     In our example:
      * a_4 already has a tidy form, a1, so don't change that
      * a_1 gets tidied to a2

  3. Trim the TidyOccEnv to OccNames of the tidied free vars (`trimTidyEnv`)
     In our example "a1" and "a2"

  4. Now tidy the types.  In our example we get
      [a2, forall a3. Maybe (a3,a1), forall b. (b, a2)]

Note [Tidying is idempotent]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Key invariant: tidyFreeTyCoVars is idempotent, at least if you start with
an empty TidyEnv. This is important because:

  * The typechecker error message processing carefully tidies types, using
    global knowledge; see for example calls to `tidyCt` in GHC.Tc.Errors.

  * Then the type pretty-printer, GHC.Core.TyCo.Ppr.pprType tidies the type
    again, because that's important for pretty-printing types in general.

But the second tidying is a no-op if the first step has happened, because
all the free vars will have distinct OccNames, so no renaming needs to happen.

Note [tidyAvoiding]
~~~~~~~~~~~~~~~~~~~
Consider tidying this unsolved constraint in GHC.Tc.Errors.report_unsolved.
    C a_33, (forall a. Eq a => D a)
Here a_33 is a free unification variable.  If we firs tidy [a_33 :-> "a"]
then we have no choice but to tidy the `forall a` to something else. But it
is confusing (sometimes very confusing) to gratuitously rename skolems in
this way -- see #24868.  So it is better to :

  * Find the /bound/ skolems (just `a` in this case)
  * Initialise the TidyOccEnv to avoid using "a"
  * Now tidy the free a_33 to, say, "a1"
  * Delete "a" from the TidyOccEnv

This is done by `tidyAvoiding`.

The last step is very important; if we leave "a" in the TidyOccEnv, when
we get to the (forall a. blah) we'll rename `a` to "a2", avoiding "a".
-}

-- | This tidies up a type for printing in an error message, or in
-- an interface file.
--
-- It doesn't change the uniques at all, just the print names.
tidyVarBndrs :: TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar])
tidyVarBndrs :: TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar])
tidyVarBndrs TidyEnv
tidy_env [TyCoVar]
tvs
  = (TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar))
-> TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar])
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar)
tidyVarBndr ([TyCoVar] -> TidyEnv -> TidyEnv
avoidNameClashes [TyCoVar]
tvs TidyEnv
tidy_env) [TyCoVar]
tvs

tidyVarBndr :: TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar)
tidyVarBndr :: TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar)
tidyVarBndr tidy_env :: TidyEnv
tidy_env@(TidyOccEnv
occ_env, VarEnv TyCoVar
subst) TyCoVar
var
  = case TidyOccEnv -> OccName -> (TidyOccEnv, OccName)
tidyOccName TidyOccEnv
occ_env (TyCoVar -> OccName
getHelpfulOccName TyCoVar
var) of
      (TidyOccEnv
occ_env', OccName
occ') -> ((TidyOccEnv
occ_env', VarEnv TyCoVar
subst'), TyCoVar
var')
        where
          subst' :: VarEnv TyCoVar
subst' = VarEnv TyCoVar -> TyCoVar -> TyCoVar -> VarEnv TyCoVar
forall a. VarEnv a -> TyCoVar -> a -> VarEnv a
extendVarEnv VarEnv TyCoVar
subst TyCoVar
var TyCoVar
var'
          var' :: TyCoVar
var'   = (Type -> Type) -> TyCoVar -> TyCoVar
updateVarType (TidyEnv -> Type -> Type
tidyType TidyEnv
tidy_env) (TyCoVar -> Name -> TyCoVar
setVarName TyCoVar
var Name
name')
          name' :: Name
name'  = Name -> OccName -> Name
tidyNameOcc Name
name OccName
occ'
          name :: Name
name   = TyCoVar -> Name
varName TyCoVar
var

avoidNameClashes :: [TyCoVar] -> TidyEnv -> TidyEnv
-- Seed the occ_env with clashes among the names, see
-- Note [Tidying multiple names at once] in GHC.Types.Name.Occurrence
avoidNameClashes :: [TyCoVar] -> TidyEnv -> TidyEnv
avoidNameClashes [TyCoVar]
tvs (TidyOccEnv
occ_env, VarEnv TyCoVar
subst)
  = (TidyOccEnv -> [OccName] -> TidyOccEnv
avoidClashesOccEnv TidyOccEnv
occ_env [OccName]
occs, VarEnv TyCoVar
subst)
  where
    occs :: [OccName]
occs = (TyCoVar -> OccName) -> [TyCoVar] -> [OccName]
forall a b. (a -> b) -> [a] -> [b]
map TyCoVar -> OccName
getHelpfulOccName [TyCoVar]
tvs

getHelpfulOccName :: TyCoVar -> OccName
-- A TcTyVar with a System Name is probably a
-- unification variable; when we tidy them we give them a trailing
-- "0" (or 1 etc) so that they don't take precedence for the
-- un-modified name. Plus, indicating a unification variable in
-- this way is a helpful clue for users
getHelpfulOccName :: TyCoVar -> OccName
getHelpfulOccName TyCoVar
tv
  | Name -> Bool
isSystemName Name
name, TyCoVar -> Bool
isTcTyVar TyCoVar
tv
  = FastString -> OccName
mkTyVarOccFS (OccName -> FastString
occNameFS OccName
occ FastString -> FastString -> FastString
`appendFS` String -> FastString
fsLit String
"0")
  | Bool
otherwise
  = OccName
occ
  where
   name :: Name
name = TyCoVar -> Name
varName TyCoVar
tv
   occ :: OccName
occ  = Name -> OccName
forall a. NamedThing a => a -> OccName
getOccName Name
name

tidyForAllTyBinder :: TidyEnv -> VarBndr TyCoVar vis
                  -> (TidyEnv, VarBndr TyCoVar vis)
tidyForAllTyBinder :: forall vis.
TidyEnv -> VarBndr TyCoVar vis -> (TidyEnv, VarBndr TyCoVar vis)
tidyForAllTyBinder TidyEnv
tidy_env (Bndr TyCoVar
tv vis
vis)
  = (TidyEnv
tidy_env', TyCoVar -> vis -> VarBndr TyCoVar vis
forall var argf. var -> argf -> VarBndr var argf
Bndr TyCoVar
tv' vis
vis)
  where
    (TidyEnv
tidy_env', TyCoVar
tv') = TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar)
tidyVarBndr TidyEnv
tidy_env TyCoVar
tv

tidyForAllTyBinders :: TidyEnv -> [VarBndr TyCoVar vis]
                   -> (TidyEnv, [VarBndr TyCoVar vis])
tidyForAllTyBinders :: forall vis.
TidyEnv
-> [VarBndr TyCoVar vis] -> (TidyEnv, [VarBndr TyCoVar vis])
tidyForAllTyBinders TidyEnv
tidy_env [VarBndr TyCoVar vis]
tvbs
  = (TidyEnv -> VarBndr TyCoVar vis -> (TidyEnv, VarBndr TyCoVar vis))
-> TidyEnv
-> [VarBndr TyCoVar vis]
-> (TidyEnv, [VarBndr TyCoVar vis])
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL TidyEnv -> VarBndr TyCoVar vis -> (TidyEnv, VarBndr TyCoVar vis)
forall vis.
TidyEnv -> VarBndr TyCoVar vis -> (TidyEnv, VarBndr TyCoVar vis)
tidyForAllTyBinder
              ([TyCoVar] -> TidyEnv -> TidyEnv
avoidNameClashes ([VarBndr TyCoVar vis] -> [TyCoVar]
forall tv argf. [VarBndr tv argf] -> [tv]
binderVars [VarBndr TyCoVar vis]
tvbs) TidyEnv
tidy_env) [VarBndr TyCoVar vis]
tvbs

---------------
tidyFreeTyCoVars :: TidyEnv -> [TyCoVar] -> TidyEnv
-- ^ Add the free 'TyVar's to the env in tidy form,
-- so that we can tidy the type they are free in
-- Precondition: input free vars are closed over kinds and
-- This function does a scopedSort, so that tidied variables
-- have tidied kinds.
-- See Note [Tidying is idempotent]
tidyFreeTyCoVars :: TidyEnv -> [TyCoVar] -> TidyEnv
tidyFreeTyCoVars TidyEnv
tidy_env [TyCoVar]
tyvars = (TidyEnv, [TyCoVar]) -> TidyEnv
forall a b. (a, b) -> a
fst (TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar])
tidyFreeTyCoVarsX TidyEnv
tidy_env [TyCoVar]
tyvars)

---------------
tidyFreeTyCoVarsX :: TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar])
-- Precondition: input free vars are closed over kinds and
-- This function does a scopedSort, so that tidied variables
-- have tidied kinds.
-- See Note [Tidying is idempotent]
tidyFreeTyCoVarsX :: TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar])
tidyFreeTyCoVarsX TidyEnv
env [TyCoVar]
tyvars = (TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar))
-> TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar])
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar)
tidyFreeTyCoVarX TidyEnv
env ([TyCoVar] -> (TidyEnv, [TyCoVar]))
-> [TyCoVar] -> (TidyEnv, [TyCoVar])
forall a b. (a -> b) -> a -> b
$
                               [TyCoVar] -> [TyCoVar]
scopedSort [TyCoVar]
tyvars

---------------
tidyFreeTyCoVarX :: TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar)
-- ^ Treat a new 'TyCoVar' as a binder, and give it a fresh tidy name
-- using the environment if one has not already been allocated. See
-- also 'tidyVarBndr'
-- See Note [Tidying is idempotent]
tidyFreeTyCoVarX :: TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar)
tidyFreeTyCoVarX env :: TidyEnv
env@(TidyOccEnv
_, VarEnv TyCoVar
subst) TyCoVar
tyvar
  = case VarEnv TyCoVar -> TyCoVar -> Maybe TyCoVar
forall a. VarEnv a -> TyCoVar -> Maybe a
lookupVarEnv VarEnv TyCoVar
subst TyCoVar
tyvar of
        Just TyCoVar
tyvar' -> (TidyEnv
env, TyCoVar
tyvar')           -- Already substituted
        Maybe TyCoVar
Nothing     -> TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar)
tidyVarBndr TidyEnv
env TyCoVar
tyvar  -- Treat it as a binder

---------------
tidyTyCoVarOcc :: TidyEnv -> TyCoVar -> TyCoVar
tidyTyCoVarOcc :: TidyEnv -> TyCoVar -> TyCoVar
tidyTyCoVarOcc env :: TidyEnv
env@(TidyOccEnv
_, VarEnv TyCoVar
subst) TyCoVar
tcv
  = case VarEnv TyCoVar -> TyCoVar -> Maybe TyCoVar
forall a. VarEnv a -> TyCoVar -> Maybe a
lookupVarEnv VarEnv TyCoVar
subst TyCoVar
tcv of
        Maybe TyCoVar
Nothing   -> (Type -> Type) -> TyCoVar -> TyCoVar
updateVarType (TidyEnv -> Type -> Type
tidyType TidyEnv
env) TyCoVar
tcv
        Just TyCoVar
tcv' -> TyCoVar
tcv'

---------------

{-
Note [Strictness in tidyType and friends]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Since the result of tidying will be inserted into the HPT, a potentially
long-lived structure, we generally want to avoid pieces of the old AST
being retained by the thunks produced by tidying.

For this reason we take great care to ensure that all pieces of the tidied AST
are evaluated strictly.  So you will see lots of strict applications ($!) and
uses of `strictMap` in `tidyType`, `tidyTypes` and `tidyCo`.

In the case of tidying of lists (e.g. lists of arguments) we prefer to use
`strictMap f xs` rather than `seqList (map f xs)` as the latter will
unnecessarily allocate a thunk, which will then be almost-immediately
evaluated, for each list element.

Making `tidyType` strict has a rather large effect on performance: see #14738.
Sometimes as much as a 5% reduction in allocation.
-}

-- | Tidy a list of Types
--
-- See Note [Strictness in tidyType and friends]
tidyTypes :: TidyEnv -> [Type] -> [Type]
tidyTypes :: TidyEnv -> [Type] -> [Type]
tidyTypes TidyEnv
env [Type]
tys = (Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
strictMap (TidyEnv -> Type -> Type
tidyType TidyEnv
env) [Type]
tys

---------------


-- | Tidy a Type
--
-- See Note [Strictness in tidyType and friends]
tidyType :: TidyEnv -> Type -> Type
tidyType :: TidyEnv -> Type -> Type
tidyType TidyEnv
_   t :: Type
t@(LitTy {})           = Type
t -- Preserve sharing
tidyType TidyEnv
env (TyVarTy TyCoVar
tv)           = TyCoVar -> Type
TyVarTy (TyCoVar -> Type) -> TyCoVar -> Type
forall a b. (a -> b) -> a -> b
$! TidyEnv -> TyCoVar -> TyCoVar
tidyTyCoVarOcc TidyEnv
env TyCoVar
tv
tidyType TidyEnv
_   t :: Type
t@(TyConApp TyCon
_ [])      = Type
t -- Preserve sharing if possible
tidyType TidyEnv
env (TyConApp TyCon
tycon [Type]
tys)   = TyCon -> [Type] -> Type
TyConApp TyCon
tycon ([Type] -> Type) -> [Type] -> Type
forall a b. (a -> b) -> a -> b
$! TidyEnv -> [Type] -> [Type]
tidyTypes TidyEnv
env [Type]
tys
tidyType TidyEnv
env (AppTy Type
fun Type
arg)        = (Type -> Type -> Type
AppTy (Type -> Type -> Type) -> Type -> Type -> Type
forall a b. (a -> b) -> a -> b
$! (TidyEnv -> Type -> Type
tidyType TidyEnv
env Type
fun)) (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$! (TidyEnv -> Type -> Type
tidyType TidyEnv
env Type
arg)
tidyType TidyEnv
env (CastTy Type
ty KindCoercion
co)         = (Type -> KindCoercion -> Type
CastTy (Type -> KindCoercion -> Type) -> Type -> KindCoercion -> Type
forall a b. (a -> b) -> a -> b
$! TidyEnv -> Type -> Type
tidyType TidyEnv
env Type
ty) (KindCoercion -> Type) -> KindCoercion -> Type
forall a b. (a -> b) -> a -> b
$! (TidyEnv -> KindCoercion -> KindCoercion
tidyCo TidyEnv
env KindCoercion
co)
tidyType TidyEnv
env (CoercionTy KindCoercion
co)        = KindCoercion -> Type
CoercionTy (KindCoercion -> Type) -> KindCoercion -> Type
forall a b. (a -> b) -> a -> b
$! (TidyEnv -> KindCoercion -> KindCoercion
tidyCo TidyEnv
env KindCoercion
co)
tidyType TidyEnv
env ty :: Type
ty@(FunTy FunTyFlag
_ Type
w Type
arg Type
res) = let { !w' :: Type
w'   = TidyEnv -> Type -> Type
tidyType TidyEnv
env Type
w
                                          ; !arg' :: Type
arg' = TidyEnv -> Type -> Type
tidyType TidyEnv
env Type
arg
                                          ; !res' :: Type
res' = TidyEnv -> Type -> Type
tidyType TidyEnv
env Type
res }
                                      in Type
ty { ft_mult = w', ft_arg = arg', ft_res = res' }
tidyType TidyEnv
env (ty :: Type
ty@(ForAllTy{}))      = TidyEnv -> Type -> Type
tidyForAllType TidyEnv
env Type
ty


tidyForAllType :: TidyEnv -> Type -> Type
tidyForAllType :: TidyEnv -> Type -> Type
tidyForAllType TidyEnv
env Type
ty
   = ([(TyCoVar, ForAllTyFlag)] -> Type -> Type
mkForAllTys' ([(TyCoVar, ForAllTyFlag)] -> Type -> Type)
-> [(TyCoVar, ForAllTyFlag)] -> Type -> Type
forall a b. (a -> b) -> a -> b
$! ([TyCoVar] -> [ForAllTyFlag] -> [(TyCoVar, ForAllTyFlag)]
forall a b. [a] -> [b] -> [(a, b)]
zip [TyCoVar]
tcvs' [ForAllTyFlag]
vis)) (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$! TidyEnv -> Type -> Type
tidyType TidyEnv
body_env Type
body_ty
  where
    ([TyCoVar]
tcvs, [ForAllTyFlag]
vis, Type
body_ty) = Type -> ([TyCoVar], [ForAllTyFlag], Type)
splitForAllTyCoVars' Type
ty
    (TidyEnv
body_env, [TyCoVar]
tcvs') = TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar])
tidyVarBndrs TidyEnv
env [TyCoVar]
tcvs

-- The following two functions differ from mkForAllTys and splitForAllTyCoVars in that
-- they expect/preserve the ForAllTyFlag argument. These belong to "GHC.Core.Type", but
-- how should they be named?
mkForAllTys' :: [(TyCoVar, ForAllTyFlag)] -> Type -> Type
mkForAllTys' :: [(TyCoVar, ForAllTyFlag)] -> Type -> Type
mkForAllTys' [(TyCoVar, ForAllTyFlag)]
tvvs Type
ty = ((TyCoVar, ForAllTyFlag) -> Type -> Type)
-> Type -> [(TyCoVar, ForAllTyFlag)] -> Type
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (TyCoVar, ForAllTyFlag) -> Type -> Type
strictMkForAllTy Type
ty [(TyCoVar, ForAllTyFlag)]
tvvs
  where
    strictMkForAllTy :: (TyCoVar, ForAllTyFlag) -> Type -> Type
strictMkForAllTy (TyCoVar
tv,ForAllTyFlag
vis) Type
ty = (ForAllTyBinder -> Type -> Type
ForAllTy (ForAllTyBinder -> Type -> Type) -> ForAllTyBinder -> Type -> Type
forall a b. (a -> b) -> a -> b
$! ((TyCoVar -> ForAllTyFlag -> ForAllTyBinder
forall var argf. var -> argf -> VarBndr var argf
Bndr (TyCoVar -> ForAllTyFlag -> ForAllTyBinder)
-> TyCoVar -> ForAllTyFlag -> ForAllTyBinder
forall a b. (a -> b) -> a -> b
$! TyCoVar
tv) (ForAllTyFlag -> ForAllTyBinder) -> ForAllTyFlag -> ForAllTyBinder
forall a b. (a -> b) -> a -> b
$! ForAllTyFlag
vis)) (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$! Type
ty

splitForAllTyCoVars' :: Type -> ([TyCoVar], [ForAllTyFlag], Type)
splitForAllTyCoVars' :: Type -> ([TyCoVar], [ForAllTyFlag], Type)
splitForAllTyCoVars' Type
ty = Type
-> [TyCoVar] -> [ForAllTyFlag] -> ([TyCoVar], [ForAllTyFlag], Type)
go Type
ty [] []
  where
    go :: Type
-> [TyCoVar] -> [ForAllTyFlag] -> ([TyCoVar], [ForAllTyFlag], Type)
go (ForAllTy (Bndr TyCoVar
tv ForAllTyFlag
vis) Type
ty) [TyCoVar]
tvs [ForAllTyFlag]
viss = Type
-> [TyCoVar] -> [ForAllTyFlag] -> ([TyCoVar], [ForAllTyFlag], Type)
go Type
ty (TyCoVar
tvTyCoVar -> [TyCoVar] -> [TyCoVar]
forall a. a -> [a] -> [a]
:[TyCoVar]
tvs) (ForAllTyFlag
visForAllTyFlag -> [ForAllTyFlag] -> [ForAllTyFlag]
forall a. a -> [a] -> [a]
:[ForAllTyFlag]
viss)
    go Type
ty                          [TyCoVar]
tvs [ForAllTyFlag]
viss = ([TyCoVar] -> [TyCoVar]
forall a. [a] -> [a]
reverse [TyCoVar]
tvs, [ForAllTyFlag] -> [ForAllTyFlag]
forall a. [a] -> [a]
reverse [ForAllTyFlag]
viss, Type
ty)


---------------
tidyAvoiding :: [OccName]
             -> (TidyEnv -> a -> TidyEnv)
             -> a -> TidyEnv
-- Initialise an empty TidyEnv with some bound vars to avoid,
-- run the do_tidy function, and then remove the bound vars again.
-- See Note [tidyAvoiding]
tidyAvoiding :: forall a. [OccName] -> (TidyEnv -> a -> TidyEnv) -> a -> TidyEnv
tidyAvoiding [OccName]
bound_var_avoids TidyEnv -> a -> TidyEnv
do_tidy a
thing
  = (TidyOccEnv
occs' TidyOccEnv -> [OccName] -> TidyOccEnv
`delTidyOccEnvList` [OccName]
bound_var_avoids, VarEnv TyCoVar
vars')
  where
    (TidyOccEnv
occs', VarEnv TyCoVar
vars') = TidyEnv -> a -> TidyEnv
do_tidy TidyEnv
init_tidy_env a
thing
    init_tidy_env :: TidyEnv
init_tidy_env  = TidyOccEnv -> TidyEnv
mkEmptyTidyEnv ([OccName] -> TidyOccEnv
initTidyOccEnv [OccName]
bound_var_avoids)

---------------
trimTidyEnv :: TidyEnv -> [TyCoVar] -> TidyEnv
trimTidyEnv :: TidyEnv -> [TyCoVar] -> TidyEnv
trimTidyEnv (TidyOccEnv
occ_env, VarEnv TyCoVar
var_env) [TyCoVar]
tcvs
  = (TidyOccEnv -> [OccName] -> TidyOccEnv
trimTidyOccEnv TidyOccEnv
occ_env ((TyCoVar -> OccName) -> [TyCoVar] -> [OccName]
forall a b. (a -> b) -> [a] -> [b]
map TyCoVar -> OccName
forall a. NamedThing a => a -> OccName
getOccName [TyCoVar]
tcvs), VarEnv TyCoVar
var_env)

---------------
-- | Grabs the free type variables, tidies them
-- and then uses 'tidyType' to work over the type itself
tidyOpenTypesX :: TidyEnv -> [Type] -> (TidyEnv, [Type])
-- See Note [Tidying open types]
tidyOpenTypesX :: TidyEnv -> [Type] -> (TidyEnv, [Type])
tidyOpenTypesX TidyEnv
env [Type]
tys
  = (TidyEnv
env1, TidyEnv -> [Type] -> [Type]
tidyTypes TidyEnv
inner_env [Type]
tys)
  where
    free_tcvs :: [TyCoVar] -- Closed over kinds
    free_tcvs :: [TyCoVar]
free_tcvs          = [Type] -> [TyCoVar]
tyCoVarsOfTypesList [Type]
tys
    (TidyEnv
env1, [TyCoVar]
free_tcvs') = TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar])
tidyFreeTyCoVarsX TidyEnv
env [TyCoVar]
free_tcvs
    inner_env :: TidyEnv
inner_env          = TidyEnv -> [TyCoVar] -> TidyEnv
trimTidyEnv TidyEnv
env1 [TyCoVar]
free_tcvs'

---------------
tidyOpenTypeX :: TidyEnv -> Type -> (TidyEnv, Type)
-- See Note [Tidying open types]
tidyOpenTypeX :: TidyEnv -> Type -> (TidyEnv, Type)
tidyOpenTypeX TidyEnv
env Type
ty
  = (TidyEnv
env1, TidyEnv -> Type -> Type
tidyType TidyEnv
inner_env Type
ty)
  where
    free_tcvs :: [TyCoVar]
free_tcvs          = Type -> [TyCoVar]
tyCoVarsOfTypeList Type
ty
    (TidyEnv
env1, [TyCoVar]
free_tcvs') = TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar])
tidyFreeTyCoVarsX TidyEnv
env [TyCoVar]
free_tcvs
    inner_env :: TidyEnv
inner_env          = TidyEnv -> [TyCoVar] -> TidyEnv
trimTidyEnv TidyEnv
env1 [TyCoVar]
free_tcvs'

---------------
tidyOpenTypes :: TidyEnv -> [Type] -> [Type]
tidyOpenTypes :: TidyEnv -> [Type] -> [Type]
tidyOpenTypes TidyEnv
env [Type]
ty = (TidyEnv, [Type]) -> [Type]
forall a b. (a, b) -> b
snd (TidyEnv -> [Type] -> (TidyEnv, [Type])
tidyOpenTypesX TidyEnv
env [Type]
ty)

tidyOpenType :: TidyEnv -> Type -> Type
tidyOpenType :: TidyEnv -> Type -> Type
tidyOpenType TidyEnv
env Type
ty = (TidyEnv, Type) -> Type
forall a b. (a, b) -> b
snd (TidyEnv -> Type -> (TidyEnv, Type)
tidyOpenTypeX TidyEnv
env Type
ty)

---------------
-- | Calls 'tidyType' on a top-level type (i.e. with an empty tidying environment)
tidyTopType :: Type -> Type
tidyTopType :: Type -> Type
tidyTopType Type
ty = TidyEnv -> Type -> Type
tidyType TidyEnv
emptyTidyEnv Type
ty

---------------

-- | Tidy a Coercion
--
-- See Note [Strictness in tidyType and friends]
tidyCo :: TidyEnv -> Coercion -> Coercion
tidyCo :: TidyEnv -> KindCoercion -> KindCoercion
tidyCo TidyEnv
env KindCoercion
co
  = KindCoercion -> KindCoercion
go KindCoercion
co
  where
    go_mco :: MCoercion -> MCoercion
go_mco MCoercion
MRefl    = MCoercion
MRefl
    go_mco (MCo KindCoercion
co) = KindCoercion -> MCoercion
MCo (KindCoercion -> MCoercion) -> KindCoercion -> MCoercion
forall a b. (a -> b) -> a -> b
$! KindCoercion -> KindCoercion
go KindCoercion
co

    go :: KindCoercion -> KindCoercion
go (Refl Type
ty)             = Type -> KindCoercion
Refl (Type -> KindCoercion) -> Type -> KindCoercion
forall a b. (a -> b) -> a -> b
$! TidyEnv -> Type -> Type
tidyType TidyEnv
env Type
ty
    go (GRefl Role
r Type
ty MCoercion
mco)      = (Role -> Type -> MCoercion -> KindCoercion
GRefl Role
r (Type -> MCoercion -> KindCoercion)
-> Type -> MCoercion -> KindCoercion
forall a b. (a -> b) -> a -> b
$! TidyEnv -> Type -> Type
tidyType TidyEnv
env Type
ty) (MCoercion -> KindCoercion) -> MCoercion -> KindCoercion
forall a b. (a -> b) -> a -> b
$! MCoercion -> MCoercion
go_mco MCoercion
mco
    go (TyConAppCo Role
r TyCon
tc [KindCoercion]
cos) = Role -> TyCon -> [KindCoercion] -> KindCoercion
TyConAppCo Role
r TyCon
tc ([KindCoercion] -> KindCoercion) -> [KindCoercion] -> KindCoercion
forall a b. (a -> b) -> a -> b
$! (KindCoercion -> KindCoercion) -> [KindCoercion] -> [KindCoercion]
forall a b. (a -> b) -> [a] -> [b]
strictMap KindCoercion -> KindCoercion
go [KindCoercion]
cos
    go (AppCo KindCoercion
co1 KindCoercion
co2)       = (KindCoercion -> KindCoercion -> KindCoercion
AppCo (KindCoercion -> KindCoercion -> KindCoercion)
-> KindCoercion -> KindCoercion -> KindCoercion
forall a b. (a -> b) -> a -> b
$! KindCoercion -> KindCoercion
go KindCoercion
co1) (KindCoercion -> KindCoercion) -> KindCoercion -> KindCoercion
forall a b. (a -> b) -> a -> b
$! KindCoercion -> KindCoercion
go KindCoercion
co2
    go (ForAllCo TyCoVar
tv ForAllTyFlag
visL ForAllTyFlag
visR KindCoercion
h KindCoercion
co)
      = ((((TyCoVar
-> ForAllTyFlag
-> ForAllTyFlag
-> KindCoercion
-> KindCoercion
-> KindCoercion
ForAllCo (TyCoVar
 -> ForAllTyFlag
 -> ForAllTyFlag
 -> KindCoercion
 -> KindCoercion
 -> KindCoercion)
-> TyCoVar
-> ForAllTyFlag
-> ForAllTyFlag
-> KindCoercion
-> KindCoercion
-> KindCoercion
forall a b. (a -> b) -> a -> b
$! TyCoVar
tvp) (ForAllTyFlag
 -> ForAllTyFlag -> KindCoercion -> KindCoercion -> KindCoercion)
-> ForAllTyFlag
-> ForAllTyFlag
-> KindCoercion
-> KindCoercion
-> KindCoercion
forall a b. (a -> b) -> a -> b
$! ForAllTyFlag
visL) (ForAllTyFlag -> KindCoercion -> KindCoercion -> KindCoercion)
-> ForAllTyFlag -> KindCoercion -> KindCoercion -> KindCoercion
forall a b. (a -> b) -> a -> b
$! ForAllTyFlag
visR) (KindCoercion -> KindCoercion -> KindCoercion)
-> KindCoercion -> KindCoercion -> KindCoercion
forall a b. (a -> b) -> a -> b
$! (KindCoercion -> KindCoercion
go KindCoercion
h)) (KindCoercion -> KindCoercion) -> KindCoercion -> KindCoercion
forall a b. (a -> b) -> a -> b
$! (TidyEnv -> KindCoercion -> KindCoercion
tidyCo TidyEnv
envp KindCoercion
co)
      where (TidyEnv
envp, TyCoVar
tvp) = TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar)
tidyVarBndr TidyEnv
env TyCoVar
tv
            -- the case above duplicates a bit of work in tidying h and the kind
            -- of tv. But the alternative is to use coercionKind, which seems worse.
    go (FunCo Role
r FunTyFlag
afl FunTyFlag
afr KindCoercion
w KindCoercion
co1 KindCoercion
co2) = ((Role
-> FunTyFlag
-> FunTyFlag
-> KindCoercion
-> KindCoercion
-> KindCoercion
-> KindCoercion
FunCo Role
r FunTyFlag
afl FunTyFlag
afr (KindCoercion -> KindCoercion -> KindCoercion -> KindCoercion)
-> KindCoercion -> KindCoercion -> KindCoercion -> KindCoercion
forall a b. (a -> b) -> a -> b
$! KindCoercion -> KindCoercion
go KindCoercion
w) (KindCoercion -> KindCoercion -> KindCoercion)
-> KindCoercion -> KindCoercion -> KindCoercion
forall a b. (a -> b) -> a -> b
$! KindCoercion -> KindCoercion
go KindCoercion
co1) (KindCoercion -> KindCoercion) -> KindCoercion -> KindCoercion
forall a b. (a -> b) -> a -> b
$! KindCoercion -> KindCoercion
go KindCoercion
co2
    go (CoVarCo TyCoVar
cv)          = TyCoVar -> KindCoercion
CoVarCo (TyCoVar -> KindCoercion) -> TyCoVar -> KindCoercion
forall a b. (a -> b) -> a -> b
$! TyCoVar -> TyCoVar
go_cv TyCoVar
cv
    go (HoleCo CoercionHole
h)            = CoercionHole -> KindCoercion
HoleCo (CoercionHole -> KindCoercion) -> CoercionHole -> KindCoercion
forall a b. (a -> b) -> a -> b
$! CoercionHole -> CoercionHole
go_hole CoercionHole
h
    go (AxiomCo CoAxiomRule
ax [KindCoercion]
cos)      = CoAxiomRule -> [KindCoercion] -> KindCoercion
AxiomCo CoAxiomRule
ax ([KindCoercion] -> KindCoercion) -> [KindCoercion] -> KindCoercion
forall a b. (a -> b) -> a -> b
$ (KindCoercion -> KindCoercion) -> [KindCoercion] -> [KindCoercion]
forall a b. (a -> b) -> [a] -> [b]
strictMap KindCoercion -> KindCoercion
go [KindCoercion]
cos
    go (UnivCo UnivCoProvenance
prov Role
role Type
t1 Type
t2 [KindCoercion]
cos)
                             = ((UnivCoProvenance
-> Role -> Type -> Type -> [KindCoercion] -> KindCoercion
UnivCo UnivCoProvenance
prov Role
role
                                (Type -> Type -> [KindCoercion] -> KindCoercion)
-> Type -> Type -> [KindCoercion] -> KindCoercion
forall a b. (a -> b) -> a -> b
$! TidyEnv -> Type -> Type
tidyType TidyEnv
env Type
t1)
                                (Type -> [KindCoercion] -> KindCoercion)
-> Type -> [KindCoercion] -> KindCoercion
forall a b. (a -> b) -> a -> b
$! TidyEnv -> Type -> Type
tidyType TidyEnv
env Type
t2)
                                ([KindCoercion] -> KindCoercion) -> [KindCoercion] -> KindCoercion
forall a b. (a -> b) -> a -> b
$! (KindCoercion -> KindCoercion) -> [KindCoercion] -> [KindCoercion]
forall a b. (a -> b) -> [a] -> [b]
strictMap KindCoercion -> KindCoercion
go [KindCoercion]
cos
    go (SymCo KindCoercion
co)            = KindCoercion -> KindCoercion
SymCo (KindCoercion -> KindCoercion) -> KindCoercion -> KindCoercion
forall a b. (a -> b) -> a -> b
$! KindCoercion -> KindCoercion
go KindCoercion
co
    go (TransCo KindCoercion
co1 KindCoercion
co2)     = (KindCoercion -> KindCoercion -> KindCoercion
TransCo (KindCoercion -> KindCoercion -> KindCoercion)
-> KindCoercion -> KindCoercion -> KindCoercion
forall a b. (a -> b) -> a -> b
$! KindCoercion -> KindCoercion
go KindCoercion
co1) (KindCoercion -> KindCoercion) -> KindCoercion -> KindCoercion
forall a b. (a -> b) -> a -> b
$! KindCoercion -> KindCoercion
go KindCoercion
co2
    go (SelCo CoSel
d KindCoercion
co)          = CoSel -> KindCoercion -> KindCoercion
SelCo CoSel
d (KindCoercion -> KindCoercion) -> KindCoercion -> KindCoercion
forall a b. (a -> b) -> a -> b
$! KindCoercion -> KindCoercion
go KindCoercion
co
    go (LRCo LeftOrRight
lr KindCoercion
co)          = LeftOrRight -> KindCoercion -> KindCoercion
LRCo LeftOrRight
lr (KindCoercion -> KindCoercion) -> KindCoercion -> KindCoercion
forall a b. (a -> b) -> a -> b
$! KindCoercion -> KindCoercion
go KindCoercion
co
    go (InstCo KindCoercion
co KindCoercion
ty)        = (KindCoercion -> KindCoercion -> KindCoercion
InstCo (KindCoercion -> KindCoercion -> KindCoercion)
-> KindCoercion -> KindCoercion -> KindCoercion
forall a b. (a -> b) -> a -> b
$! KindCoercion -> KindCoercion
go KindCoercion
co) (KindCoercion -> KindCoercion) -> KindCoercion -> KindCoercion
forall a b. (a -> b) -> a -> b
$! KindCoercion -> KindCoercion
go KindCoercion
ty
    go (KindCo KindCoercion
co)           = KindCoercion -> KindCoercion
KindCo (KindCoercion -> KindCoercion) -> KindCoercion -> KindCoercion
forall a b. (a -> b) -> a -> b
$! KindCoercion -> KindCoercion
go KindCoercion
co
    go (SubCo KindCoercion
co)            = KindCoercion -> KindCoercion
SubCo (KindCoercion -> KindCoercion) -> KindCoercion -> KindCoercion
forall a b. (a -> b) -> a -> b
$! KindCoercion -> KindCoercion
go KindCoercion
co

    go_cv :: TyCoVar -> TyCoVar
go_cv TyCoVar
cv = TidyEnv -> TyCoVar -> TyCoVar
tidyTyCoVarOcc TidyEnv
env TyCoVar
cv

    go_hole :: CoercionHole -> CoercionHole
go_hole (CoercionHole TyCoVar
cv IORef (Maybe KindCoercion)
r Bool
h) = (TyCoVar -> IORef (Maybe KindCoercion) -> Bool -> CoercionHole
CoercionHole (TyCoVar -> IORef (Maybe KindCoercion) -> Bool -> CoercionHole)
-> TyCoVar -> IORef (Maybe KindCoercion) -> Bool -> CoercionHole
forall a b. (a -> b) -> a -> b
$! TyCoVar -> TyCoVar
go_cv TyCoVar
cv) IORef (Maybe KindCoercion)
r Bool
h
    -- Tidy even the holes; tidied types should have tidied kinds

tidyCos :: TidyEnv -> [Coercion] -> [Coercion]
tidyCos :: TidyEnv -> [KindCoercion] -> [KindCoercion]
tidyCos TidyEnv
env = (KindCoercion -> KindCoercion) -> [KindCoercion] -> [KindCoercion]
forall a b. (a -> b) -> [a] -> [b]
strictMap (TidyEnv -> KindCoercion -> KindCoercion
tidyCo TidyEnv
env)