Commit 371dadfb authored by Ben Gamari's avatar Ben Gamari 🐢 Committed by Marge Bot

Break up TyCoRep

This breaks up the monstrous TyCoReps module into several new modules by
topic:

 * TyCoRep: Contains the `Coercion`, `Type`, and related type
   definitions and a few simple predicates but nothing further

 * TyCoPpr: Contains the the pretty-printer logic

 * TyCoFVs: Contains the free variable computations (and
   `tyConAppNeedsKindSig`, although I suspect this should change)

 * TyCoSubst: Contains the substitution logic for types and coercions

 * TyCoTidy: Contains the tidying logic for types

While we are able to eliminate a good number of `SOURCE` imports (and
make a few others smaller) with this change, we must introduce one new
`hs-boot` file for `TyCoPpr` so that `TyCoRep` can define `Outputable`
instances for the types it defines.

Metric Increase:
    haddock.Cabal
    haddock.compiler
parent 2829f6da
......@@ -89,7 +89,8 @@ module Var (
import GhcPrelude
import {-# SOURCE #-} TyCoRep( Type, Kind, pprKind )
import {-# SOURCE #-} TyCoRep( Type, Kind )
import {-# SOURCE #-} TyCoPpr( pprKind )
import {-# SOURCE #-} TcType( TcTyVarDetails, pprTcTyVarDetails, vanillaSkolemTv )
import {-# SOURCE #-} IdInfo( IdDetails, IdInfo, coVarDetails, isCoVarDetails,
vanillaIdInfo, pprIdDetails )
......
......@@ -72,6 +72,7 @@ import VarSet
import Var
import Type
import TyCoRep
import TyCoFVs
import TyCon
import CoAxiom
import FamInstEnv
......
......@@ -49,6 +49,8 @@ import Kind
import Type
import RepType
import TyCoRep -- checks validity of types/coercions
import TyCoSubst
import TyCoFVs
import TyCon
import CoAxiom
import BasicTypes
......@@ -1051,7 +1053,7 @@ lintTyApp fun_ty arg_ty
; in_scope <- getInScope
-- substTy needs the set of tyvars in scope to avoid generating
-- uniques that are already in scope.
-- See Note [The substitution invariant] in TyCoRep
-- See Note [The substitution invariant] in TyCoSubst
; return (substTyWithInScope in_scope [tv] [arg_ty] body_ty) }
| otherwise
......@@ -1495,7 +1497,7 @@ lint_app :: SDoc -> LintedKind -> [(LintedType,LintedKind)] -> LintM Kind
lint_app doc kfn kas
= do { in_scope <- getInScope
-- We need the in_scope set to satisfy the invariant in
-- Note [The substitution invariant] in TyCoRep
-- Note [The substitution invariant] in TyCoSubst
; foldlM (go_app in_scope) kfn kas }
where
fail_msg extra = vcat [ hang (text "Kind application error in") 2 doc
......@@ -1717,7 +1719,7 @@ lintCoercion (ForAllCo tv1 kind_co co)
-- scope. All the free vars of `t2` and `kind_co` should
-- already be in `in_scope`, because they've been
-- linted and `tv2` has the same unique as `tv1`.
-- See Note [The substitution invariant]
-- See Note [The substitution invariant] in TyCoSubst.
unitVarEnv tv1 (TyVarTy tv2 `mkCastTy` mkSymCo kind_co)
tyr = mkInvForAllTy tv2 $
substTy subst t2
......@@ -1748,7 +1750,7 @@ lintCoercion (ForAllCo cv1 kind_co co)
-- scope. All the free vars of `t2` and `kind_co` should
-- already be in `in_scope`, because they've been
-- linted and `cv2` has the same unique as `cv1`.
-- See Note [The substitution invariant]
-- See Note [The substitution invariant] in TyCoSubst.
unitVarEnv cv1 (eta1 `mkTransCo` (mkCoVarCo cv2)
`mkTransCo` (mkSymCo eta2))
tyr = mkTyCoInvForAllTy cv2 $
......
......@@ -79,9 +79,9 @@ import Data.List
--
-- Some invariants apply to how you use the substitution:
--
-- 1. Note [The substitution invariant] in TyCoRep
-- 1. Note [The substitution invariant] in TyCoSubst
--
-- 2. Note [Substitutions apply only once] in TyCoRep
-- 2. Note [Substitutions apply only once] in TyCoSubst
data Subst
= Subst InScopeSet -- Variables in in scope (both Ids and TyVars) /after/
-- applying the substitution
......@@ -89,7 +89,7 @@ data Subst
TvSubstEnv -- Substitution from TyVars to Types
CvSubstEnv -- Substitution from CoVars to Coercions
-- INVARIANT 1: See TyCoRep Note [The substitution invariant]
-- INVARIANT 1: See TyCoSubst Note [The substitution invariant]
-- This is what lets us deal with name capture properly
-- It's a hard invariant to check...
--
......@@ -104,7 +104,7 @@ Note [Extending the Subst]
For a core Subst, which binds Ids as well, we make a different choice for Ids
than we do for TyVars.
For TyVars, see Note [Extending the TCvSubst] with Type.TvSubstEnv
For TyVars, see Note [Extending the TCvSubst] in TyCoSubst.
For Ids, we have a different invariant
The IdSubstEnv is extended *only* when the Unique on an Id changes
......@@ -171,7 +171,7 @@ mkEmptySubst in_scope = Subst in_scope emptyVarEnv emptyVarEnv emptyVarEnv
mkSubst :: InScopeSet -> TvSubstEnv -> CvSubstEnv -> IdSubstEnv -> Subst
mkSubst in_scope tvs cvs ids = Subst in_scope ids tvs cvs
-- | Find the in-scope set: see TyCoRep Note [The substitution invariant]
-- | Find the in-scope set: see TyCoSubst Note [The substitution invariant]
substInScope :: Subst -> InScopeSet
substInScope (Subst in_scope _ _ _) = in_scope
......@@ -181,7 +181,7 @@ zapSubstEnv :: Subst -> Subst
zapSubstEnv (Subst in_scope _ _ _) = Subst in_scope emptyVarEnv emptyVarEnv emptyVarEnv
-- | Add a substitution for an 'Id' to the 'Subst': you must ensure that the in-scope set is
-- such that TyCoRep Note [The substitution invariant]
-- such that TyCoSubst Note [The substitution invariant]
-- holds after extending the substitution like this
extendIdSubst :: Subst -> Id -> CoreExpr -> Subst
-- ToDo: add an ASSERT that fvs(subst-result) is already in the in-scope set
......@@ -198,7 +198,7 @@ extendIdSubstList (Subst in_scope ids tvs cvs) prs
-- | Add a substitution for a 'TyVar' to the 'Subst'
-- The 'TyVar' *must* be a real TyVar, and not a CoVar
-- You must ensure that the in-scope set is such that
-- TyCoRep Note [The substitution invariant] holds
-- TyCoSubst Note [The substitution invariant] holds
-- after extending the substitution like this.
extendTvSubst :: Subst -> TyVar -> Type -> Subst
extendTvSubst (Subst in_scope ids tvs cvs) tv ty
......@@ -214,7 +214,7 @@ extendTvSubstList subst vrs
-- | Add a substitution from a 'CoVar' to a 'Coercion' to the 'Subst':
-- you must ensure that the in-scope set satisfies
-- TyCoRep Note [The substitution invariant]
-- TyCoSubst Note [The substitution invariant]
-- after extending the substitution like this
extendCvSubst :: Subst -> CoVar -> Coercion -> Subst
extendCvSubst (Subst in_scope ids tvs cvs) v r
......@@ -339,7 +339,7 @@ instance Outputable Subst where
-- | Apply a substitution to an entire 'CoreExpr'. Remember, you may only
-- apply the substitution /once/:
-- see Note [Substitutions apply only once] in TyCoRep
-- See Note [Substitutions apply only once] in TyCoSubst
--
-- Do *not* attempt to short-cut in the case of an empty substitution!
-- See Note [Extending the Subst]
......
......@@ -547,6 +547,10 @@ Library
Kind
Type
TyCoRep
TyCoFVs
TyCoSubst
TyCoPpr
TyCoTidy
Unify
Bag
Binary
......
......@@ -106,6 +106,7 @@ import TcEvidence
import RdrName
import Var
import TyCoRep
import TyCoFVs ( tyConAppNeedsKindSig )
import Type ( appTyArgFlags, splitAppTys, tyConArgFlags )
import TysWiredIn ( unitTy )
import TcType
......
......@@ -1075,7 +1075,7 @@ pprIfaceSigmaType show_forall ty
pprUserIfaceForAll :: [IfaceForAllBndr] -> SDoc
pprUserIfaceForAll tvs
= sdocWithDynFlags $ \dflags ->
-- See Note [When to print foralls]
-- See Note [When to print foralls] in this module.
ppWhen (any tv_has_kind_var tvs
|| any tv_is_required tvs
|| gopt Opt_PrintExplicitForalls dflags) $
......
......@@ -35,6 +35,7 @@ import Type
import Coercion
import CoAxiom
import TyCoRep -- needs to build types & coercions in a knot
import TyCoSubst ( substTyCoVars )
import HscTypes
import Annotations
import InstEnv
......
......@@ -68,6 +68,7 @@ import Var
import VarEnv
import VarSet
import TyCoRep
import TyCoTidy ( tidyCo )
import Demand ( isTopSig )
import Data.Maybe ( catMaybes )
......
......@@ -72,7 +72,7 @@ extendInScope :: Id -> Subst -> Subst
extendInScope id (Subst in_scope env) = Subst (in_scope `extendInScopeSet` id) env
-- | Add a substitution for an 'Id' to the 'Subst': you must ensure that the
-- in-scope set is such that TyCORep Note [The substitution invariant]
-- in-scope set is such that TyCoSubst Note [The substitution invariant]
-- holds after extending the substitution like this.
extendSubst :: Id -> Id -> Subst -> Subst
extendSubst id new_id (Subst in_scope env)
......
......@@ -56,6 +56,7 @@ import NameSet
import RdrName
import TyCon
import TyCoRep
import TyCoSubst (substTyWithInScope)
import Type
import TcEvidence
import VarSet
......
......@@ -397,7 +397,7 @@ tcCheckPatSynDecl psb@PSB{ psb_id = lname@(dL->L _ name), psb_args = details
-- satisfy the substitution invariant. There's no need to
-- add 'ex_tvs' as they are already in the domain of the
-- substitution.
-- See also Note [The substitution invariant] in TyCoRep.
-- See also Note [The substitution invariant] in TyCoSubst.
; prov_dicts <- mapM (emitWanted (ProvCtxtOrigin psb)) prov_theta'
; args' <- zipWithM (tc_arg subst) arg_names arg_tys
; return (ex_tvs', prov_dicts, args') }
......
......@@ -74,6 +74,7 @@ import TcMType
import TcHsType
import TcIface
import TyCoRep
import TyCoFVs ( tyConAppNeedsKindSig )
import FamInst
import FamInstEnv
import InstEnv
......
......@@ -196,6 +196,9 @@ import GhcPrelude
import Kind
import TyCoRep
import TyCoSubst ( mkTvSubst, substTyWithCoVars )
import TyCoFVs
import TyCoPpr ( pprParendTheta )
import Class
import Var
import ForeignCall
......
......@@ -26,7 +26,8 @@ module Class (
import GhcPrelude
import {-# SOURCE #-} TyCon ( TyCon )
import {-# SOURCE #-} TyCoRep ( Type, PredType, pprType )
import {-# SOURCE #-} TyCoRep ( Type, PredType )
import {-# SOURCE #-} TyCoPpr ( pprType )
import Var
import Name
import BasicTypes
......
......@@ -31,7 +31,8 @@ module CoAxiom (
import GhcPrelude
import {-# SOURCE #-} TyCoRep ( Type, pprType )
import {-# SOURCE #-} TyCoRep ( Type )
import {-# SOURCE #-} TyCoPpr ( pprType )
import {-# SOURCE #-} TyCon ( TyCon )
import Outputable
import FastString
......
......@@ -120,6 +120,10 @@ import GhcPrelude
import IfaceType
import TyCoRep
import TyCoFVs
import TyCoPpr
import TyCoSubst
import TyCoTidy
import Type
import TyCon
import CoAxiom
......
......@@ -10,6 +10,7 @@ import GhcPrelude
import DynFlags
import TyCoRep
import TyCoSubst
import Coercion
import Type hiding( substTyVarBndr, substTy )
import TcType ( exactTyCoVarsOfType )
......
This diff is collapsed.
This diff is collapsed.
module TyCoPpr where
import {-# SOURCE #-} TyCoRep (Type, Kind, Coercion, TyLit)
import Outputable
pprType :: Type -> SDoc
pprKind :: Kind -> SDoc
pprCo :: Coercion -> SDoc
pprTyLit :: TyLit -> SDoc
This source diff could not be displayed because it is too large. You can view the blob instead.
......@@ -2,7 +2,6 @@ module TyCoRep where
import GhcPrelude
import Outputable ( SDoc )
import Data.Data ( Data )
import {-# SOURCE #-} Var( Var, ArgFlag, AnonArgFlag )
......@@ -10,7 +9,6 @@ data Type
data TyThing
data Coercion
data UnivCoProvenance
data TCvSubst
data TyLit
data TyCoBinder
data MCoercion
......@@ -21,8 +19,6 @@ type ThetaType = [PredType]
type CoercionN = Coercion
type MCoercionN = MCoercion
pprKind :: Kind -> SDoc
pprType :: Type -> SDoc
mkFunTy :: AnonArgFlag -> Type -> Type -> Type
mkForAllTy :: Var -> ArgFlag -> Type -> Type
......
This diff is collapsed.
{-# LANGUAGE BangPatterns #-}
-- | Tidying types and coercions for printing in error messages.
module TyCoTidy
(
-- * Tidying type related things up for printing
tidyType, tidyTypes,
tidyOpenType, tidyOpenTypes,
tidyOpenKind,
tidyVarBndr, tidyVarBndrs, tidyFreeTyCoVars, avoidNameClashes,
tidyOpenTyCoVar, tidyOpenTyCoVars,
tidyTyCoVarOcc,
tidyTopType,
tidyKind,
tidyCo, tidyCos,
tidyTyCoVarBinder, tidyTyCoVarBinders
) where
import GhcPrelude
import TyCoRep
import TyCoFVs (tyCoVarsOfTypesWellScoped, tyCoVarsOfTypeList)
import Name hiding (varName)
import Var
import VarEnv
import Util (seqList)
import Data.List
{-
%************************************************************************
%* *
\subsection{TidyType}
%* *
%************************************************************************
-}
-- | This tidies up a type for printing in an error message, or in
-- an interface file.
--
-- It doesn't change the uniques at all, just the print names.
tidyVarBndrs :: TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar])
tidyVarBndrs tidy_env tvs
= mapAccumL tidyVarBndr (avoidNameClashes tvs tidy_env) tvs
tidyVarBndr :: TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar)
tidyVarBndr tidy_env@(occ_env, subst) var
= case tidyOccName occ_env (getHelpfulOccName var) of
(occ_env', occ') -> ((occ_env', subst'), var')
where
subst' = extendVarEnv subst var var'
var' = setVarType (setVarName var name') type'
type' = tidyType tidy_env (varType var)
name' = tidyNameOcc name occ'
name = varName var
avoidNameClashes :: [TyCoVar] -> TidyEnv -> TidyEnv
-- Seed the occ_env with clashes among the names, see
-- Note [Tidying multiple names at once] in OccName
avoidNameClashes tvs (occ_env, subst)
= (avoidClashesOccEnv occ_env occs, subst)
where
occs = map getHelpfulOccName tvs
getHelpfulOccName :: TyCoVar -> OccName
-- A TcTyVar with a System Name is probably a
-- unification variable; when we tidy them we give them a trailing
-- "0" (or 1 etc) so that they don't take precedence for the
-- un-modified name. Plus, indicating a unification variable in
-- this way is a helpful clue for users
getHelpfulOccName tv
| isSystemName name, isTcTyVar tv
= mkTyVarOcc (occNameString occ ++ "0")
| otherwise
= occ
where
name = varName tv
occ = getOccName name
tidyTyCoVarBinder :: TidyEnv -> VarBndr TyCoVar vis
-> (TidyEnv, VarBndr TyCoVar vis)
tidyTyCoVarBinder tidy_env (Bndr tv vis)
= (tidy_env', Bndr tv' vis)
where
(tidy_env', tv') = tidyVarBndr tidy_env tv
tidyTyCoVarBinders :: TidyEnv -> [VarBndr TyCoVar vis]
-> (TidyEnv, [VarBndr TyCoVar vis])
tidyTyCoVarBinders tidy_env tvbs
= mapAccumL tidyTyCoVarBinder
(avoidNameClashes (binderVars tvbs) tidy_env) tvbs
---------------
tidyFreeTyCoVars :: TidyEnv -> [TyCoVar] -> TidyEnv
-- ^ Add the free 'TyVar's to the env in tidy form,
-- so that we can tidy the type they are free in
tidyFreeTyCoVars (full_occ_env, var_env) tyvars
= fst (tidyOpenTyCoVars (full_occ_env, var_env) tyvars)
---------------
tidyOpenTyCoVars :: TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar])
tidyOpenTyCoVars env tyvars = mapAccumL tidyOpenTyCoVar env tyvars
---------------
tidyOpenTyCoVar :: TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar)
-- ^ Treat a new 'TyCoVar' as a binder, and give it a fresh tidy name
-- using the environment if one has not already been allocated. See
-- also 'tidyVarBndr'
tidyOpenTyCoVar env@(_, subst) tyvar
= case lookupVarEnv subst tyvar of
Just tyvar' -> (env, tyvar') -- Already substituted
Nothing ->
let env' = tidyFreeTyCoVars env (tyCoVarsOfTypeList (tyVarKind tyvar))
in tidyVarBndr env' tyvar -- Treat it as a binder
---------------
tidyTyCoVarOcc :: TidyEnv -> TyCoVar -> TyCoVar
tidyTyCoVarOcc env@(_, subst) tv
= case lookupVarEnv subst tv of
Nothing -> updateVarType (tidyType env) tv
Just tv' -> tv'
---------------
tidyTypes :: TidyEnv -> [Type] -> [Type]
tidyTypes env tys = map (tidyType env) tys
---------------
tidyType :: TidyEnv -> Type -> Type
tidyType _ (LitTy n) = LitTy n
tidyType env (TyVarTy tv) = TyVarTy (tidyTyCoVarOcc env tv)
tidyType env (TyConApp tycon tys) = let args = tidyTypes env tys
in args `seqList` TyConApp tycon args
tidyType env (AppTy fun arg) = (AppTy $! (tidyType env fun)) $! (tidyType env arg)
tidyType env ty@(FunTy _ arg res) = let { !arg' = tidyType env arg
; !res' = tidyType env res }
in ty { ft_arg = arg', ft_res = res' }
tidyType env (ty@(ForAllTy{})) = mkForAllTys' (zip tvs' vis) $! tidyType env' body_ty
where
(tvs, vis, body_ty) = splitForAllTys' ty
(env', tvs') = tidyVarBndrs env tvs
tidyType env (CastTy ty co) = (CastTy $! tidyType env ty) $! (tidyCo env co)
tidyType env (CoercionTy co) = CoercionTy $! (tidyCo env co)
-- The following two functions differ from mkForAllTys and splitForAllTys in that
-- they expect/preserve the ArgFlag argument. Thes belong to types/Type.hs, but
-- how should they be named?
mkForAllTys' :: [(TyCoVar, ArgFlag)] -> Type -> Type
mkForAllTys' tvvs ty = foldr strictMkForAllTy ty tvvs
where
strictMkForAllTy (tv,vis) ty = (ForAllTy $! ((Bndr $! tv) $! vis)) $! ty
splitForAllTys' :: Type -> ([TyCoVar], [ArgFlag], Type)
splitForAllTys' ty = go ty [] []
where
go (ForAllTy (Bndr tv vis) ty) tvs viss = go ty (tv:tvs) (vis:viss)
go ty tvs viss = (reverse tvs, reverse viss, ty)
---------------
-- | Grabs the free type variables, tidies them
-- and then uses 'tidyType' to work over the type itself
tidyOpenTypes :: TidyEnv -> [Type] -> (TidyEnv, [Type])
tidyOpenTypes env tys
= (env', tidyTypes (trimmed_occ_env, var_env) tys)
where
(env'@(_, var_env), tvs') = tidyOpenTyCoVars env $
tyCoVarsOfTypesWellScoped tys
trimmed_occ_env = initTidyOccEnv (map getOccName tvs')
-- The idea here was that we restrict the new TidyEnv to the
-- _free_ vars of the types, so that we don't gratuitously rename
-- the _bound_ variables of the types.
---------------
tidyOpenType :: TidyEnv -> Type -> (TidyEnv, Type)
tidyOpenType env ty = let (env', [ty']) = tidyOpenTypes env [ty] in
(env', ty')
---------------
-- | Calls 'tidyType' on a top-level type (i.e. with an empty tidying environment)
tidyTopType :: Type -> Type
tidyTopType ty = tidyType emptyTidyEnv ty
---------------
tidyOpenKind :: TidyEnv -> Kind -> (TidyEnv, Kind)
tidyOpenKind = tidyOpenType
tidyKind :: TidyEnv -> Kind -> Kind
tidyKind = tidyType
----------------
tidyCo :: TidyEnv -> Coercion -> Coercion
tidyCo env@(_, subst) co
= go co
where
go_mco MRefl = MRefl
go_mco (MCo co) = MCo (go co)
go (Refl ty) = Refl (tidyType env ty)
go (GRefl r ty mco) = GRefl r (tidyType env ty) $! go_mco mco
go (TyConAppCo r tc cos) = let args = map go cos
in args `seqList` TyConAppCo r tc args
go (AppCo co1 co2) = (AppCo $! go co1) $! go co2
go (ForAllCo tv h co) = ((ForAllCo $! tvp) $! (go h)) $! (tidyCo envp co)
where (envp, tvp) = tidyVarBndr env tv
-- the case above duplicates a bit of work in tidying h and the kind
-- of tv. But the alternative is to use coercionKind, which seems worse.
go (FunCo r co1 co2) = (FunCo r $! go co1) $! go co2
go (CoVarCo cv) = case lookupVarEnv subst cv of
Nothing -> CoVarCo cv
Just cv' -> CoVarCo cv'
go (HoleCo h) = HoleCo h
go (AxiomInstCo con ind cos) = let args = map go cos
in args `seqList` AxiomInstCo con ind args
go (UnivCo p r t1 t2) = (((UnivCo $! (go_prov p)) $! r) $!
tidyType env t1) $! tidyType env t2
go (SymCo co) = SymCo $! go co
go (TransCo co1 co2) = (TransCo $! go co1) $! go co2
go (NthCo r d co) = NthCo r d $! go co
go (LRCo lr co) = LRCo lr $! go co
go (InstCo co ty) = (InstCo $! go co) $! go ty
go (KindCo co) = KindCo $! go co
go (SubCo co) = SubCo $! go co
go (AxiomRuleCo ax cos) = let cos1 = tidyCos env cos
in cos1 `seqList` AxiomRuleCo ax cos1
go_prov UnsafeCoerceProv = UnsafeCoerceProv
go_prov (PhantomProv co) = PhantomProv (go co)
go_prov (ProofIrrelProv co) = ProofIrrelProv (go co)
go_prov p@(PluginProv _) = p
tidyCos :: TidyEnv -> [Coercion] -> [Coercion]
tidyCos env = map (tidyCo env)
......@@ -132,7 +132,8 @@ module TyCon(
import GhcPrelude
import {-# SOURCE #-} TyCoRep ( Kind, Type, PredType, pprType, mkForAllTy, mkFunTy )
import {-# SOURCE #-} TyCoRep ( Kind, Type, PredType, mkForAllTy, mkFunTy )
import {-# SOURCE #-} TyCoPpr ( pprType )
import {-# SOURCE #-} TysWiredIn ( runtimeRepTyCon, constraintKind
, vecCountTyCon, vecElemTyCon, liftedTypeKind )
import {-# SOURCE #-} DataCon ( DataCon, dataConExTyCoVars, dataConFieldLabels
......
......@@ -214,7 +214,7 @@ module Type (
pprTheta, pprThetaArrowTy, pprClassPred,
pprKind, pprParendKind, pprSourceTyCon,
PprPrec(..), topPrec, sigPrec, opPrec, funPrec, appPrec, maybeParen,
pprTyVar, pprTyVars,
pprTyVar, pprTyVars, debugPprType,
pprWithTYPE,
-- * Tidying type related things up for printing
......@@ -240,6 +240,10 @@ import BasicTypes
import Kind
import TyCoRep
import TyCoSubst
import TyCoTidy
import TyCoPpr
import TyCoFVs
-- friends:
import Var
......@@ -365,7 +369,7 @@ tcView (TyConApp tc tys) | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc tys
= Just (mkAppTys (substTy (mkTvSubstPrs tenv) rhs) tys')
-- The free vars of 'rhs' should all be bound by 'tenv', so it's
-- ok to use 'substTy' here.
-- See also Note [The substitution invariant] in TyCoRep.
-- See also Note [The substitution invariant] in TyCoSubst.
-- Its important to use mkAppTys, rather than (foldl AppTy),
-- because the function part might well return a
-- partially-applied type constructor; indeed, usually will!
......@@ -2105,108 +2109,6 @@ predTypeEqRel ty
| otherwise
= NomEq
{-
%************************************************************************
%* *
Well-scoped tyvars
* *
************************************************************************
Note [ScopedSort]
~~~~~~~~~~~~~~~~~
Consider
foo :: Proxy a -> Proxy (b :: k) -> Proxy (a :: k2) -> ()
This function type is implicitly generalised over [a, b, k, k2]. These
variables will be Specified; that is, they will be available for visible
type application. This is because they are written in the type signature
by the user.
However, we must ask: what order will they appear in? In cases without
dependency, this is easy: we just use the lexical left-to-right ordering
of first occurrence. With dependency, we cannot get off the hook so
easily.
We thus state:
* These variables appear in the order as given by ScopedSort, where
the input to ScopedSort is the left-to-right order of first occurrence.
Note that this applies only to *implicit* quantification, without a
`forall`. If the user writes a `forall`, then we just use the order given.
ScopedSort is defined thusly (as proposed in #15743):
* Work left-to-right through the input list, with a cursor.
* If variable v at the cursor is depended on by any earlier variable w,
move v immediately before the leftmost such w.
INVARIANT: The prefix of variables before the cursor form a valid telescope.
Note that ScopedSort makes sense only after type inference is done and all
types/kinds are fully settled and zonked.
-}
-- | Do a topological sort on a list of tyvars,
-- so that binders occur before occurrences
-- E.g. given [ a::k, k::*, b::k ]
-- it'll return a well-scoped list [ k::*, a::k, b::k ]
--
-- This is a deterministic sorting operation
-- (that is, doesn't depend on Uniques).
--
-- It is also meant to be stable: that is, variables should not
-- be reordered unnecessarily. This is specified in Note [ScopedSort]
-- See also Note [Ordering of implicit variables] in RnTypes
scopedSort :: [TyCoVar] -> [TyCoVar]
scopedSort = go [] []
where
go :: [TyCoVar] -- already sorted, in reverse order
-> [TyCoVarSet] -- each set contains all the variables which must be placed
-- before the tv corresponding to the set; they are accumulations
-- of the fvs in the sorted tvs' kinds
-- This list is in 1-to-1 correspondence with the sorted tyvars
-- INVARIANT:
-- all (\tl -> all (`subVarSet` head tl) (tail tl)) (tails fv_list)
-- That is, each set in the list is a superset of all later sets.
-> [TyCoVar] -- yet to be sorted
-> [TyCoVar]
go acc _fv_list [] = reverse acc
go acc fv_list (tv:tvs)
= go acc' fv_list' tvs
where
(acc', fv_list') = insert tv acc fv_list
insert :: TyCoVar -- var to insert
-> [TyCoVar] -- sorted list, in reverse order
-> [TyCoVarSet] -- list of fvs, as above
-> ([TyCoVar], [TyCoVarSet]) -- augmented lists
insert tv [] [] = ([tv], [tyCoVarsOfType (tyVarKind tv)])
insert tv (a:as) (fvs:fvss)
| tv `elemVarSet` fvs
, (as', fvss') <- insert tv as fvss
= (a:as', fvs `unionVarSet` fv_tv : fvss')
| otherwise
= (tv:a:as, fvs `unionVarSet` fv_tv : fvs : fvss)
where
fv_tv = tyCoVarsOfType (tyVarKind tv)
-- lists not in correspondence
insert _ _ _ = panic "scopedSort"
-- | Get the free vars of a type in scoped order
tyCoVarsOfTypeWellScoped :: Type -> [TyVar]
tyCoVarsOfTypeWellScoped = scopedSort . tyCoVarsOfTypeList
-- | Get the free vars of types in scoped order
tyCoVarsOfTypesWellScoped :: [Type] -> [TyVar]
tyCoVarsOfTypesWellScoped = scopedSort . tyCoVarsOfTypesList
------------- Closing over kinds -----------------
-- | Add the kind variables free in the kinds of the tyvars in the given set.
......
......@@ -4,7 +4,6 @@ module Type where
import GhcPrelude
import TyCon
import Var ( TyCoVar )
import {-# SOURCE #-} TyCoRep( Type, Coercion )
import Util
......@@ -20,7 +19,4 @@ eqType :: Type -> Type -> Bool
coreView :: Type -> Maybe Type
tcView :: Type -> Maybe Type