{-
(c) The University of Glasgow 2006
(c) The AQUA Project, Glasgow University, 1996-1998
-}

-- | Zonking types within the typechecker.
--
-- Distinct from the final zonking pass in "GHC.Tc.Zonk.Type";
-- see Note [Module structure for zonking] in GHC.Tc.Zonk.Type.
module GHC.Tc.Zonk.TcType
  ( -- * Zonking (within the typechecker)

    -- ** The 'ZonkM' monad and 'ZonkGblEnv'
    module GHC.Tc.Zonk.Monad

    -- ** Zonking types
  , zonkTcType, zonkTcTypes, zonkScaledTcType
  , zonkTcTyVar, zonkTcTyVars
  , zonkTcTyVarToTcTyVar, zonkTcTyVarsToTcTyVars
  , zonkInvisTVBinder
  , zonkCo

    -- ** Zonking 'TyCon's
  , zonkTcTyCon

    -- *** FreeVars
  , zonkTcTypeAndFV, zonkTyCoVarsAndFV, zonkTyCoVarsAndFVList
  , zonkDTyCoVarSetAndFV

    -- ** Zonking 'CoVar's and 'Id's
  , zonkId, zonkCoVar, zonkTyCoVar, zonkTyCoVarKind, zonkTyCoVarBndrKind

    -- ** Zonking skolem info
  , zonkSkolemInfo, zonkSkolemInfoAnon

    -- ** Zonking constraints
  , zonkCt, zonkWC, zonkSimples, zonkImplication

    -- * Tidying
  , tcInitTidyEnv, tcInitOpenTidyEnv
  , tidyCt, tidyEvVar, tidyDelayedError

    -- ** Zonk & tidy
  , zonkTidyTcType, zonkTidyTcTypes
  , zonkTidyOrigin, zonkTidyOrigins
  , zonkTidyFRRInfos

    -- * Writing to metavariables
  , writeMetaTyVar, writeMetaTyVarRef

    -- * Handling coercion holes
  , checkCoercionHole

  )
  where

import GHC.Prelude

import GHC.Types.Name
import GHC.Types.Var
import GHC.Types.Var.Env
import GHC.Types.Var.Set
import GHC.Types.Unique.Set

import GHC.Tc.Errors.Types
import GHC.Tc.Errors.Ppr
import GHC.Tc.Types.Constraint
import GHC.Tc.Types.Origin
import GHC.Tc.Types.TcRef
import GHC.Tc.Types.Evidence
import GHC.Tc.Types.BasicTypes
import GHC.Tc.Utils.TcType
import GHC.Tc.Zonk.Monad

import GHC.Core.InstEnv (ClsInst(is_tys))
import GHC.Core.TyCo.Rep
import GHC.Core.TyCon
import GHC.Core.Type
import GHC.Core.Coercion
import GHC.Core.Predicate

import GHC.Utils.Constants
import GHC.Utils.Outputable
import GHC.Utils.Misc
import GHC.Utils.Monad ( mapAccumLM )
import GHC.Utils.Panic

import GHC.Data.Bag
import GHC.Data.Pair

{- *********************************************************************
*                                                                      *
                    Writing to metavariables
*                                                                      *
************************************************************************
-}

-- | Write into a currently-empty MetaTyVar.
--
-- Works with both type and kind variables.
writeMetaTyVar :: HasDebugCallStack
               => TcTyVar -- ^ the type varfiable to write to
               -> TcType  -- ^ the type to write into the mutable reference
               -> ZonkM ()
writeMetaTyVar :: HasDebugCallStack => CoVar -> Type -> ZonkM ()
writeMetaTyVar CoVar
tyvar Type
ty
  | Bool -> Bool
not Bool
debugIsOn
  = HasDebugCallStack => CoVar -> TcRef MetaDetails -> Type -> ZonkM ()
CoVar -> TcRef MetaDetails -> Type -> ZonkM ()
writeMetaTyVarRef CoVar
tyvar (CoVar -> TcRef MetaDetails
metaTyVarRef CoVar
tyvar) Type
ty

-- Everything from here on only happens if DEBUG is on
  | Bool -> Bool
not (CoVar -> Bool
isTcTyVar CoVar
tyvar)
  = Bool -> SDoc -> ZonkM ()
forall (m :: * -> *).
(HasCallStack, Applicative m) =>
Bool -> SDoc -> m ()
massertPpr Bool
False (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Writing to non-tc tyvar" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> CoVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoVar
tyvar)

  | MetaTv { mtv_ref :: TcTyVarDetails -> TcRef MetaDetails
mtv_ref = TcRef MetaDetails
ref } <- CoVar -> TcTyVarDetails
tcTyVarDetails CoVar
tyvar
  = HasDebugCallStack => CoVar -> TcRef MetaDetails -> Type -> ZonkM ()
CoVar -> TcRef MetaDetails -> Type -> ZonkM ()
writeMetaTyVarRef CoVar
tyvar TcRef MetaDetails
ref Type
ty

  | Bool
otherwise
  = Bool -> SDoc -> ZonkM ()
forall (m :: * -> *).
(HasCallStack, Applicative m) =>
Bool -> SDoc -> m ()
massertPpr Bool
False (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Writing to non-meta tyvar" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> CoVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoVar
tyvar)
{-# INLINE writeMetaTyVar #-} -- See NOTE [Inlining writeMetaTyVar]

-- | Write into the 'MetaDetails' mutable references of a 'MetaTv'.
writeMetaTyVarRef :: HasDebugCallStack
                  => TcTyVar -- ^ for debug assertions only;
                  -> TcRef MetaDetails -- ^ ref cell must be for the same tyvar
                  -> TcType -- ^ the type to write to the mutable reference
                  -> ZonkM ()
writeMetaTyVarRef :: HasDebugCallStack => CoVar -> TcRef MetaDetails -> Type -> ZonkM ()
writeMetaTyVarRef CoVar
tyvar TcRef MetaDetails
ref Type
ty
  | Bool -> Bool
not Bool
debugIsOn
  = do { String -> SDoc -> ZonkM ()
traceZonk String
"writeMetaTyVar" (CoVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoVar
tyvar SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (CoVar -> Type
tyVarKind CoVar
tyvar)
                                     SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
":=" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)
       ; TcRef MetaDetails -> MetaDetails -> ZonkM ()
forall (m :: * -> *) a. MonadIO m => TcRef a -> a -> m ()
writeTcRef TcRef MetaDetails
ref (Type -> MetaDetails
Indirect Type
ty) }

  -- Everything from here on only happens if DEBUG is on
  -- Need to zonk 'ty' because we may only recently have promoted
  -- its free meta-tyvars (see GHC.Tc.Utils.Unify.checkPromoteFreeVars)
  | Bool
otherwise
  = do { meta_details <- TcRef MetaDetails -> ZonkM MetaDetails
forall (m :: * -> *) a. MonadIO m => TcRef a -> m a
readTcRef TcRef MetaDetails
ref;
       -- Zonk kinds to allow the error check to work
       ; zonked_tv_kind <- zonkTcType tv_kind
       ; zonked_ty      <- zonkTcType ty
       ; let zonked_ty_kind = HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
zonked_ty
             zonked_ty_lvl  = Type -> TcLevel
tcTypeLevel Type
zonked_ty
             level_check_ok  = Bool -> Bool
not (TcLevel
zonked_ty_lvl TcLevel -> TcLevel -> Bool
`strictlyDeeperThan` TcLevel
tv_lvl)
             level_check_msg = TcLevel -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcLevel
zonked_ty_lvl SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ TcLevel -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcLevel
tv_lvl SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ CoVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoVar
tyvar SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
zonked_ty
             kind_check_ok = Type
zonked_ty_kind HasCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`eqType` Type
zonked_tv_kind
             -- Note [Extra-constraint holes in partial type signatures] in GHC.Tc.Gen.HsType

             kind_msg = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Ill-kinded update to meta tyvar")
                           Int
2 (    CoVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoVar
tyvar SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"::" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
tv_kind SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
zonked_tv_kind)
                              SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
":="
                              SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"::" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
zonked_ty_kind) )

       ; traceZonk "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)

       -- Check for double updates
       ; massertPpr (isFlexi meta_details) (double_upd_msg meta_details)

       -- Check for level OK
       ; massertPpr level_check_ok level_check_msg

       -- Check Kinds ok
       ; massertPpr kind_check_ok kind_msg

       -- Do the write
       ; writeTcRef ref (Indirect ty) }
  where
    tv_kind :: Type
