{-
(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
  , 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 :: (() :: Constraint) => CoVar -> Type -> ZonkM ()
writeMetaTyVar CoVar
tyvar Type
ty
  | Bool -> Bool
not Bool
debugIsOn
  = (() :: Constraint) =>
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
  = (() :: Constraint) =>
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 :: (() :: Constraint) =>
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 { MetaDetails
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
       ; Type
zonked_tv_kind <- Type -> ZonkM Type
zonkTcType Type
tv_kind
       ; Type
zonked_ty      <- Type -> ZonkM Type
zonkTcType Type
ty
       ; let zonked_ty_kind :: Type
zonked_ty_kind = (() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
zonked_ty
             zonked_ty_lvl :: TcLevel
zonked_ty_lvl  = Type -> TcLevel
tcTypeLevel Type
zonked_ty
             level_check_ok :: Bool
level_check_ok  = Bool -> Bool
not (TcLevel
zonked_ty_lvl TcLevel -> TcLevel -> Bool
`strictlyDeeperThan` TcLevel
tv_lvl)
             level_check_msg :: SDoc
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 :: Bool
kind_check_ok = Type
zonked_ty_kind Type -> Type -> Bool
`eqType` Type
zonked_tv_kind
             -- Note [Extra-constraint holes in partial type signatures] in GHC.Tc.Gen.HsType

             kind_msg :: SDoc
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) )

       ; 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
<+> 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)

       -- Check for double updates
       ; Bool -> SDoc -> ZonkM ()
forall (m :: * -> *).
(HasCallStack, Applicative m) =>
Bool -> SDoc -> m ()
massertPpr (MetaDetails -> Bool
isFlexi MetaDetails
meta_details) (MetaDetails -> SDoc
double_upd_msg MetaDetails
meta_details)

       -- Check for level OK
       ; Bool -> SDoc -> ZonkM ()
forall (m :: * -> *).
(HasCallStack, Applicative m) =>
Bool -> SDoc -> m ()
massertPpr Bool
level_check_ok SDoc
level_check_msg

       -- Check Kinds ok
       ; Bool -> SDoc -> ZonkM ()
forall (m :: * -> *).
(HasCallStack, Applicative m) =>
Bool -> SDoc -> m ()
massertPpr Bool
kind_check_ok SDoc
kind_msg

       -- Do the write
       ; TcRef MetaDetails -> MetaDetails -> ZonkM ()
forall (m :: * -> *) a. MonadIO m => TcRef a -> a -> m ()
writeTcRef TcRef MetaDetails
ref (Type -> MetaDetails
Indirect Type
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
*                                                                      *
************************************************************************
-}

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

-- | 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 { Maybe Coercion
contents <- IORef (Maybe Coercion) -> ZonkM (Maybe Coercion)
forall (m :: * -> *) a. MonadIO m => TcRef a -> m a
readTcRef IORef (Maybe Coercion)
ref
           ; case Maybe Coercion
contents of
               Just Coercion
co -> do { Coercion
co' <- Coercion -> ZonkM Coercion
zonkCo Coercion
co
                             ; CoVar -> Coercion -> ZonkM Coercion
checkCoercionHole CoVar
cv Coercion
co' }
               Maybe Coercion
Nothing -> do { CoVar
cv' <- CoVar -> ZonkM CoVar
zonkCoVar CoVar
cv
                             ; Coercion -> ZonkM Coercion
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion -> ZonkM Coercion) -> Coercion -> ZonkM Coercion
forall a b. (a -> b) -> a -> b
$ CoercionHole -> Coercion
HoleCo (CoercionHole
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 { Type
tck' <- Type -> ZonkM Type
zonkTcType (TyCon -> Type
tyConKind TyCon
tc)
                         ; TyCon -> ZonkM TyCon
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return (TyCon -> Type -> TyCon
setTcTyConKind TyCon
tc Type
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 { MetaDetails
cts <- TcRef MetaDetails -> ZonkM MetaDetails
forall (m :: * -> *) a. MonadIO m => TcRef a -> m a
readTcRef TcRef MetaDetails
ref
               ; case MetaDetails
cts of
                    MetaDetails
Flexi       -> ZonkM Type
zonk_kind_and_return
                    Indirect Type
ty -> do { Type
zty <- Type -> ZonkM Type
zonkTcType Type
ty
                                      ; TcRef MetaDetails -> MetaDetails -> ZonkM ()
forall (m :: * -> *) a. MonadIO m => TcRef a -> a -> m ()
writeTcRef TcRef MetaDetails
ref (Type -> MetaDetails
Indirect Type
zty)
                                        -- See Note [Sharing in zonking]
                                      ; Type -> ZonkM Type
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
zty } }

  | Bool
otherwise -- coercion variable
  = ZonkM Type
zonk_kind_and_return
  where
    zonk_kind_and_return :: ZonkM Type
zonk_kind_and_return = do { CoVar
z_tv <- CoVar -> ZonkM CoVar
zonkTyCoVarKind CoVar
tv
                              ; Type -> ZonkM Type
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return (CoVar -> Type
mkTyVarTy CoVar
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 :: (() :: Constraint) => [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 (() :: Constraint) => CoVar -> ZonkM CoVar
CoVar -> ZonkM CoVar
zonkTcTyVarToTcTyVar

zonkTcTyVarToTcTyVar :: HasDebugCallStack => TcTyVar -> ZonkM TcTyVar
zonkTcTyVarToTcTyVar :: (() :: Constraint) => CoVar -> ZonkM CoVar
zonkTcTyVarToTcTyVar CoVar
tv
  = do { Type
ty <- CoVar -> ZonkM Type
zonkTcTyVar CoVar
tv
       ; let tv' :: CoVar
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)
       ; CoVar -> ZonkM CoVar
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return CoVar
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 { CoVar
tv' <- (() :: Constraint) => CoVar -> ZonkM CoVar
CoVar -> ZonkM CoVar
zonkTcTyVarToTcTyVar CoVar
tv
                                      ; VarBndr CoVar spec -> ZonkM (VarBndr CoVar spec)
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return (CoVar -> spec -> VarBndr CoVar spec
forall var argf. var -> argf -> VarBndr var argf
Bndr CoVar
tv' spec
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 { Type
kind' <- Type -> ZonkM Type
zonkTcType (CoVar -> Type
tyVarKind CoVar
tv)
                        ; CoVar -> ZonkM CoVar
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return (CoVar -> Type -> CoVar
setTyVarKind CoVar
tv Type
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 { CoVar
tv' <- CoVar -> ZonkM CoVar
zonkTyCoVarKind CoVar
tv
     ; VarBndr CoVar flag -> ZonkM (VarBndr CoVar flag)
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return (CoVar -> flag -> VarBndr CoVar flag
forall var argf. var -> argf -> VarBndr var argf
Bndr CoVar
tv' flag
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 { Type
cv_ty <- Type -> ZonkM Type
zonkTcType (CoVar -> Type
varType CoVar
cv)
                  -- co is already zonked, but cv might not be
       ; Coercion -> ZonkM Coercion
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion -> ZonkM Coercion) -> Coercion -> ZonkM Coercion
forall a b. (a -> b) -> a -> b
$
         Bool -> SDoc -> Coercion -> Coercion
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (Type -> Bool
ok Type
cv_ty)
                   (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Bad coercion hole" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+>
                    CoVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoVar
cv SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> SDoc
forall doc. IsLine doc => doc
colon SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
t1, Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
t2, Role -> SDoc
forall a. Outputable a => a -> SDoc
ppr Role
role
                                             , Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
cv_ty ])
         Coercion
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 Type -> Type -> Bool
`eqType` Type
cv_t1
             Bool -> Bool -> Bool
&& Type
t2 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 { [CoVar]
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
       ; [CoVar]
given'  <- (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
zonkEvVar [CoVar]
given
       ; SkolemInfoAnon
info'   <- SkolemInfoAnon -> ZonkM SkolemInfoAnon
zonkSkolemInfoAnon SkolemInfoAnon
info
       ; WantedConstraints
wanted' <- WantedConstraints -> ZonkM WantedConstraints
zonkWCRec WantedConstraints
wanted
       ; Implication -> ZonkM Implication
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Implication
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 { Bag Ct
simple' <- Bag Ct -> ZonkM (Bag Ct)
zonkSimples Bag Ct
simple
       ; Bag Implication
implic' <- (Implication -> ZonkM Implication)
-> Bag Implication -> ZonkM (Bag Implication)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Bag a -> m (Bag b)
mapBagM Implication -> ZonkM Implication
zonkImplication Bag Implication
implic
       ; Bag DelayedError
errs'   <- (DelayedError -> ZonkM DelayedError)
-> Bag DelayedError -> ZonkM (Bag DelayedError)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Bag a -> m (Bag b)
mapBagM DelayedError -> ZonkM DelayedError
zonkDelayedError Bag DelayedError
errs
       ; WantedConstraints -> ZonkM WantedConstraints
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return (WC { wc_simple :: Bag Ct
wc_simple = Bag Ct
simple', wc_impl :: Bag Implication
wc_impl = Bag Implication
implic', wc_errors :: Bag DelayedError
wc_errors = Bag DelayedError
errs' }) }

zonkSimples :: Cts -> ZonkM Cts
zonkSimples :: Bag Ct -> ZonkM (Bag Ct)
zonkSimples Bag Ct
cts = do { Bag Ct
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
                     ; String -> SDoc -> ZonkM ()
traceZonk String
"zonkSimples done:" (Bag Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bag Ct
cts')
                     ; Bag Ct -> ZonkM (Bag Ct)
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return Bag Ct
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

zonkHole :: Hole -> ZonkM Hole
zonkHole :: Hole -> ZonkM Hole
zonkHole hole :: Hole
hole@(Hole { hole_ty :: Hole -> Type
hole_ty = Type
ty })
  = do { Type
ty' <- Type -> ZonkM Type
zonkTcType Type
ty
       ; Hole -> ZonkM Hole
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Hole
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 { FixedRuntimeRepOrigin
frr_orig  <- FixedRuntimeRepOrigin -> ZonkM FixedRuntimeRepOrigin
zonkFRROrigin FixedRuntimeRepOrigin
frr_orig
       ; NotConcreteError -> ZonkM NotConcreteError
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return (NotConcreteError -> ZonkM NotConcreteError)
-> NotConcreteError -> ZonkM NotConcreteError
forall a b. (a -> b) -> a -> b
$ NotConcreteError
err { nce_frr_origin = frr_orig  } }

zonkFRROrigin :: FixedRuntimeRepOrigin -> ZonkM FixedRuntimeRepOrigin
zonkFRROrigin :: FixedRuntimeRepOrigin -> ZonkM FixedRuntimeRepOrigin
zonkFRROrigin (FixedRuntimeRepOrigin Type
ty FixedRuntimeRepContext
orig)
  = do { Type
ty' <- Type -> ZonkM Type
zonkTcType Type
ty
       ; FixedRuntimeRepOrigin -> ZonkM FixedRuntimeRepOrigin
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return (FixedRuntimeRepOrigin -> ZonkM FixedRuntimeRepOrigin)
-> FixedRuntimeRepOrigin -> ZonkM FixedRuntimeRepOrigin
forall a b. (a -> b) -> a -> b
$ Type -> FixedRuntimeRepContext -> FixedRuntimeRepOrigin
FixedRuntimeRepOrigin Type
ty' FixedRuntimeRepContext
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 { CtEvidence
ev'   <- CtEvidence -> ZonkM CtEvidence
zonkCtEvidence CtEvidence
ev
       ; [Type]
args' <- (Type -> ZonkM Type) -> [Type] -> 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 Type -> ZonkM Type
zonkTcType [Type]
args
       ; Ct -> ZonkM Ct
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return (DictCt -> Ct
CDictCan (DictCt
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 { CtEvidence
ev' <- CtEvidence -> ZonkM CtEvidence
zonkCtEvidence CtEvidence
ev
       ; Ct -> ZonkM Ct
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return (IrredCt -> Ct
CIrredCan (IrredCt
ir { ir_ev = ev' })) }

zonkCt Ct
ct
  = do { CtEvidence
fl' <- CtEvidence -> ZonkM CtEvidence
zonkCtEvidence (Ct -> CtEvidence
ctEvidence Ct
ct)
       ; Ct -> ZonkM Ct
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return (CtEvidence -> Ct
mkNonCanonical CtEvidence
fl') }

zonkCtEvidence :: CtEvidence -> ZonkM CtEvidence
zonkCtEvidence :: CtEvidence -> ZonkM CtEvidence
zonkCtEvidence CtEvidence
ctev
  = do { let pred :: Type
pred = CtEvidence -> Type
ctev_pred CtEvidence
ctev
       ; Type
pred' <- Type -> ZonkM Type
zonkTcType Type
pred
       ; CtEvidence -> ZonkM CtEvidence
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return ((() :: Constraint) => CtEvidence -> Type -> CtEvidence
CtEvidence -> Type -> CtEvidence
setCtEvPredType CtEvidence
ctev Type
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 { Type
ty' <- Type -> ZonkM Type
zonkTcType Type
ty
                                               ; SkolemInfoAnon -> ZonkM SkolemInfoAnon
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return (UserTypeCtxt -> Type -> [(Name, CoVar)] -> SkolemInfoAnon
SigSkol UserTypeCtxt
cx Type
ty' [(Name, CoVar)]
tv_prs) }
zonkSkolemInfoAnon (InferSkol [(Name, Type)]
ntys) = do { [(Name, Type)]
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
                                     ; SkolemInfoAnon -> ZonkM SkolemInfoAnon
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Name, Type)] -> SkolemInfoAnon
InferSkol [(Name, Type)]
ntys') }
  where
    do_one :: (a, Type) -> ZonkM (a, Type)
do_one (a
n, Type
ty) = do { Type
ty' <- Type -> ZonkM Type
zonkTcType Type
ty; (a, Type) -> ZonkM (a, Type)
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return (a
n, Type
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 :: ZonkGblEnv -> TcBinderStack
zge_binder_stack = TcBinderStack
bndrs } <- ZonkM ZonkGblEnv
getZonkGblEnv
        ; TidyEnv -> TcBinderStack -> ZonkM TidyEnv
go TidyEnv
emptyTidyEnv TcBinderStack
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'
            ; CoVar
tyvar2 <- (() :: Constraint) => 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)
            ; TidyEnv -> TcBinderStack -> ZonkM TidyEnv
go (TidyOccEnv
env', VarEnv CoVar -> CoVar -> CoVar -> VarEnv CoVar
forall a. VarEnv a -> CoVar -> a -> VarEnv a
extendVarEnv VarEnv CoVar
subst CoVar
tyvar CoVar
tyvar2) TcBinderStack
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 { TidyEnv
env1 <- ZonkM TidyEnv
tcInitTidyEnv
       ; let env2 :: TidyEnv
env2 = TidyEnv -> [CoVar] -> TidyEnv
tidyFreeTyCoVars TidyEnv
env1 [CoVar]
tvs
       ; TidyEnv -> ZonkM TidyEnv
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return TidyEnv
env2 }

zonkTidyTcType :: TidyEnv -> TcType -> ZonkM (TidyEnv, TcType)
zonkTidyTcType :: TidyEnv -> Type -> ZonkM (TidyEnv, Type)
zonkTidyTcType TidyEnv
env Type
ty = do { Type
ty' <- Type -> ZonkM Type
zonkTcType Type
ty
                           ; (TidyEnv, Type) -> ZonkM (TidyEnv, Type)
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv -> Type -> (TidyEnv, Type)
tidyOpenType TidyEnv
env Type
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 { (TidyEnv
env', Type
ty') <- TidyEnv -> Type -> ZonkM (TidyEnv, Type)
zonkTidyTcType TidyEnv
env Type
ty
               ; [Type] -> TidyEnv -> [Type] -> ZonkM (TidyEnv, [Type])
zonkTidyTcTypes' (Type
ty'Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
zs) TidyEnv
env' [Type]
tys }

zonkTidyOrigin :: TidyEnv -> CtOrigin -> ZonkM (TidyEnv, CtOrigin)
zonkTidyOrigin :: TidyEnv -> CtOrigin -> ZonkM (TidyEnv, CtOrigin)
zonkTidyOrigin TidyEnv
env (GivenOrigin SkolemInfoAnon
skol_info)
  = do { SkolemInfoAnon
skol_info1 <- SkolemInfoAnon -> ZonkM SkolemInfoAnon
zonkSkolemInfoAnon SkolemInfoAnon
skol_info
       ; let skol_info2 :: SkolemInfoAnon
skol_info2 = TidyEnv -> SkolemInfoAnon -> SkolemInfoAnon
tidySkolemInfoAnon TidyEnv
env SkolemInfoAnon
skol_info1
       ; (TidyEnv, CtOrigin) -> ZonkM (TidyEnv, CtOrigin)
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
env, SkolemInfoAnon -> CtOrigin
GivenOrigin SkolemInfoAnon
skol_info2) }
zonkTidyOrigin TidyEnv
env (GivenSCOrigin SkolemInfoAnon
skol_info Int
sc_depth Bool
blocked)
  = do { SkolemInfoAnon
skol_info1 <- SkolemInfoAnon -> ZonkM SkolemInfoAnon
zonkSkolemInfoAnon SkolemInfoAnon
skol_info
       ; let skol_info2 :: SkolemInfoAnon
skol_info2 = TidyEnv -> SkolemInfoAnon -> SkolemInfoAnon
tidySkolemInfoAnon TidyEnv
env SkolemInfoAnon
skol_info1
       ; (TidyEnv, CtOrigin) -> ZonkM (TidyEnv, CtOrigin)
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
env, SkolemInfoAnon -> Int -> Bool -> CtOrigin
GivenSCOrigin SkolemInfoAnon
skol_info2 Int
sc_depth Bool
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 { (TidyEnv
env1, Type
act') <- TidyEnv -> Type -> ZonkM (TidyEnv, Type)
zonkTidyTcType TidyEnv
env  Type
act
       ; (TidyEnv
env2, Type
exp') <- TidyEnv -> Type -> ZonkM (TidyEnv, Type)
zonkTidyTcType TidyEnv
env1 Type
exp
       ; (TidyEnv, CtOrigin) -> ZonkM (TidyEnv, CtOrigin)
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return ( TidyEnv
env2, CtOrigin
orig { uo_actual   = act'
                             , uo_expected = exp' }) }
zonkTidyOrigin TidyEnv
env (KindEqOrigin Type
ty1 Type
ty2 CtOrigin
orig Maybe TypeOrKind
t_or_k)
  = do { (TidyEnv
env1, Type
ty1')  <- TidyEnv -> Type -> ZonkM (TidyEnv, Type)
zonkTidyTcType TidyEnv
env  Type
ty1
       ; (TidyEnv
env2, Type
ty2')  <- TidyEnv -> Type -> ZonkM (TidyEnv, Type)
zonkTidyTcType TidyEnv
env1 Type
ty2
       ; (TidyEnv
env3, CtOrigin
orig') <- TidyEnv -> CtOrigin -> ZonkM (TidyEnv, CtOrigin)
zonkTidyOrigin TidyEnv
env2 CtOrigin
orig
       ; (TidyEnv, CtOrigin) -> ZonkM (TidyEnv, CtOrigin)
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
env3, Type -> Type -> CtOrigin -> Maybe TypeOrKind -> CtOrigin
KindEqOrigin Type
ty1' Type
ty2' CtOrigin
orig' Maybe TypeOrKind
t_or_k) }
zonkTidyOrigin TidyEnv
env (FunDepOrigin1 Type
p1 CtOrigin
o1 RealSrcSpan
l1 Type
p2 CtOrigin
o2 RealSrcSpan
l2)
  = do { (TidyEnv
env1, Type
p1') <- TidyEnv -> Type -> ZonkM (TidyEnv, Type)
zonkTidyTcType TidyEnv
env  Type
p1
       ; (TidyEnv
env2, CtOrigin
o1') <- TidyEnv -> CtOrigin -> ZonkM (TidyEnv, CtOrigin)
zonkTidyOrigin TidyEnv
env1 CtOrigin
o1
       ; (TidyEnv
env3, Type
p2') <- TidyEnv -> Type -> ZonkM (TidyEnv, Type)
zonkTidyTcType TidyEnv
env2 Type
p2
       ; (TidyEnv
env4, CtOrigin
o2') <- TidyEnv -> CtOrigin -> ZonkM (TidyEnv, CtOrigin)
zonkTidyOrigin TidyEnv
env3 CtOrigin
o2
       ; (TidyEnv, CtOrigin) -> ZonkM (TidyEnv, CtOrigin)
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
env4, Type
-> CtOrigin
-> RealSrcSpan
-> Type
-> CtOrigin
-> RealSrcSpan
-> CtOrigin
FunDepOrigin1 Type
p1' CtOrigin
o1' RealSrcSpan
l1 Type
p2' CtOrigin
o2' RealSrcSpan
l2) }
zonkTidyOrigin TidyEnv
env (FunDepOrigin2 Type
p1 CtOrigin
o1 Type
p2 SrcSpan
l2)
  = do { (TidyEnv
env1, Type
p1') <- TidyEnv -> Type -> ZonkM (TidyEnv, Type)
zonkTidyTcType TidyEnv
env  Type
p1
       ; (TidyEnv
env2, Type
p2') <- TidyEnv -> Type -> ZonkM (TidyEnv, Type)
zonkTidyTcType TidyEnv
env1 Type
p2
       ; (TidyEnv
env3, CtOrigin
o1') <- TidyEnv -> CtOrigin -> ZonkM (TidyEnv, CtOrigin)
zonkTidyOrigin TidyEnv
env2 CtOrigin
o1
       ; (TidyEnv, CtOrigin) -> ZonkM (TidyEnv, CtOrigin)
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
env3, Type -> CtOrigin -> Type -> SrcSpan -> CtOrigin
FunDepOrigin2 Type
p1' CtOrigin
o1' Type
p2' SrcSpan
l2) }
zonkTidyOrigin TidyEnv
env (InjTFOrigin1 Type
pred1 CtOrigin
orig1 RealSrcSpan
loc1 Type
pred2 CtOrigin
orig2 RealSrcSpan
loc2)
  = do { (TidyEnv
env1, Type
pred1') <- TidyEnv -> Type -> ZonkM (TidyEnv, Type)
zonkTidyTcType TidyEnv
env  Type
pred1
       ; (TidyEnv
env2, CtOrigin
orig1') <- TidyEnv -> CtOrigin -> ZonkM (TidyEnv, CtOrigin)
zonkTidyOrigin TidyEnv
env1 CtOrigin
orig1
       ; (TidyEnv
env3, Type
pred2') <- TidyEnv -> Type -> ZonkM (TidyEnv, Type)
zonkTidyTcType TidyEnv
env2 Type
pred2
       ; (TidyEnv
env4, CtOrigin
orig2') <- TidyEnv -> CtOrigin -> ZonkM (TidyEnv, CtOrigin)
zonkTidyOrigin TidyEnv
env3 CtOrigin
orig2
       ; (TidyEnv, CtOrigin) -> ZonkM (TidyEnv, CtOrigin)
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
env4, Type
-> CtOrigin
-> RealSrcSpan
-> Type
-> CtOrigin
-> RealSrcSpan
-> CtOrigin
InjTFOrigin1 Type
pred1' CtOrigin
orig1' RealSrcSpan
loc1 Type
pred2' CtOrigin
orig2' RealSrcSpan
loc2) }
zonkTidyOrigin TidyEnv
env (CycleBreakerOrigin CtOrigin
orig)
  = do { (TidyEnv
env1, CtOrigin
orig') <- TidyEnv -> CtOrigin -> ZonkM (TidyEnv, CtOrigin)
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
env1, CtOrigin -> CtOrigin
CycleBreakerOrigin CtOrigin
orig') }
zonkTidyOrigin TidyEnv
env (InstProvidedOrigin Module
mod ClsInst
cls_inst)
  = do { (TidyEnv
env1, [Type]
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)
       ; (TidyEnv, CtOrigin) -> ZonkM (TidyEnv, CtOrigin)
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
env1, Module -> ClsInst -> CtOrigin
InstProvidedOrigin Module
mod (ClsInst
cls_inst {is_tys = is_tys'})) }
zonkTidyOrigin TidyEnv
env (WantedSuperclassOrigin Type
pty CtOrigin
orig)
  = do { (TidyEnv
env1, Type
pty')  <- TidyEnv -> Type -> ZonkM (TidyEnv, Type)
zonkTidyTcType TidyEnv
env Type
pty
       ; (TidyEnv
env2, CtOrigin
orig') <- TidyEnv -> CtOrigin -> ZonkM (TidyEnv, CtOrigin)
zonkTidyOrigin TidyEnv
env1 CtOrigin
orig
       ; (TidyEnv, CtOrigin) -> ZonkM (TidyEnv, CtOrigin)
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
env2, Type -> CtOrigin -> CtOrigin
WantedSuperclassOrigin Type
pty' CtOrigin
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 { (TidyEnv
env, Type
ty) <- TidyEnv -> Type -> ZonkM (TidyEnv, Type)
zonkTidyTcType TidyEnv
env Type
ty
           ; (TidyEnv
env, Maybe (CoVar, Type)
mb_not_conc) <- TidyEnv
-> Maybe (CoVar, Type) -> ZonkM (TidyEnv, Maybe (CoVar, Type))
go_mb_not_conc TidyEnv
env Maybe (CoVar, Type)
mb_not_conc
           ; let info :: FixedRuntimeRepErrorInfo
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 }
           ; [FixedRuntimeRepErrorInfo]
-> TidyEnv
-> [FixedRuntimeRepErrorInfo]
-> ZonkM (TidyEnv, [FixedRuntimeRepErrorInfo])
go (FixedRuntimeRepErrorInfo
infoFixedRuntimeRepErrorInfo
-> [FixedRuntimeRepErrorInfo] -> [FixedRuntimeRepErrorInfo]
forall a. a -> [a] -> [a]
:[FixedRuntimeRepErrorInfo]
zs) TidyEnv
env [FixedRuntimeRepErrorInfo]
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 { (TidyEnv
env, CoVar
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)
tidyOpenTyCoVar TidyEnv
env CoVar
tv
           ; (TidyEnv
env, Type
ty) <- TidyEnv -> Type -> ZonkM (TidyEnv, Type)
zonkTidyTcType TidyEnv
env Type
ty
           ; (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, (CoVar, Type) -> Maybe (CoVar, Type)
forall a. a -> Maybe a
Just (CoVar
tv, Type
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 = tidyType env ty }
  where
    ty :: Type
ty  = CtEvidence -> Type
ctev_pred CtEvidence
ctev

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 = tidyType env ty }

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

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

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