---------------------------
--- First the TyCons...
-
--- | See "Type#kind_subtyping" for details of the distinction between the 'Kind' 'TyCon's
-funTyCon, tySuperKindTyCon, coSuperKindTyCon, liftedTypeKindTyCon,
- openTypeKindTyCon, unliftedTypeKindTyCon,
- ubxTupleKindTyCon, argTypeKindTyCon
- :: TyCon
-funTyConName, tySuperKindTyConName, coSuperKindTyConName, liftedTypeKindTyConName,
- openTypeKindTyConName, unliftedTypeKindTyConName,
- ubxTupleKindTyConName, argTypeKindTyConName
- :: Name
-
-funTyCon = mkFunTyCon funTyConName (mkArrowKinds [argTypeKind, openTypeKind] liftedTypeKind)
- -- You might think that (->) should have type (?? -> ? -> *), and you'd be right
- -- But if we do that we get kind errors when saying
- -- instance Control.Arrow (->)
- -- becuase the expected kind is (*->*->*). The trouble is that the
- -- expected/actual stuff in the unifier does not go contra-variant, whereas
- -- the kind sub-typing does. Sigh. It really only matters if you use (->) in
- -- a prefix way, thus: (->) Int# Int#. And this is unusual.
-
-
-tySuperKindTyCon = mkSuperKindTyCon tySuperKindTyConName
-coSuperKindTyCon = mkSuperKindTyCon coSuperKindTyConName
-
-liftedTypeKindTyCon = mkKindTyCon liftedTypeKindTyConName tySuperKind
-openTypeKindTyCon = mkKindTyCon openTypeKindTyConName tySuperKind
-unliftedTypeKindTyCon = mkKindTyCon unliftedTypeKindTyConName tySuperKind
-ubxTupleKindTyCon = mkKindTyCon ubxTupleKindTyConName tySuperKind
-argTypeKindTyCon = mkKindTyCon argTypeKindTyConName tySuperKind
-
---------------------------
--- ... and now their names
-
-tySuperKindTyConName = mkPrimTyConName (fsLit "BOX") tySuperKindTyConKey tySuperKindTyCon
-coSuperKindTyConName = mkPrimTyConName (fsLit "COERCION") coSuperKindTyConKey coSuperKindTyCon
-liftedTypeKindTyConName = mkPrimTyConName (fsLit "*") liftedTypeKindTyConKey liftedTypeKindTyCon
-openTypeKindTyConName = mkPrimTyConName (fsLit "?") openTypeKindTyConKey openTypeKindTyCon
-unliftedTypeKindTyConName = mkPrimTyConName (fsLit "#") unliftedTypeKindTyConKey unliftedTypeKindTyCon
-ubxTupleKindTyConName = mkPrimTyConName (fsLit "(#)") ubxTupleKindTyConKey ubxTupleKindTyCon
-argTypeKindTyConName = mkPrimTyConName (fsLit "??") argTypeKindTyConKey argTypeKindTyCon
-funTyConName = mkPrimTyConName (fsLit "(->)") funTyConKey funTyCon
-
-mkPrimTyConName :: FastString -> Unique -> TyCon -> Name
-mkPrimTyConName occ key tycon = mkWiredInName gHC_PRIM (mkTcOccFS occ)
- key
- (ATyCon tycon)
- BuiltInSyntax
- -- All of the super kinds and kinds are defined in Prim and use BuiltInSyntax,
- -- because they are never in scope in the source
-
-------------------
--- We also need Kinds and SuperKinds, locally and in TyCon
-
-kindTyConType :: TyCon -> Type
-kindTyConType kind = TyConApp kind []
-
--- | See "Type#kind_subtyping" for details of the distinction between these 'Kind's
-liftedTypeKind, unliftedTypeKind, openTypeKind, argTypeKind, ubxTupleKind :: Kind
-
-liftedTypeKind = kindTyConType liftedTypeKindTyCon
-unliftedTypeKind = kindTyConType unliftedTypeKindTyCon
-openTypeKind = kindTyConType openTypeKindTyCon
-argTypeKind = kindTyConType argTypeKindTyCon
-ubxTupleKind = kindTyConType ubxTupleKindTyCon
+-- | Type substitution
+--
+-- #tvsubst_invariant#
+-- The following invariants must hold of a 'TvSubst':
+--
+-- 1. The in-scope set is needed /only/ to
+-- guide the generation of fresh uniques
+--
+-- 2. In particular, the /kind/ of the type variables in
+-- the in-scope set is not relevant
+--
+-- 3. The substition is only applied ONCE! This is because
+-- in general such application will not reached a fixed point.
+data TvSubst
+ = TvSubst InScopeSet -- The in-scope type variables
+ TvSubstEnv -- Substitution of types
+ -- See Note [Apply Once]
+ -- and Note [Extending the TvSubstEnv]
+
+-- | A substitition of 'Type's for 'TyVar's
+type TvSubstEnv = TyVarEnv Type
+ -- A TvSubstEnv is used both inside a TvSubst (with the apply-once
+ -- invariant discussed in Note [Apply Once]), and also independently
+ -- in the middle of matching, and unification (see Types.Unify)
+ -- So you have to look at the context to know if it's idempotent or
+ -- apply-once or whatever
+\end{code}