tv_kind = CoVar -> Type
tyVarKind CoVar
tyvar

    tv_lvl :: TcLevel
tv_lvl = CoVar -> TcLevel
tcTyVarLevel CoVar
tyvar


    double_upd_msg :: MetaDetails -> SDoc
double_upd_msg MetaDetails
details = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Double update of meta tyvar")
                                Int
2 (CoVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoVar
tyvar SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ MetaDetails -> SDoc
forall a. Outputable a => a -> SDoc
ppr MetaDetails
details)
{-# INLINE writeMetaTyVarRef #-} -- See NOTE [Inlining writeMetaTyVar]

{- NOTE [Inlining writeMetaTyVar]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
writeMetaTyVar is defined in the ZonkM monad, but it is often used within
TcM with the following idiom:

  liftZonkM $ writeMetaTyVar tv ty

Using liftZonkM within TcM generally means extracting out a ZonkGblEnv
from the TcM monad to pass to the inner ZonkM computation (see the definition
of liftZonkM). This can cause writeMetaTyVar to allocate a ZonkGblEnv, which we
would much rather avoid!
Instead, we should directly pass the bits of the ZonkGblEnv that writeMetaTyVar
needs (the Logger and NamePprCtxt, which are needed for the traceZonk call
in writeMetaTyVar). This is achieved by inlining writeMetaTyVar and writeMetaTyVarRef.
These functions just wrap writeTcRef, with some extra tracing
(and some assertions if running in debug mode), so it's fine to inline them.

See for example test T5631, which regresses without this change.
-}

{-
************************************************************************
*                                                                      *
     Zonking -- the main work-horses: zonkTcType, zonkTcTyVar
*                                                                      *
************************************************************************
-}

zonkScaledTcType :: Scaled TcType -> ZonkM (Scaled TcType)
zonkScaledTcType :: Scaled Type -> ZonkM (Scaled Type)
zonkScaledTcType (Scaled Type
m Type
ty)
  = Type -> Type -> Scaled Type
forall a. Type -> a -> Scaled a
Scaled (Type -> Type -> Scaled Type)
-> ZonkM Type -> ZonkM (Type -> Scaled Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> ZonkM Type
zonkTcType Type
m ZonkM (Type -> Scaled Type) -> ZonkM Type -> ZonkM (Scaled Type)
forall a b. ZonkM (a -> b) -> ZonkM a -> ZonkM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> ZonkM Type
zonkTcType Type
ty

-- For unbound, mutable tyvars, zonkType uses the function given to it
-- For tyvars bound at a for-all, zonkType zonks them to an immutable
--      type variable and zonks the kind too
zonkTcType  :: TcType   -> ZonkM TcType
zonkTcTypes :: [TcType] -> ZonkM [TcType]
zonkCo      :: Coercion -> ZonkM Coercion
(Type -> ZonkM Type
zonkTcType, [Type] -> ZonkM [Type]
zonkTcTypes, Coercion -> ZonkM Coercion
zonkCo, [Coercion] -> ZonkM [Coercion]
_)
  = TyCoMapper () ZonkM
-> (Type -> ZonkM Type, [Type] -> ZonkM [Type],
    Coercion -> ZonkM Coercion, [Coercion] -> ZonkM [Coercion])
forall (m :: * -> *).
Monad m =>
TyCoMapper () m
-> (Type -> m Type, [Type] -> m [Type], Coercion -> m Coercion,
    [Coercion] -> m [Coercion])
mapTyCo TyCoMapper () ZonkM
zonkTcTypeMapper
  where
    -- A suitable TyCoMapper for zonking a type during type-checking,
    -- before all metavars are filled in.
    zonkTcTypeMapper :: TyCoMapper () ZonkM
    zonkTcTypeMapper :: TyCoMapper () ZonkM
zonkTcTypeMapper = TyCoMapper
      { tcm_tyvar :: () -> CoVar -> ZonkM Type
tcm_tyvar = (CoVar -> ZonkM Type) -> () -> CoVar -> ZonkM Type
forall a b. a -> b -> a
const CoVar -> ZonkM Type
zonkTcTyVar
      , tcm_covar :: () -> CoVar -> ZonkM Coercion
tcm_covar = (CoVar -> ZonkM Coercion) -> () -> CoVar -> ZonkM Coercion
forall a b. a -> b -> a
const (\CoVar
cv -> CoVar -> Coercion
mkCoVarCo (CoVar -> Coercion) -> ZonkM CoVar -> ZonkM Coercion
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CoVar -> ZonkM CoVar
zonkTyCoVarKind CoVar
cv)
      , tcm_hole :: () -> CoercionHole -> ZonkM Coercion
tcm_hole  = () -> CoercionHole -> ZonkM Coercion
hole
      , tcm_tycobinder :: forall r.
() -> CoVar -> ForAllTyFlag -> (() -> CoVar -> ZonkM r) -> ZonkM r
tcm_tycobinder = \ ()
_env CoVar
tcv ForAllTyFlag
_vis () -> CoVar -> ZonkM r
k -> CoVar -> ZonkM CoVar
zonkTyCoVarKind CoVar
tcv ZonkM CoVar -> (CoVar -> ZonkM r) -> ZonkM r
forall a b. ZonkM a -> (a -> ZonkM b) -> ZonkM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= () -> CoVar -> ZonkM r
k ()
      , tcm_tycon :: TyCon -> ZonkM TyCon
tcm_tycon      = TyCon -> ZonkM TyCon
zonkTcTyCon }
      where
        hole :: () -> CoercionHole -> ZonkM Coercion
        hole :: () -> CoercionHole -> ZonkM Coercion
hole ()
_ hole :: CoercionHole
hole@(CoercionHole { ch_ref :: CoercionHole -> IORef (Maybe Coercion)
ch_ref = IORef (Maybe Coercion)
ref, ch_co_var :: CoercionHole -> CoVar
ch_co_var = CoVar
cv })
          = do { contents <- IORef (Maybe Coercion) -> ZonkM (Maybe Coercion)
forall (m :: * -> *) a. MonadIO m => TcRef a -> m a
readTcRef IORef (Maybe Coercion)
ref
               ; case contents of
                   Just Coercion
co -> do { co' <- Coercion -> ZonkM Coercion
zonkCo Coercion
co
                                 ; checkCoercionHole cv co' }
                   Maybe Coercion
Nothing -> do { cv' <- CoVar -> ZonkM CoVar
zonkCoVar CoVar
cv
                                 ; return $ HoleCo (hole { ch_co_var = cv' }) } }

zonkTcTyCon :: TcTyCon -> ZonkM TcTyCon
-- Only called on TcTyCons
-- A non-poly TcTyCon may have unification
-- variables that need zonking, but poly ones cannot
zonkTcTyCon :: TyCon -> ZonkM TyCon
zonkTcTyCon TyCon
tc
 | TyCon -> Bool
isMonoTcTyCon TyCon
tc = do { tck' <- Type -> ZonkM Type
zonkTcType (TyCon -> Type
tyConKind TyCon
tc)
                         ; return (setTcTyConKind tc tck') }
 | Bool
otherwise        = TyCon -> ZonkM TyCon
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return TyCon
tc

zonkTcTyVar :: TcTyVar -> ZonkM TcType
-- Simply look through all Flexis
zonkTcTyVar :: CoVar -> ZonkM Type
zonkTcTyVar CoVar
tv
  | CoVar -> Bool
isTcTyVar CoVar
tv
  = case CoVar -> TcTyVarDetails
tcTyVarDetails CoVar
tv of
      SkolemTv {}   -> ZonkM Type
zonk_kind_and_return
      RuntimeUnk {} -> ZonkM Type
zonk_kind_and_return
      MetaTv { mtv_ref :: TcTyVarDetails -> TcRef MetaDetails
mtv_ref = TcRef MetaDetails
ref }
         -> do { cts <- TcRef MetaDetails -> ZonkM MetaDetails
forall (m :: * -> *) a. MonadIO m => TcRef a -> m a
readTcRef TcRef MetaDetails
ref
               ; case cts of
                    MetaDetails
Flexi       -> ZonkM Type
zonk_kind_and_return
                    Indirect Type
ty -> do { zty <- Type -> ZonkM Type
zonkTcType Type
ty
                                      ; writeTcRef ref (Indirect zty)
                                        -- See Note [Sharing in zonking]
                                      ; return zty } }

  | Bool
otherwise -- coercion variable
  = ZonkM Type
zonk_kind_and_return
  where
    zonk_kind_and_return :: ZonkM Type
zonk_kind_and_return = do { z_tv <- CoVar -> ZonkM CoVar
zonkTyCoVarKind CoVar
tv
                              ; return (mkTyVarTy z_tv) }

-- Variant that assumes that any result of zonking is still a TyVar.
-- Should be used only on skolems and TyVarTvs
zonkTcTyVarsToTcTyVars :: HasDebugCallStack => [TcTyVar] -> ZonkM [TcTyVar]
zonkTcTyVarsToTcTyVars :: HasDebugCallStack => [CoVar] -> ZonkM [CoVar]
zonkTcTyVarsToTcTyVars = (CoVar -> ZonkM CoVar) -> [CoVar] -> ZonkM [CoVar]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM HasDebugCallStack => CoVar -> ZonkM CoVar
CoVar -> ZonkM CoVar
zonkTcTyVarToTcTyVar

zonkTcTyVarToTcTyVar :: HasDebugCallStack => TcTyVar -> ZonkM TcTyVar
zonkTcTyVarToTcTyVar :: HasDebugCallStack => CoVar -> ZonkM CoVar
zonkTcTyVarToTcTyVar CoVar
tv
  = do { ty <- CoVar -> ZonkM Type
zonkTcTyVar CoVar
tv
       ; let tv' = case Type -> Maybe CoVar
getTyVar_maybe Type
ty of
                     Just CoVar
tv' -> CoVar
tv'
                     Maybe CoVar
Nothing  -> String -> SDoc -> CoVar
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"zonkTcTyVarToTcTyVar"
                                          (CoVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoVar
tv SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)
       ; return tv' }

zonkInvisTVBinder :: VarBndr TcTyVar spec -> ZonkM (VarBndr TcTyVar spec)
zonkInvisTVBinder :: forall spec. VarBndr CoVar spec -> ZonkM (VarBndr CoVar spec)
zonkInvisTVBinder (Bndr CoVar
tv spec
spec) = do { tv' <- HasDebugCallStack => CoVar -> ZonkM CoVar
CoVar -> ZonkM CoVar
zonkTcTyVarToTcTyVar CoVar
tv
                                      ; return (Bndr tv' spec) }

{- *********************************************************************
*                                                                      *
              Zonking types
*                                                                      *
********************************************************************* -}

zonkTcTypeAndFV :: TcType -> ZonkM DTyCoVarSet
-- Zonk a type and take its free variables
-- With kind polymorphism it can be essential to zonk *first*
-- so that we find the right set of free variables.  Eg
--    forall k1. forall (a:k2). a
-- where k2:=k1 is in the substitution.  We don't want
-- k2 to look free in this type!
zonkTcTypeAndFV :: Type -> ZonkM DTyCoVarSet
zonkTcTypeAndFV Type
ty
  = Type -> DTyCoVarSet
tyCoVarsOfTypeDSet (Type -> DTyCoVarSet) -> ZonkM Type -> ZonkM DTyCoVarSet
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> ZonkM Type
zonkTcType Type
ty

zonkTyCoVar :: TyCoVar -> ZonkM TcType
-- Works on TyVars and TcTyVars
zonkTyCoVar :: CoVar -> ZonkM Type
zonkTyCoVar CoVar
tv | CoVar -> Bool
isTcTyVar CoVar
tv = CoVar -> ZonkM Type
zonkTcTyVar CoVar
tv
               | CoVar -> Bool
isTyVar   CoVar
tv = CoVar -> Type
mkTyVarTy (CoVar -> Type) -> ZonkM CoVar -> ZonkM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CoVar -> ZonkM CoVar
zonkTyCoVarKind CoVar
tv
               | Bool
otherwise    = Bool -> SDoc -> ZonkM Type -> ZonkM Type
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (CoVar -> Bool
isCoVar CoVar
tv) (CoVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoVar
tv) (ZonkM Type -> ZonkM Type) -> ZonkM Type -> ZonkM Type
forall a b. (a -> b) -> a -> b
$
                                Coercion -> Type
mkCoercionTy (Coercion -> Type) -> (CoVar -> Coercion) -> CoVar -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoVar -> Coercion
mkCoVarCo (CoVar -> Type) -> ZonkM CoVar -> ZonkM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CoVar -> ZonkM CoVar
zonkTyCoVarKind CoVar
tv
   -- Hackily, when typechecking type and class decls
   -- we have TyVars in scope added (only) in
   -- GHC.Tc.Gen.HsType.bindTyClTyVars, but it seems
   -- painful to make them into TcTyVars there

zonkTyCoVarsAndFV :: TyCoVarSet -> ZonkM TyCoVarSet
zonkTyCoVarsAndFV :: TyCoVarSet -> ZonkM TyCoVarSet
zonkTyCoVarsAndFV TyCoVarSet
tycovars
  = [Type] -> TyCoVarSet
tyCoVarsOfTypes ([Type] -> TyCoVarSet) -> ZonkM [Type] -> ZonkM TyCoVarSet
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CoVar -> ZonkM Type) -> [CoVar] -> ZonkM [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM CoVar -> ZonkM Type
zonkTyCoVar (TyCoVarSet -> [CoVar]
forall elt. UniqSet elt -> [elt]
nonDetEltsUniqSet TyCoVarSet
tycovars)
  -- It's OK to use nonDetEltsUniqSet here because we immediately forget about
  -- the ordering by turning it into a nondeterministic set and the order
  -- of zonking doesn't matter for determinism.

zonkDTyCoVarSetAndFV :: DTyCoVarSet -> ZonkM DTyCoVarSet
zonkDTyCoVarSetAndFV :: DTyCoVarSet -> ZonkM DTyCoVarSet
zonkDTyCoVarSetAndFV DTyCoVarSet
tycovars
  = [CoVar] -> DTyCoVarSet
mkDVarSet ([CoVar] -> DTyCoVarSet) -> ZonkM [CoVar] -> ZonkM DTyCoVarSet
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([CoVar] -> ZonkM [CoVar]
zonkTyCoVarsAndFVList ([CoVar] -> ZonkM [CoVar]) -> [CoVar] -> ZonkM [CoVar]
forall a b. (a -> b) -> a -> b
$ DTyCoVarSet -> [CoVar]
dVarSetElems DTyCoVarSet
tycovars)

-- Takes a list of TyCoVars, zonks them and returns a
-- deterministically ordered list of their free variables.
zonkTyCoVarsAndFVList :: [TyCoVar] -> ZonkM [TyCoVar]
zonkTyCoVarsAndFVList :: [CoVar] -> ZonkM [CoVar]
zonkTyCoVarsAndFVList [CoVar]
tycovars
  = [Type] -> [CoVar]
tyCoVarsOfTypesList ([Type] -> [CoVar]) -> ZonkM [Type] -> ZonkM [CoVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CoVar -> ZonkM Type) -> [CoVar] -> ZonkM [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM CoVar -> ZonkM Type
zonkTyCoVar [CoVar]
tycovars

zonkTcTyVars :: [TcTyVar] -> ZonkM [TcType]
zonkTcTyVars :: [CoVar] -> ZonkM [Type]
zonkTcTyVars [CoVar]
tyvars = (CoVar -> ZonkM Type) -> [CoVar] -> ZonkM [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM CoVar -> ZonkM Type
zonkTcTyVar [CoVar]
tyvars

-----------------  Types
zonkTyCoVarKind :: TyCoVar -> ZonkM TyCoVar
zonkTyCoVarKind :: CoVar -> ZonkM CoVar
zonkTyCoVarKind CoVar
tv = do { kind' <- Type -> ZonkM Type
zonkTcType (CoVar -> Type
tyVarKind CoVar
tv)
                        ; return (setTyVarKind tv kind') }

zonkTyCoVarBndrKind :: VarBndr TyCoVar flag -> ZonkM (VarBndr TyCoVar flag)
zonkTyCoVarBndrKind :: forall spec. VarBndr CoVar spec -> ZonkM (VarBndr CoVar spec)
zonkTyCoVarBndrKind (Bndr CoVar
tv flag
flag) =
  do { tv' <- CoVar -> ZonkM CoVar
zonkTyCoVarKind CoVar
tv
     ; return (Bndr tv' flag) }

-- | zonkId is used *during* typechecking just to zonk the 'Id''s type
zonkId :: TcId -> ZonkM TcId
zonkId :: CoVar -> ZonkM CoVar
zonkId CoVar
id = (Type -> ZonkM Type) -> CoVar -> ZonkM CoVar
forall (m :: * -> *).
Monad m =>
(Type -> m Type) -> CoVar -> m CoVar
updateIdTypeAndMultM Type -> ZonkM Type
zonkTcType CoVar
id

zonkCoVar :: CoVar -> ZonkM CoVar
zonkCoVar :: CoVar -> ZonkM CoVar
zonkCoVar = CoVar -> ZonkM CoVar
zonkId

{-
************************************************************************
*                                                                      *
        Coercion holes
*                                                                      *
************************************************************************
-}

-- | Check that a coercion is appropriate for filling a hole. (The hole
-- itself is needed only for printing.)
-- Always returns the checked coercion, but this return value is necessary
-- so that the input coercion is forced only when the output is forced.
checkCoercionHole :: CoVar -> Coercion -> ZonkM Coercion
checkCoercionHole :: CoVar -> Coercion -> ZonkM Coercion
checkCoercionHole CoVar
cv Coercion
co
  | Bool
debugIsOn
  = do { cv_ty <- Type -> ZonkM Type
zonkTcType (CoVar -> Type
varType CoVar
cv)
                  -- co is already zonked, but cv might not be
       ; return $
         assertPpr (ok cv_ty)
                   (text "Bad coercion hole" <+>
                    ppr cv <> colon <+> vcat [ ppr t1, ppr t2, ppr role
                                             , ppr cv_ty ])
         co }
  | Bool
otherwise
  = Coercion -> ZonkM Coercion
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return Coercion
co

  where
    (Pair Type
t1 Type
t2, Role
role) = Coercion -> (Pair Type, Role)
coercionKindRole Coercion
co
    ok :: Type -> Bool
ok Type
cv_ty | EqPred EqRel
cv_rel Type
cv_t1 Type
cv_t2 <- Type -> Pred
classifyPredType Type
cv_ty
             =  Type
t1 HasCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`eqType` Type
cv_t1
             Bool -> Bool -> Bool
&& Type
t2 HasCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`eqType` Type
cv_t2
             Bool -> Bool -> Bool
&& Role
role Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== EqRel -> Role
eqRelRole EqRel
cv_rel
             | Bool
otherwise
             = Bool
False


{-
************************************************************************
*                                                                      *
              Zonking constraints
*                                                                      *
************************************************************************
-}

zonkImplication :: Implication -> ZonkM Implication
zonkImplication :: Implication -> ZonkM Implication
zonkImplication implic :: Implication
implic@(Implic { ic_skols :: Implication -> [CoVar]
ic_skols  = [CoVar]
skols
                               , ic_given :: Implication -> [CoVar]
ic_given  = [CoVar]
given
                               , ic_wanted :: Implication -> WantedConstraints
ic_wanted = WantedConstraints
wanted
                               , ic_info :: Implication -> SkolemInfoAnon
ic_info   = SkolemInfoAnon
info })
  = do { skols'  <- (CoVar -> ZonkM CoVar) -> [CoVar] -> ZonkM [CoVar]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM CoVar -> ZonkM CoVar
zonkTyCoVarKind [CoVar]
skols  -- Need to zonk their kinds!
                                                -- as #7230 showed
       ; given'  <- mapM zonkEvVar given
       ; info'   <- zonkSkolemInfoAnon info
       ; wanted' <- zonkWCRec wanted
       ; return (implic { ic_skols  = skols'
                        , ic_given  = given'
                        , ic_wanted = wanted'
                        , ic_info   = info' }) }

zonkEvVar :: EvVar -> ZonkM EvVar
zonkEvVar :: CoVar -> ZonkM CoVar
zonkEvVar CoVar
var = (Type -> ZonkM Type) -> CoVar -> ZonkM CoVar
forall (m :: * -> *).
Monad m =>
(Type -> m Type) -> CoVar -> m CoVar
updateIdTypeAndMultM Type -> ZonkM Type
zonkTcType CoVar
var


zonkWC :: WantedConstraints -> ZonkM WantedConstraints
zonkWC :: WantedConstraints -> ZonkM WantedConstraints
zonkWC WantedConstraints
wc = WantedConstraints -> ZonkM WantedConstraints
zonkWCRec WantedConstraints
wc

zonkWCRec :: WantedConstraints -> ZonkM WantedConstraints
zonkWCRec :: WantedConstraints -> ZonkM WantedConstraints
zonkWCRec (WC { wc_simple :: WantedConstraints -> Bag Ct
wc_simple = Bag Ct
simple, wc_impl :: WantedConstraints -> Bag Implication
wc_impl = Bag Implication
implic, wc_errors :: WantedConstraints -> Bag DelayedError
wc_errors = Bag DelayedError
errs })
  = do { simple' <- Bag Ct -> ZonkM (Bag Ct)
zonkSimples Bag Ct
simple
       ; implic' <- mapBagM zonkImplication implic
       ; errs'   <- mapBagM zonkDelayedError errs
       ; return (WC { wc_simple = simple', wc_impl = implic', wc_errors = errs' }) }

zonkSimples :: Cts -> ZonkM Cts
zonkSimples :: Bag Ct -> ZonkM (Bag Ct)
zonkSimples Bag Ct
cts = do { cts' <- (Ct -> ZonkM Ct) -> Bag Ct -> ZonkM (Bag Ct)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Bag a -> m (Bag b)
mapBagM Ct -> ZonkM Ct
zonkCt Bag Ct
cts
                     ; traceZonk "zonkSimples done:" (ppr cts')
                     ; return cts' }

zonkDelayedError :: DelayedError -> ZonkM DelayedError
zonkDelayedError :: DelayedError -> ZonkM DelayedError
zonkDelayedError (DE_Hole Hole
hole)
  = Hole -> DelayedError
DE_Hole (Hole -> DelayedError) -> ZonkM Hole -> ZonkM DelayedError
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Hole -> ZonkM Hole
zonkHole Hole
hole
zonkDelayedError (DE_NotConcrete NotConcreteError
err)
  = NotConcreteError -> DelayedError
DE_NotConcrete (NotConcreteError -> DelayedError)
-> ZonkM NotConcreteError -> ZonkM DelayedError
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NotConcreteError -> ZonkM NotConcreteError
zonkNotConcreteError NotConcreteError
err
zonkDelayedError (DE_Multiplicity Coercion
mult_co CtLoc
loc)
  = Coercion -> CtLoc -> DelayedError
DE_Multiplicity (Coercion -> CtLoc -> DelayedError)
-> ZonkM Coercion -> ZonkM (CtLoc -> DelayedError)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Coercion -> ZonkM Coercion
zonkCo Coercion
mult_co ZonkM (CtLoc -> DelayedError) -> ZonkM CtLoc -> ZonkM DelayedError
forall a b. ZonkM (a -> b) -> ZonkM a -> ZonkM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> CtLoc -> ZonkM CtLoc
forall a. a -> ZonkM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CtLoc
loc

zonkHole :: Hole -> ZonkM Hole
zonkHole :: Hole -> ZonkM Hole
zonkHole hole :: Hole
hole@(Hole { hole_ty :: Hole -> Type
hole_ty = Type
ty })
  = do { ty' <- Type -> ZonkM Type
zonkTcType Type
ty
       ; return (hole { hole_ty = ty' }) }

zonkNotConcreteError :: NotConcreteError -> ZonkM NotConcreteError
zonkNotConcreteError :: NotConcreteError -> ZonkM NotConcreteError
zonkNotConcreteError err :: NotConcreteError
err@(NCE_FRR { nce_frr_origin :: NotConcreteError -> FixedRuntimeRepOrigin
nce_frr_origin = FixedRuntimeRepOrigin
frr_orig })
  = do { frr_orig  <- FixedRuntimeRepOrigin -> ZonkM FixedRuntimeRepOrigin
zonkFRROrigin FixedRuntimeRepOrigin
frr_orig
       ; return $ err { nce_frr_origin = frr_orig  } }

zonkFRROrigin :: FixedRuntimeRepOrigin -> ZonkM FixedRuntimeRepOrigin
zonkFRROrigin :: FixedRuntimeRepOrigin -> ZonkM FixedRuntimeRepOrigin
zonkFRROrigin (FixedRuntimeRepOrigin Type
ty FixedRuntimeRepContext
orig)
  = do { ty' <- Type -> ZonkM Type
zonkTcType Type
ty
       ; return $ FixedRuntimeRepOrigin ty' orig }

{- Note [zonkCt behaviour]
~~~~~~~~~~~~~~~~~~~~~~~~~~
zonkCt tries to maintain the canonical form of a Ct.  For example,
  - a CDictCan should stay a CDictCan;
  - a CIrredCan should stay a CIrredCan with its cc_reason flag intact

Why?, for example:
- For CDictCan, the @GHC.Tc.Solver.expandSuperClasses@ step, which runs after the
  simple wanted and plugin loop, looks for @CDictCan@s. If a plugin is in use,
  constraints are zonked before being passed to the plugin. This means if we
  don't preserve a canonical form, @expandSuperClasses@ fails to expand
  superclasses. This is what happened in #11525.

- For CIrredCan we want to see if a constraint is insoluble with insolubleWC

On the other hand, we change CEqCan to CNonCanonical, because of all of
CEqCan's invariants, which can break during zonking. (Example: a ~R alpha, where
we have alpha := N Int, where N is a newtype.) Besides, the constraint
will be canonicalised again, so there is little benefit in keeping the
CEqCan structure.

NB: Constraints are always rewritten etc by the canonicaliser in
GHC.Tc.Solver.Solve.solveCt even if they come in as CDictCan. Only canonical
constraints that are actually in the inert set carry all the guarantees. So it
is okay if zonkCt creates e.g. a CDictCan where the cc_tyars are /not/ fully
reduced.
-}

zonkCt :: Ct -> ZonkM Ct
-- See Note [zonkCt behaviour]
zonkCt :: Ct -> ZonkM Ct
zonkCt (CDictCan dict :: DictCt
dict@(DictCt { di_ev :: DictCt -> CtEvidence
di_ev = CtEvidence
ev, di_tys :: DictCt -> [Type]
di_tys = [Type]
args }))
  = do { ev'   <- CtEvidence -> ZonkM CtEvidence
zonkCtEvidence CtEvidence
ev
       ; args' <- mapM zonkTcType args
       ; return (CDictCan (dict { di_ev = ev', di_tys = args' })) }

zonkCt (CEqCan (EqCt { eq_ev :: EqCt -> CtEvidence
eq_ev = CtEvidence
ev }))
  = CtEvidence -> Ct
mkNonCanonical (CtEvidence -> Ct) -> ZonkM CtEvidence -> ZonkM Ct
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CtEvidence -> ZonkM CtEvidence
zonkCtEvidence CtEvidence
ev

zonkCt (CIrredCan ir :: IrredCt
ir@(IrredCt { ir_ev :: IrredCt -> CtEvidence
ir_ev = CtEvidence
ev })) -- Preserve the ir_reason flag
  = do { ev' <- CtEvidence -> ZonkM CtEvidence
zonkCtEvidence CtEvidence
ev
       ; return (CIrredCan (ir { ir_ev = ev' })) }

zonkCt Ct
ct
  = do { fl' <- CtEvidence -> ZonkM CtEvidence
zonkCtEvidence (Ct -> CtEvidence
ctEvidence Ct
ct)
       ; return (mkNonCanonical fl') }

zonkCtEvidence :: CtEvidence -> ZonkM CtEvidence
zonkCtEvidence :: CtEvidence -> ZonkM CtEvidence
zonkCtEvidence CtEvidence
ctev
  = do { let pred :: Type
pred = CtEvidence -> Type
ctev_pred CtEvidence
ctev
       ; pred' <- Type -> ZonkM Type
zonkTcType Type
pred
       ; return (setCtEvPredType ctev pred') }

zonkSkolemInfo :: SkolemInfo -> ZonkM SkolemInfo
zonkSkolemInfo :: SkolemInfo -> ZonkM SkolemInfo
zonkSkolemInfo (SkolemInfo Unique
u SkolemInfoAnon
sk) = Unique -> SkolemInfoAnon -> SkolemInfo
SkolemInfo Unique
u (SkolemInfoAnon -> SkolemInfo)
-> ZonkM SkolemInfoAnon -> ZonkM SkolemInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SkolemInfoAnon -> ZonkM SkolemInfoAnon
zonkSkolemInfoAnon SkolemInfoAnon
sk

zonkSkolemInfoAnon :: SkolemInfoAnon -> ZonkM SkolemInfoAnon
zonkSkolemInfoAnon :: SkolemInfoAnon -> ZonkM SkolemInfoAnon
zonkSkolemInfoAnon (SigSkol UserTypeCtxt
cx Type
ty [(Name, CoVar)]
tv_prs) = do { ty' <- Type -> ZonkM Type
zonkTcType Type
ty
                                               ; return (SigSkol cx ty' tv_prs) }
zonkSkolemInfoAnon (InferSkol [(Name, Type)]
ntys) = do { ntys' <- ((Name, Type) -> ZonkM (Name, Type))
-> [(Name, Type)] -> ZonkM [(Name, Type)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Name, Type) -> ZonkM (Name, Type)
forall {a}. (a, Type) -> ZonkM (a, Type)
do_one [(Name, Type)]
ntys
                                     ; return (InferSkol ntys') }
  where
    do_one :: (a, Type) -> ZonkM (a, Type)
do_one (a
n, Type
ty) = do { ty' <- Type -> ZonkM Type
zonkTcType Type
ty; return (n, ty') }
zonkSkolemInfoAnon SkolemInfoAnon
skol_info = SkolemInfoAnon -> ZonkM SkolemInfoAnon
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return SkolemInfoAnon
skol_info

{- Note [Sharing in zonking]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have
   alpha :-> beta :-> gamma :-> ty
where the ":->" means that the unification variable has been
filled in with Indirect. Then when zonking alpha, it'd be nice
to short-circuit beta too, so we end up with
   alpha :-> zty
   beta  :-> zty
   gamma :-> zty
where zty is the zonked version of ty.  That way, if we come across
beta later, we'll have less work to do.  (And indeed the same for
alpha.)

This is easily achieved: just overwrite (Indirect ty) with (Indirect
zty).  Non-systematic perf comparisons suggest that this is a modest
win.

But c.f Note [Sharing when zonking to Type] in GHC.Tc.Zonk.Type.

%************************************************************************
%*                                                                      *
                 Tidying
*                                                                      *
************************************************************************
-}

tcInitTidyEnv :: ZonkM TidyEnv
-- We initialise the "tidy-env", used for tidying types before printing,
-- by building a reverse map from the in-scope type variables to the
-- OccName that the programmer originally used for them
tcInitTidyEnv :: ZonkM TidyEnv
tcInitTidyEnv
  = do  { ZonkGblEnv { zge_binder_stack = bndrs } <- ZonkM ZonkGblEnv
getZonkGblEnv
        ; go emptyTidyEnv bndrs }
  where
    go :: TidyEnv -> TcBinderStack -> ZonkM TidyEnv
go (TidyOccEnv
env, VarEnv CoVar
subst) []
      = TidyEnv -> ZonkM TidyEnv
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyOccEnv
env, VarEnv CoVar
subst)
    go (TidyOccEnv
env, VarEnv CoVar
subst) (TcBinder
b : TcBinderStack
bs)
      | TcTvBndr Name
name CoVar
tyvar <- TcBinder
b
       = do { let (TidyOccEnv
env', OccName
occ') = TidyOccEnv -> OccName -> (TidyOccEnv, OccName)
tidyOccName TidyOccEnv
env (Name -> OccName
nameOccName Name
name)
                  name' :: Name
name'  = Name -> OccName -> Name
tidyNameOcc Name
name OccName
occ'
                  tyvar1 :: CoVar
tyvar1 = CoVar -> Name -> CoVar
setTyVarName CoVar
tyvar Name
name'
            ; tyvar2 <- HasDebugCallStack => CoVar -> ZonkM CoVar
CoVar -> ZonkM CoVar
zonkTcTyVarToTcTyVar CoVar
tyvar1
              -- Be sure to zonk here!  Tidying applies to zonked
              -- types, so if we don't zonk we may create an
              -- ill-kinded type (#14175)
            ; go (env', extendVarEnv subst tyvar tyvar2) bs }
      | Bool
otherwise
      = TidyEnv -> TcBinderStack -> ZonkM TidyEnv
go (TidyOccEnv
env, VarEnv CoVar
subst) TcBinderStack
bs

-- | Get a 'TidyEnv' that includes mappings for all vars free in the given
-- type. Useful when tidying open types.
tcInitOpenTidyEnv :: [TyCoVar] -> ZonkM TidyEnv
tcInitOpenTidyEnv :: [CoVar] -> ZonkM TidyEnv
tcInitOpenTidyEnv [CoVar]
tvs
  = do { env1 <- ZonkM TidyEnv
tcInitTidyEnv
       ; return (tidyFreeTyCoVars env1 tvs) }

zonkTidyTcType :: TidyEnv -> TcType -> ZonkM (TidyEnv, TcType)
zonkTidyTcType :: TidyEnv -> Type -> ZonkM (TidyEnv, Type)
zonkTidyTcType TidyEnv
env Type
ty = do { ty' <- Type -> ZonkM Type
zonkTcType Type
ty
                           ; return (tidyOpenTypeX env ty') }

zonkTidyTcTypes :: TidyEnv -> [TcType] -> ZonkM (TidyEnv, [TcType])
zonkTidyTcTypes :: TidyEnv -> [Type] -> ZonkM (TidyEnv, [Type])
zonkTidyTcTypes = [Type] -> TidyEnv -> [Type] -> ZonkM (TidyEnv, [Type])
zonkTidyTcTypes' []
  where zonkTidyTcTypes' :: [Type] -> TidyEnv -> [Type] -> ZonkM (TidyEnv, [Type])
zonkTidyTcTypes' [Type]
zs TidyEnv
env [] = (TidyEnv, [Type]) -> ZonkM (TidyEnv, [Type])
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
env, [Type] -> [Type]
forall a. [a] -> [a]
reverse [Type]
zs)
        zonkTidyTcTypes' [Type]
zs TidyEnv
env (Type
ty:[Type]
tys)
          = do { (env', ty') <- TidyEnv -> Type -> ZonkM (TidyEnv, Type)
zonkTidyTcType TidyEnv
env Type
ty
               ; zonkTidyTcTypes' (ty':zs) env' tys }

zonkTidyOrigin :: TidyEnv -> CtOrigin -> ZonkM (TidyEnv, CtOrigin)
zonkTidyOrigin :: TidyEnv -> CtOrigin -> ZonkM (TidyEnv, CtOrigin)
zonkTidyOrigin TidyEnv
env (GivenOrigin SkolemInfoAnon
skol_info)
  = do { skol_info1 <- SkolemInfoAnon -> ZonkM SkolemInfoAnon
zonkSkolemInfoAnon SkolemInfoAnon
skol_info
       ; let skol_info2 = TidyEnv -> SkolemInfoAnon -> SkolemInfoAnon
tidySkolemInfoAnon TidyEnv
env SkolemInfoAnon
skol_info1
       ; return (env, GivenOrigin skol_info2) }
zonkTidyOrigin TidyEnv
env (GivenSCOrigin SkolemInfoAnon
skol_info Int
sc_depth Bool
blocked)
  = do { skol_info1 <- SkolemInfoAnon -> ZonkM SkolemInfoAnon
zonkSkolemInfoAnon SkolemInfoAnon
skol_info
       ; let skol_info2 = TidyEnv -> SkolemInfoAnon -> SkolemInfoAnon
tidySkolemInfoAnon TidyEnv
env SkolemInfoAnon
skol_info1
       ; return (env, GivenSCOrigin skol_info2 sc_depth blocked) }
zonkTidyOrigin TidyEnv
env orig :: CtOrigin
orig@(TypeEqOrigin { uo_actual :: CtOrigin -> Type
uo_actual   = Type
act
                                      , uo_expected :: CtOrigin -> Type
uo_expected = Type
exp })
  = do { (env1, act') <- TidyEnv -> Type -> ZonkM (TidyEnv, Type)
zonkTidyTcType TidyEnv
env  Type
act
       ; (env2, exp') <- zonkTidyTcType env1 exp
       ; return ( env2, orig { uo_actual   = act'
                             , uo_expected = exp' }) }
zonkTidyOrigin TidyEnv
env (KindEqOrigin Type
ty1 Type
ty2 CtOrigin
orig Maybe TypeOrKind
t_or_k)
  = do { (env1, ty1')  <- TidyEnv -> Type -> ZonkM (TidyEnv, Type)
zonkTidyTcType TidyEnv
env  Type
ty1
       ; (env2, ty2')  <- zonkTidyTcType env1 ty2
       ; (env3, orig') <- zonkTidyOrigin env2 orig
       ; return (env3, KindEqOrigin ty1' ty2' orig' t_or_k) }
zonkTidyOrigin TidyEnv
env (FunDepOrigin1 Type
p1 CtOrigin
o1 RealSrcSpan
l1 Type
p2 CtOrigin
o2 RealSrcSpan
l2)
  = do { (env1, p1') <- TidyEnv -> Type -> ZonkM (TidyEnv, Type)
zonkTidyTcType TidyEnv
env  Type
p1
       ; (env2, o1') <- zonkTidyOrigin env1 o1
       ; (env3, p2') <- zonkTidyTcType env2 p2
       ; (env4, o2') <- zonkTidyOrigin env3 o2
       ; return (env4, FunDepOrigin1 p1' o1' l1 p2' o2' l2) }
zonkTidyOrigin TidyEnv
env (FunDepOrigin2 Type
p1 CtOrigin
o1 Type
p2 SrcSpan
l2)
  = do { (env1, p1') <- TidyEnv -> Type -> ZonkM (TidyEnv, Type)
zonkTidyTcType TidyEnv
env  Type
p1
       ; (env2, p2') <- zonkTidyTcType env1 p2
       ; (env3, o1') <- zonkTidyOrigin env2 o1
       ; return (env3, FunDepOrigin2 p1' o1' p2' l2) }
zonkTidyOrigin TidyEnv
env (InjTFOrigin1 Type
pred1 CtOrigin
orig1 RealSrcSpan
loc1 Type
pred2 CtOrigin
orig2 RealSrcSpan
loc2)
  = do { (env1, pred1') <- TidyEnv -> Type -> ZonkM (TidyEnv, Type)
zonkTidyTcType TidyEnv
env  Type
pred1
       ; (env2, orig1') <- zonkTidyOrigin env1 orig1
       ; (env3, pred2') <- zonkTidyTcType env2 pred2
       ; (env4, orig2') <- zonkTidyOrigin env3 orig2
       ; return (env4, InjTFOrigin1 pred1' orig1' loc1 pred2' orig2' loc2) }
zonkTidyOrigin TidyEnv
env (CycleBreakerOrigin CtOrigin
orig)
  = do { (env1, orig') <- TidyEnv -> CtOrigin -> ZonkM (TidyEnv, CtOrigin)
zonkTidyOrigin TidyEnv
env CtOrigin
orig
       ; return (env1, CycleBreakerOrigin orig') }
zonkTidyOrigin TidyEnv
env (InstProvidedOrigin Module
mod ClsInst
cls_inst)
  = do { (env1, is_tys') <- (TidyEnv -> Type -> ZonkM (TidyEnv, Type))
-> TidyEnv -> [Type] -> ZonkM (TidyEnv, [Type])
forall (m :: * -> *) (t :: * -> *) acc x y.
(Monad m, Traversable t) =>
(acc -> x -> m (acc, y)) -> acc -> t x -> m (acc, t y)
mapAccumLM TidyEnv -> Type -> ZonkM (TidyEnv, Type)
zonkTidyTcType TidyEnv
env (ClsInst -> [Type]
is_tys ClsInst
cls_inst)
       ; return (env1, InstProvidedOrigin mod (cls_inst {is_tys = is_tys'})) }
zonkTidyOrigin TidyEnv
env (WantedSuperclassOrigin Type
pty CtOrigin
orig)
  = do { (env1, pty')  <- TidyEnv -> Type -> ZonkM (TidyEnv, Type)
zonkTidyTcType TidyEnv
env Type
pty
       ; (env2, orig') <- zonkTidyOrigin env1 orig
       ; return (env2, WantedSuperclassOrigin pty' orig') }
zonkTidyOrigin TidyEnv
env CtOrigin
orig = (TidyEnv, CtOrigin) -> ZonkM (TidyEnv, CtOrigin)
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
env, CtOrigin
orig)

zonkTidyOrigins :: TidyEnv -> [CtOrigin] -> ZonkM (TidyEnv, [CtOrigin])
zonkTidyOrigins :: TidyEnv -> [CtOrigin] -> ZonkM (TidyEnv, [CtOrigin])
zonkTidyOrigins = (TidyEnv -> CtOrigin -> ZonkM (TidyEnv, CtOrigin))
-> TidyEnv -> [CtOrigin] -> ZonkM (TidyEnv, [CtOrigin])
forall (m :: * -> *) (t :: * -> *) acc x y.
(Monad m, Traversable t) =>
(acc -> x -> m (acc, y)) -> acc -> t x -> m (acc, t y)
mapAccumLM TidyEnv -> CtOrigin -> ZonkM (TidyEnv, CtOrigin)
zonkTidyOrigin

zonkTidyFRRInfos :: TidyEnv
                 -> [FixedRuntimeRepErrorInfo]
                 -> ZonkM (TidyEnv, [FixedRuntimeRepErrorInfo])
zonkTidyFRRInfos :: TidyEnv
-> [FixedRuntimeRepErrorInfo]
-> ZonkM (TidyEnv, [FixedRuntimeRepErrorInfo])
zonkTidyFRRInfos = [FixedRuntimeRepErrorInfo]
-> TidyEnv
-> [FixedRuntimeRepErrorInfo]
-> ZonkM (TidyEnv, [FixedRuntimeRepErrorInfo])
go []
  where
    go :: [FixedRuntimeRepErrorInfo]
-> TidyEnv
-> [FixedRuntimeRepErrorInfo]
-> ZonkM (TidyEnv, [FixedRuntimeRepErrorInfo])
go [FixedRuntimeRepErrorInfo]
zs TidyEnv
env [] = (TidyEnv, [FixedRuntimeRepErrorInfo])
-> ZonkM (TidyEnv, [FixedRuntimeRepErrorInfo])
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
env, [FixedRuntimeRepErrorInfo] -> [FixedRuntimeRepErrorInfo]
forall a. [a] -> [a]
reverse [FixedRuntimeRepErrorInfo]
zs)
    go [FixedRuntimeRepErrorInfo]
zs TidyEnv
env (FRR_Info { frr_info_origin :: FixedRuntimeRepErrorInfo -> FixedRuntimeRepOrigin
frr_info_origin = FixedRuntimeRepOrigin Type
ty FixedRuntimeRepContext
orig
                        , frr_info_not_concrete :: FixedRuntimeRepErrorInfo -> Maybe (CoVar, Type)
frr_info_not_concrete = Maybe (CoVar, Type)
mb_not_conc } : [FixedRuntimeRepErrorInfo]
tys)
      = do { (env, ty) <- TidyEnv -> Type -> ZonkM (TidyEnv, Type)
zonkTidyTcType TidyEnv
env Type
ty
           ; (env, mb_not_conc) <- go_mb_not_conc env mb_not_conc
           ; let info = FRR_Info { frr_info_origin :: FixedRuntimeRepOrigin
frr_info_origin = Type -> FixedRuntimeRepContext -> FixedRuntimeRepOrigin
FixedRuntimeRepOrigin Type
ty FixedRuntimeRepContext
orig
                                 , frr_info_not_concrete :: Maybe (CoVar, Type)
frr_info_not_concrete = Maybe (CoVar, Type)
mb_not_conc }
           ; go (info:zs) env tys }

    go_mb_not_conc :: TidyEnv
-> Maybe (CoVar, Type) -> ZonkM (TidyEnv, Maybe (CoVar, Type))
go_mb_not_conc TidyEnv
env Maybe (CoVar, Type)
Nothing = (TidyEnv, Maybe (CoVar, Type))
-> ZonkM (TidyEnv, Maybe (CoVar, Type))
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
env, Maybe (CoVar, Type)
forall a. Maybe a
Nothing)
    go_mb_not_conc TidyEnv
env (Just (CoVar
tv, Type
ty))
      = do { (env, tv) <- (TidyEnv, CoVar) -> ZonkM (TidyEnv, CoVar)
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return ((TidyEnv, CoVar) -> ZonkM (TidyEnv, CoVar))
-> (TidyEnv, CoVar) -> ZonkM (TidyEnv, CoVar)
forall a b. (a -> b) -> a -> b
$ TidyEnv -> CoVar -> (TidyEnv, CoVar)
tidyFreeTyCoVarX TidyEnv
env CoVar
tv
           ; (env, ty) <- zonkTidyTcType env ty
           ; return (env, Just (tv, ty)) }

----------------
tidyCt :: TidyEnv -> Ct -> Ct
-- Used only in error reporting
tidyCt :: TidyEnv -> Ct -> Ct
tidyCt TidyEnv
env = (CtEvidence -> CtEvidence) -> Ct -> Ct
updCtEvidence (TidyEnv -> CtEvidence -> CtEvidence
tidyCtEvidence TidyEnv
env)

tidyCtEvidence :: TidyEnv -> CtEvidence -> CtEvidence
     -- NB: we do not tidy the ctev_evar field because we don't
     --     show it in error messages
tidyCtEvidence :: TidyEnv -> CtEvidence -> CtEvidence
tidyCtEvidence TidyEnv
env CtEvidence
ctev
  = CtEvidence
ctev { ctev_pred = tidyOpenType env $ ctev_pred ctev }
  -- tidyOpenType: for (beta ~ (forall a. a->a), don't gratuitously
  -- rename the 'forall a' just because of an 'a' in scope somewhere
  -- else entirely.

tidyHole :: TidyEnv -> Hole -> Hole
tidyHole :: TidyEnv -> Hole -> Hole
tidyHole TidyEnv
env h :: Hole
h@(Hole { hole_ty :: Hole -> Type
hole_ty = Type
ty })
  = Hole
h { hole_ty = tidyOpenType env ty }
  -- tidyOpenType: for, say, (b -> (forall a. a->a)), don't gratuitously
  -- rename the 'forall a' just because of an 'a' in scope somewhere
  -- else entirely.

tidyDelayedError :: TidyEnv -> DelayedError -> DelayedError
tidyDelayedError :: TidyEnv -> DelayedError -> DelayedError
tidyDelayedError TidyEnv
env (DE_Hole Hole
hole)       = Hole -> DelayedError
DE_Hole        (Hole -> DelayedError) -> Hole -> DelayedError
forall a b. (a -> b) -> a -> b
$ TidyEnv -> Hole -> Hole
tidyHole TidyEnv
env Hole
hole
tidyDelayedError TidyEnv
env (DE_NotConcrete NotConcreteError
err) = NotConcreteError -> DelayedError
DE_NotConcrete (NotConcreteError -> DelayedError)
-> NotConcreteError -> DelayedError
forall a b. (a -> b) -> a -> b
$ TidyEnv -> NotConcreteError -> NotConcreteError
tidyConcreteError TidyEnv
env NotConcreteError
err
tidyDelayedError TidyEnv
env (DE_Multiplicity Coercion
mult_co CtLoc
loc)
  = Coercion -> CtLoc -> DelayedError
DE_Multiplicity (TidyEnv -> Coercion -> Coercion
tidyCo TidyEnv
env Coercion
mult_co) CtLoc
loc

tidyConcreteError :: TidyEnv -> NotConcreteError -> NotConcreteError
tidyConcreteError :: TidyEnv -> NotConcreteError -> NotConcreteError
tidyConcreteError TidyEnv
env err :: NotConcreteError
err@(NCE_FRR { nce_frr_origin :: NotConcreteError -> FixedRuntimeRepOrigin
nce_frr_origin = FixedRuntimeRepOrigin
frr_orig })
  = NotConcreteError
err { nce_frr_origin = tidyFRROrigin env frr_orig }

tidyFRROrigin :: TidyEnv -> FixedRuntimeRepOrigin -> FixedRuntimeRepOrigin
tidyFRROrigin :: TidyEnv -> FixedRuntimeRepOrigin -> FixedRuntimeRepOrigin
tidyFRROrigin TidyEnv
env (FixedRuntimeRepOrigin Type
ty FixedRuntimeRepContext
orig)
  = Type -> FixedRuntimeRepContext -> FixedRuntimeRepOrigin
FixedRuntimeRepOrigin (TidyEnv -> Type -> Type
tidyType TidyEnv
env Type
ty) FixedRuntimeRepContext
orig
  -- No need for tidyOpenType because all the free tyvars are already tidied

----------------
tidyEvVar :: TidyEnv -> EvVar -> EvVar
tidyEvVar :: TidyEnv -> CoVar -> CoVar
tidyEvVar TidyEnv
env CoVar
var = (Type -> Type) -> CoVar -> CoVar
updateIdTypeAndMult (TidyEnv -> Type -> Type
tidyType TidyEnv
env) CoVar
var
  -- No need for tidyOpenType because all the free tyvars are already tidied