diff options
Diffstat (limited to 'compiler/types/TyCoRep.hs')
| -rw-r--r-- | compiler/types/TyCoRep.hs | 1295 |
1 files changed, 915 insertions, 380 deletions
diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs index 5ac63e5b04..b50327fc37 100644 --- a/compiler/types/TyCoRep.hs +++ b/compiler/types/TyCoRep.hs @@ -18,7 +18,6 @@ Note [The Type-related module hierarchy] -- We expose the relevant stuff from this module via the Type module {-# OPTIONS_HADDOCK hide #-} {-# LANGUAGE CPP, DeriveDataTypeable, MultiWayIf #-} -{-# LANGUAGE ImplicitParams #-} module TyCoRep ( TyThing(..), tyThingCategory, pprTyThingCategory, pprShortTyThing, @@ -27,45 +26,55 @@ module TyCoRep ( Type(..), TyLit(..), KindOrType, Kind, + KnotTied, PredType, ThetaType, -- Synonyms ArgFlag(..), -- * Coercions Coercion(..), - UnivCoProvenance(..), CoercionHole(..), + UnivCoProvenance(..), + CoercionHole(..), coHoleCoVar, setCoHoleCoVar, CoercionN, CoercionR, CoercionP, KindCoercion, + MCoercion(..), MCoercionR, MCoercionN, -- * Functions over types mkTyConTy, mkTyVarTy, mkTyVarTys, - mkFunTy, mkFunTys, mkForAllTy, mkForAllTys, - mkPiTy, mkPiTys, + mkTyCoVarTy, mkTyCoVarTys, + mkFunTy, mkFunTys, mkTyCoForAllTy, mkForAllTys, + mkForAllTy, + mkTyCoPiTy, mkTyCoPiTys, + mkPiTys, + isTYPE, isLiftedTypeKind, isUnliftedTypeKind, isCoercionType, isRuntimeRepTy, isRuntimeRepVar, - isRuntimeRepKindedTy, dropRuntimeRepArgs, sameVis, -- * Functions over binders - TyBinder(..), TyVarBinder, - binderVar, binderVars, binderKind, binderArgFlag, + TyCoBinder(..), TyCoVarBinder, TyBinder, + binderVar, binderVars, binderType, binderArgFlag, delBinderVar, isInvisibleArgFlag, isVisibleArgFlag, isInvisibleBinder, isVisibleBinder, + isTyBinder, -- * Functions over coercions pickLR, -- * Pretty-printing pprType, pprParendType, pprPrecType, - pprTypeApp, pprTvBndr, pprTvBndrs, + pprTypeApp, pprTCvBndr, pprTCvBndrs, pprSigmaType, pprTheta, pprParendTheta, pprForAll, pprUserForAll, pprTyVar, pprTyVars, pprThetaArrowTy, pprClassPred, pprKind, pprParendKind, pprTyLit, - TyPrec(..), maybeParen, pprTcAppCo, - pprPrefixApp, pprArrowChain, + PprPrec(..), topPrec, sigPrec, opPrec, funPrec, appPrec, maybeParen, pprDataCons, ppSuggestExplicitKinds, + pprCo, pprParendCo, + + debugPprType, + -- * Free variables tyCoVarsOfType, tyCoVarsOfTypeDSet, tyCoVarsOfTypes, tyCoVarsOfTypesDSet, tyCoFVsBndr, tyCoFVsOfType, tyCoVarsOfTypeList, @@ -78,6 +87,7 @@ module TyCoRep ( tyCoFVsOfCo, tyCoFVsOfCos, tyCoVarsOfCoList, tyCoVarsOfProv, closeOverKinds, + injectiveVarsOfBinder, injectiveVarsOfType, noFreeVarsOfType, noFreeVarsOfCo, @@ -85,18 +95,20 @@ module TyCoRep ( TCvSubst(..), TvSubstEnv, CvSubstEnv, emptyTvSubstEnv, emptyCvSubstEnv, composeTCvSubstEnv, composeTCvSubst, emptyTCvSubst, mkEmptyTCvSubst, isEmptyTCvSubst, - mkTCvSubst, mkTvSubst, + mkTCvSubst, mkTvSubst, mkCvSubst, getTvSubstEnv, getCvSubstEnv, getTCvInScope, getTCvSubstRangeFVs, isInScope, notElemTCvSubst, setTvSubstEnv, setCvSubstEnv, zapTCvSubst, extendTCvInScope, extendTCvInScopeList, extendTCvInScopeSet, - extendTCvSubst, + extendTCvSubst, extendTCvSubstWithClone, extendCvSubst, extendCvSubstWithClone, - extendTvSubst, extendTvSubstBinder, extendTvSubstWithClone, + extendTvSubst, extendTvSubstBinderAndInScope, extendTvSubstWithClone, extendTvSubstList, extendTvSubstAndInScope, + extendTCvSubstList, unionTCvSubst, zipTyEnv, zipCoEnv, mkTyCoInScopeSet, zipTvSubst, zipCvSubst, + zipTCvSubst, mkTvSubstPrs, substTyWith, substTyWithCoVars, substTysWith, substTysWithCoVars, @@ -107,25 +119,28 @@ module TyCoRep ( substCoUnchecked, substCoWithUnchecked, substTyWithInScope, substTys, substTheta, - lookupTyVar, substTyVarBndr, + lookupTyVar, substCo, substCos, substCoVar, substCoVars, lookupCoVar, - substCoVarBndr, cloneTyVarBndr, cloneTyVarBndrs, - substTyVar, substTyVars, + cloneTyVarBndr, cloneTyVarBndrs, + substVarBndr, substVarBndrs, + substTyVarBndr, substTyVarBndrs, + substCoVarBndr, + substTyVar, substTyVars, substTyCoVars, substForAllCoBndr, - substTyVarBndrCallback, substForAllCoBndrCallback, + substVarBndrUsing, substForAllCoBndrUsing, checkValidSubst, isValidTCvSubst, -- * Tidying type related things up for printing tidyType, tidyTypes, tidyOpenType, tidyOpenTypes, tidyOpenKind, - tidyTyCoVarBndr, tidyTyCoVarBndrs, tidyFreeTyCoVars, + tidyVarBndr, tidyVarBndrs, tidyFreeTyCoVars, tidyOpenTyCoVar, tidyOpenTyCoVars, - tidyTyVarOcc, + tidyTyCoVarOcc, tidyTopType, tidyKind, tidyCo, tidyCos, - tidyTyVarBinder, tidyTyVarBinders, + tidyTyCoVarBinder, tidyTyCoVarBinders, -- * Sizes typeSize, coercionSize, provSize @@ -133,19 +148,22 @@ module TyCoRep ( #include "HsVersions.h" +import GhcPrelude + import {-# SOURCE #-} DataCon( dataConFullSig - , dataConUnivTyVarBinders, dataConExTyVarBinders - , DataCon, filterEqSpec ) + , dataConUserTyVarBinders + , DataCon ) import {-# SOURCE #-} Type( isPredTy, isCoercionTy, mkAppTy, mkCastTy - , tyCoVarsOfTypesWellScoped , tyCoVarsOfTypeWellScoped - , coreView, typeKind ) + , tyCoVarsOfTypesWellScoped + , toposortTyVars + , coreView ) -- Transitively pulls in a LOT of stuff, better to break the loop import {-# SOURCE #-} Coercion import {-# SOURCE #-} ConLike ( ConLike(..), conLikeName ) import {-# SOURCE #-} ToIface( toIfaceTypeX, toIfaceTyLit, toIfaceForAllBndr - , toIfaceTyCon, toIfaceTcArgs, toIfaceCoercion ) + , toIfaceTyCon, toIfaceTcArgs, toIfaceCoercionX ) -- friends: import IfaceType @@ -159,7 +177,8 @@ import CoAxiom import FV -- others -import BasicTypes ( LeftOrRight(..), TyPrec(..), maybeParen, pickLR ) +import BasicTypes ( LeftOrRight(..), PprPrec(..), topPrec, sigPrec, opPrec + , funPrec, appPrec, maybeParen, pickLR ) import PrelNames import Outputable import DynFlags @@ -258,8 +277,10 @@ data Type Type Type -- ^ Type application to something other than a 'TyCon'. Parameters: -- - -- 1) Function: must /not/ be a 'TyConApp', + -- 1) Function: must /not/ be a 'TyConApp' or 'CastTy', -- must be another 'AppTy', or 'TyVarTy' + -- See Note [Respecting definitional equality] (EQ1) about the + -- no 'CastTy' requirement -- -- 2) Argument type @@ -281,7 +302,7 @@ data Type -- can appear as the right hand side of a type synonym. | ForAllTy - {-# UNPACK #-} !TyVarBinder + {-# UNPACK #-} !TyCoVarBinder Type -- ^ A Πtype. | FunTy Type Type -- ^ t1 -> t2 Very common, so an important special case @@ -292,8 +313,8 @@ data Type Type KindCoercion -- ^ A kind cast. The coercion is always nominal. -- INVARIANT: The cast is never refl. - -- INVARIANT: The cast is "pushed down" as far as it - -- can go. See Note [Pushing down casts] + -- INVARIANT: The Type is not a CastTy (use TransCo instead) + -- See Note [Respecting definitional equality] (EQ2) and (EQ3) | CoercionTy Coercion -- ^ Injection of a Coercion into a type @@ -333,19 +354,12 @@ kinds or types. This kind instantiation only happens in TyConApp currently. -Note [Pushing down casts] -~~~~~~~~~~~~~~~~~~~~~~~~~ -Suppose we have (a :: k1 -> *), (b :: k1), and (co :: * ~ q). -The type (a b |> co) is `eqType` to ((a |> co') b), where -co' = (->) <k1> co. Thus, to make this visible to functions -that inspect types, we always push down coercions, preferring -the second form. Note that this also applies to TyConApps! - Note [Non-trivial definitional equality] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Is Int |> <*> the same as Int? YES! In order to reduce headaches, -we decide that any reflexive casts in types are just ignored. More -generally, the `eqType` function, which defines Core's type equality +we decide that any reflexive casts in types are just ignored. +(Indeed they must be. See Note [Respecting definitional equality].) +More generally, the `eqType` function, which defines Core's type equality relation, ignores casts and coercion arguments, as long as the two types have the same kind. This allows us to be a little sloppier in keeping track of coercions, which is a good thing. It also means @@ -357,11 +371,11 @@ appropriate for the implementation of eqType? Anything smaller than ~ and homogeneous is an appropriate definition for equality. The type safety of FC depends only on ~. Let's say η : τ ~ σ. Any expression of type τ can be transmuted to one of type σ at any point by -casting. The same is true of types of type τ. So in some sense, τ and σ are -interchangeable. +casting. The same is true of expressions of type σ. So in some sense, τ and σ +are interchangeable. But let's be more precise. If we examine the typing rules of FC (say, those in -http://www.cis.upenn.edu/~eir/papers/2015/equalities/equalities-extended.pdf) +https://cs.brynmawr.edu/~rae/papers/2015/equalities/equalities.pdf) there are several places where the same metavariable is used in two different premises to a rule. (For example, see Ty_App.) There is an implicit equality check here. What definition of equality should we use? By convention, we use @@ -378,6 +392,9 @@ The effect of this all is that eqType, the implementation of the implicit equality check, can use any homogeneous relation that is smaller than ~, as those rules must also be admissible. +A more drawn out argument around all of this is presented in Section 7.2 of +Richard E's thesis (http://cs.brynmawr.edu/~rae/papers/2016/thesis/eisenberg-thesis.pdf). + What would go wrong if we insisted on the casts matching? See the beginning of Section 8 in the unpublished paper above. Theoretically, nothing at all goes wrong. But in practical terms, getting the coercions right proved to be @@ -398,48 +415,145 @@ constructors and destructors in Type respect whatever relation is chosen. Another helpful principle with eqType is this: - ** If (t1 eqType t2) then I can replace t1 by t2 anywhere. ** + (EQ) If (t1 `eqType` t2) then I can replace t1 by t2 anywhere. This principle also tells us that eqType must relate only types with the same kinds. + +Note [Respecting definitional equality] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Note [Non-trivial definitional equality] introduces the property (EQ). +How is this upheld? + +Any function that pattern matches on all the constructors will have to +consider the possibility of CastTy. Presumably, those functions will handle +CastTy appropriately and we'll be OK. + +More dangerous are the splitXXX functions. Let's focus on splitTyConApp. +We don't want it to fail on (T a b c |> co). Happily, if we have + (T a b c |> co) `eqType` (T d e f) +then co must be reflexive. Why? eqType checks that the kinds are equal, as +well as checking that (a `eqType` d), (b `eqType` e), and (c `eqType` f). +By the kind check, we know that (T a b c |> co) and (T d e f) have the same +kind. So the only way that co could be non-reflexive is for (T a b c) to have +a different kind than (T d e f). But because T's kind is closed (all tycon kinds +are closed), the only way for this to happen is that one of the arguments has +to differ, leading to a contradiction. Thus, co is reflexive. + +Accordingly, by eliminating reflexive casts, splitTyConApp need not worry +about outermost casts to uphold (EQ). Eliminating reflexive casts is done +in mkCastTy. + +Unforunately, that's not the end of the story. Consider comparing + (T a b c) =? (T a b |> (co -> <Type>)) (c |> co) +These two types have the same kind (Type), but the left type is a TyConApp +while the right type is not. To handle this case, we say that the right-hand +type is ill-formed, requiring an AppTy never to have a casted TyConApp +on its left. It is easy enough to pull around the coercions to maintain +this invariant, as done in Type.mkAppTy. In the example above, trying to +form the right-hand type will instead yield (T a b (c |> co |> sym co) |> <Type>). +Both the casts there are reflexive and will be dropped. Huzzah. + +This idea of pulling coercions to the right works for splitAppTy as well. + +However, there is one hiccup: it's possible that a coercion doesn't relate two +Pi-types. For example, if we have @type family Fun a b where Fun a b = a -> b@, +then we might have (T :: Fun Type Type) and (T |> axFun) Int. That axFun can't +be pulled to the right. But we don't need to pull it: (T |> axFun) Int is not +`eqType` to any proper TyConApp -- thus, leaving it where it is doesn't violate +our (EQ) property. + +Lastly, in order to detect reflexive casts reliably, we must make sure not +to have nested casts: we update (t |> co1 |> co2) to (t |> (co1 `TransCo` co2)). + +In sum, in order to uphold (EQ), we need the following three invariants: + + (EQ1) No decomposable CastTy to the left of an AppTy, where a decomposable + cast is one that relates either a FunTy to a FunTy or a + ForAllTy to a ForAllTy. + (EQ2) No reflexive casts in CastTy. + (EQ3) No nested CastTys. + (EQ4) No CastTy over (ForAllTy (Bndr tyvar vis) body). + See Note [Weird typing rule for ForAllTy] in Type. + +These invariants are all documented above, in the declaration for Type. + +Note [Unused coercion variable in ForAllTy] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Suppose we have + \(co:t1 ~ t2). e + +What type should we give to this expression? + (1) forall (co:t1 ~ t2) -> t + (2) (t1 ~ t2) -> t + +If co is used in t, (1) should be the right choice. +if co is not used in t, we would like to have (1) and (2) equivalent. + +However, we want to keep eqType simple and don't want eqType (1) (2) to return +True in any case. + +We decide to always construct (2) if co is not used in t. + +Thus in mkTyCoForAllTy, we check whether the variable is a coercion +variable and whether it is used in the body. If so, it returns a FunTy +instead of a ForAllTy. + +There are cases we want to skip the check. For example, the check is unnecessary +when it is known from the context that the input variable is a type variable. +In those cases, we use mkForAllTy. -} +-- | A type labeled 'KnotTied' might have knot-tied tycons in it. See +-- Note [Type checking recursive type and class declarations] in +-- TcTyClsDecls +type KnotTied ty = ty + {- ********************************************************************** * * - TyBinder and ArgFlag + TyCoBinder and ArgFlag * * ********************************************************************** -} --- | A 'TyBinder' represents an argument to a function. TyBinders can be dependent --- ('Named') or nondependent ('Anon'). They may also be visible or not. --- See Note [TyBinders] -data TyBinder - = Named TyVarBinder -- A type-lambda binder - | Anon Type -- A term-lambda binder +-- | A 'TyCoBinder' represents an argument to a function. TyCoBinders can be +-- dependent ('Named') or nondependent ('Anon'). They may also be visible or +-- not. See Note [TyCoBinders] +data TyCoBinder + = Named TyCoVarBinder -- A type-lambda binder + | Anon Type -- A term-lambda binder. Type here can be CoercionTy. -- Visibility is determined by the type (Constraint vs. *) deriving Data.Data +-- | 'TyBinder' is like 'TyCoBinder', but there can only be 'TyVarBinder' +-- in the 'Named' field. +type TyBinder = TyCoBinder + -- | Remove the binder's variable from the set, if the binder has -- a variable. -delBinderVar :: VarSet -> TyVarBinder -> VarSet -delBinderVar vars (TvBndr tv _) = vars `delVarSet` tv +delBinderVar :: VarSet -> TyCoVarBinder -> VarSet +delBinderVar vars (Bndr tv _) = vars `delVarSet` tv -- | Does this binder bind an invisible argument? -isInvisibleBinder :: TyBinder -> Bool -isInvisibleBinder (Named (TvBndr _ vis)) = isInvisibleArgFlag vis -isInvisibleBinder (Anon ty) = isPredTy ty +isInvisibleBinder :: TyCoBinder -> Bool +isInvisibleBinder (Named (Bndr _ vis)) = isInvisibleArgFlag vis +isInvisibleBinder (Anon ty) = isPredTy ty -- | Does this binder bind a visible argument? -isVisibleBinder :: TyBinder -> Bool +isVisibleBinder :: TyCoBinder -> Bool isVisibleBinder = not . isInvisibleBinder +-- | If its a named binder, is the binder a tyvar? +-- Returns True for nondependent binder. +isTyBinder :: TyCoBinder -> Bool +isTyBinder (Named bnd) = isTyVarBinder bnd +isTyBinder _ = True -{- Note [TyBinders] +{- Note [TyCoBinders] ~~~~~~~~~~~~~~~~~~~ -A ForAllTy contains a TyVarBinder. But a type can be decomposed -to a telescope consisting of a [TyBinder] +A ForAllTy contains a TyCoVarBinder. But a type can be decomposed +to a telescope consisting of a [TyCoBinder] -A TyBinder represents the type of binders -- that is, the type of an +A TyCoBinder represents the type of binders -- that is, the type of an argument to a Pi-type. GHC Core currently supports two different Pi-types: @@ -457,36 +571,47 @@ words, if `x` is either a function or a polytype, `x arg` makes sense (for an appropriate `arg`). -Note [TyBinders and ArgFlags] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -A ForAllTy contains a TyVarBinder. Each TyVarBinder is equipped -with a ArgFlag, which says whether or not arguments for this -binder should be visible (explicit) in source Haskell. - ------------------------------------------------------------------------ - Occurrences look like this - TyBinder GHC displays type as in Haskell souce code ------------------------------------------------------------------------ -In the type of a term - Anon: f :: type -> type Arg required: f x - Named Inferred: f :: forall {a}. type Arg not allowed: f - Named Specified: f :: forall a. type Arg optional: f or f @Int - Named Required: Illegal: See Note [No Required TyBinder in terms] - -In the kind of a type - Anon: T :: kind -> kind Required: T * - Named Inferred: T :: forall {k}. kind Arg not allowed: T - Named Specified: T :: forall k. kind Arg not allowed[1]: T - Named Required: T :: forall k -> kind Required: T * ------------------------------------------------------------------------- +Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +* A ForAllTy (used for both types and kinds) contains a TyCoVarBinder. + Each TyCoVarBinder + Bndr a tvis + is equipped with tvis::ArgFlag, which says whether or not arguments + for this binder should be visible (explicit) in source Haskell. + +* A TyCon contains a list of TyConBinders. Each TyConBinder + Bndr a cvis + is equipped with cvis::TyConBndrVis, which says whether or not type + and kind arguments for this TyCon should be visible (explicit) in + source Haskell. + +This table summarises the visibility rules: +--------------------------------------------------------------------------------------- +| Occurrences look like this +| GHC displays type as in Haskell source code +|-------------------------------------------------------------------------------------- +| Bndr a tvis :: TyCoVarBinder, in the binder of ForAllTy for a term +| tvis :: ArgFlag +| tvis = Inferred: f :: forall {a}. type Arg not allowed: f + f :: forall {co}. type Arg not allowed: f +| tvis = Specified: f :: forall a. type Arg optional: f or f @Int +| tvis = Required: T :: forall k -> type Arg required: T * +| This last form is illegal in terms: See Note [No Required TyCoBinder in terms] +| +| Bndr k cvis :: TyConBinder, in the TyConBinders of a TyCon +| cvis :: TyConBndrVis +| cvis = AnonTCB: T :: kind -> kind Required: T * +| cvis = NamedTCB Inferred: T :: forall {k}. kind Arg not allowed: T +| T :: forall {co}. kind Arg not allowed: T +| cvis = NamedTCB Specified: T :: forall k. kind Arg not allowed[1]: T +| cvis = NamedTCB Required: T :: forall k -> kind Required: T * +--------------------------------------------------------------------------------------- [1] In types, in the Specified case, it would make sense to allow optional kind applications, thus (T @*), but we have not yet implemented that ----- Examples of where the different visibilities come from ----- - -In term declarations: +---- In term declarations ---- * Inferred. Function defn, with no signature: f1 x = x We infer f1 :: forall {a}. a -> a, with 'a' Inferred @@ -495,12 +620,12 @@ In term declarations: * Specified. Function defn, with signature (implicit forall): f2 :: a -> a; f2 x = x - So f2 gets the type f2 :: forall a. a->a, with 'a' Specified + So f2 gets the type f2 :: forall a. a -> a, with 'a' Specified even though 'a' is not bound in the source code by an explicit forall * Specified. Function defn, with signature (explicit forall): f3 :: forall a. a -> a; f3 x = x - So f3 gets the type f3 :: forall a. a->a, with 'a' Specified + So f3 gets the type f3 :: forall a. a -> a, with 'a' Specified * Inferred/Specified. Function signature with inferred kind polymorphism. f4 :: a b -> Int @@ -517,14 +642,14 @@ In term declarations: Inferred - from inferred types (e.g. no pattern type signature) - or from inferred kind polymorphism -In type declarations: +---- In type declarations ---- * Inferred (k) data T1 a b = MkT1 (a b) Here T1's kind is T1 :: forall {k:*}. (k->*) -> k -> * The kind variable 'k' is Inferred, since it is not mentioned - Note that 'a' and 'b' correspond to /Anon/ TyBinders in T1's kind, + Note that 'a' and 'b' correspond to /Anon/ TyCoBinders in T1's kind, and Anon binders don't have a visibility flag. (Or you could think of Anon having an implicit Required flag.) @@ -546,6 +671,19 @@ In type declarations: So 'k' is Specified, because it appears explicitly, but 'k1' is Inferred, because it does not +Generally, in the list of TyConBinders for a TyCon, + +* Inferred arguments always come first +* Specified, Anon and Required can be mixed + +e.g. + data Foo (a :: Type) :: forall b. (a -> b -> Type) -> Type where ... + +Here Foo's TyConBinders are + [Required 'a', Specified 'b', Anon] +and its kind prints as + Foo :: forall a -> forall b. (a -> b -> Type) -> Type + ---- Printing ----- We print forall types with enough syntax to tell you their visibility @@ -571,14 +709,14 @@ In type declarations: * Inferred variables correspond to "generalized" variables from the Visible Type Applications paper (ESOP'16). -Note [No Required TyBinder in terms] +Note [No Required TyCoBinder in terms] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We don't allow Required foralls for term variables, including pattern synonyms and data constructors. Why? Because then an application would need a /compulsory/ type argument (possibly without an "@"?), thus (f Int); and we don't have concrete syntax for that. -We could change this decision, but Required, Named TyBinders are rare +We could change this decision, but Required, Named TyCoBinders are rare anyway. (Most are Anons.) -} @@ -639,14 +777,23 @@ These functions are here so that they can be used by TysPrim, which in turn is imported by Type -} --- named with "Only" to prevent naive use of mkTyVarTy mkTyVarTy :: TyVar -> Type mkTyVarTy v = ASSERT2( isTyVar v, ppr v <+> dcolon <+> ppr (tyVarKind v) ) - TyVarTy v + TyVarTy v mkTyVarTys :: [TyVar] -> [Type] mkTyVarTys = map mkTyVarTy -- a common use of mkTyVarTy +mkTyCoVarTy :: TyCoVar -> Type +mkTyCoVarTy v + | isTyVar v + = TyVarTy v + | otherwise + = CoercionTy (CoVarCo v) + +mkTyCoVarTys :: [TyCoVar] -> [Type] +mkTyCoVarTys = map mkTyCoVarTy + infixr 3 `mkFunTy` -- Associates to the right -- | Make an arrow type mkFunTy :: Type -> Type -> Type @@ -656,18 +803,41 @@ mkFunTy arg res = FunTy arg res mkFunTys :: [Type] -> Type -> Type mkFunTys tys ty = foldr mkFunTy ty tys -mkForAllTy :: TyVar -> ArgFlag -> Type -> Type -mkForAllTy tv vis ty = ForAllTy (TvBndr tv vis) ty +-- | If tv is a coercion variable and it is not used in the body, returns +-- a FunTy, otherwise makes a forall type. +-- See Note [Unused coercion variable in ForAllTy] +mkTyCoForAllTy :: TyCoVar -> ArgFlag -> Type -> Type +mkTyCoForAllTy tv vis ty + | isCoVar tv + , not (tv `elemVarSet` tyCoVarsOfType ty) + = ASSERT( vis == Inferred ) + mkFunTy (varType tv) ty + | otherwise + = ForAllTy (Bndr tv vis) ty --- | Wraps foralls over the type using the provided 'TyVar's from left to right -mkForAllTys :: [TyVarBinder] -> Type -> Type +-- | Like 'mkTyCoForAllTy', but does not check the occurrence of the binder +-- See Note [Unused coercion variable in ForAllTy] +mkForAllTy :: TyCoVar -> ArgFlag -> Type -> Type +mkForAllTy tv vis ty = ForAllTy (Bndr tv vis) ty + +-- | Wraps foralls over the type using the provided 'TyCoVar's from left to right +mkForAllTys :: [TyCoVarBinder] -> Type -> Type mkForAllTys tyvars ty = foldr ForAllTy ty tyvars -mkPiTy :: TyBinder -> Type -> Type -mkPiTy (Anon ty1) ty2 = FunTy ty1 ty2 -mkPiTy (Named tvb) ty = ForAllTy tvb ty +mkTyCoPiTy :: TyCoBinder -> Type -> Type +mkTyCoPiTy (Anon ty1) ty2 = FunTy ty1 ty2 +mkTyCoPiTy (Named (Bndr tv vis)) ty = mkTyCoForAllTy tv vis ty + +-- | Like 'mkTyCoPiTy', but does not check the occurrence of the binder +mkPiTy:: TyCoBinder -> Type -> Type +mkPiTy (Anon ty1) ty2 = FunTy ty1 ty2 +mkPiTy (Named (Bndr tv vis)) ty = mkForAllTy tv vis ty -mkPiTys :: [TyBinder] -> Type -> Type +mkTyCoPiTys :: [TyCoBinder] -> Type -> Type +mkTyCoPiTys tbs ty = foldr mkTyCoPiTy ty tbs + +-- | Like 'mkTyCoPiTys', but does not check the occurrence of the binder +mkPiTys :: [TyCoBinder] -> Type -> Type mkPiTys tbs ty = foldr mkPiTy ty tbs -- | Does this type classify a core (unlifted) Coercion? @@ -689,22 +859,28 @@ mkTyConTy tycon = TyConApp tycon [] Some basic functions, put here to break loops eg with the pretty printer -} -is_TYPE :: ( Type -- the single argument to TYPE; not a synonym - -> Bool ) -- what to return - -> Kind -> Bool -is_TYPE f ki | Just ki' <- coreView ki = is_TYPE f ki' -is_TYPE f (TyConApp tc [arg]) +-- | If a type is @'TYPE' r@ for some @r@, run the predicate argument on @r@. +-- Otherwise, return 'False'. +-- +-- This function does not distinguish between 'Constraint' and 'Type'. For a +-- version which does distinguish between the two, see 'tcIsTYPE'. +isTYPE :: ( Type -- the single argument to TYPE; not a synonym + -> Bool ) -- what to return + -> Kind -> Bool +isTYPE f ki | Just ki' <- coreView ki = isTYPE f ki' +isTYPE f (TyConApp tc [arg]) | tc `hasKey` tYPETyConKey = go arg where go ty | Just ty' <- coreView ty = go ty' go ty = f ty -is_TYPE _ _ = False +isTYPE _ _ = False --- | This version considers Constraint to be distinct from *. Returns True --- if the argument is equivalent to Type and False otherwise. +-- | This version considers Constraint to be the same as *. Returns True +-- if the argument is equivalent to Type/Constraint and False otherwise. +-- See Note [Kind Constraint and kind Type] isLiftedTypeKind :: Kind -> Bool -isLiftedTypeKind = is_TYPE is_lifted +isLiftedTypeKind = isTYPE is_lifted where is_lifted (TyConApp lifted_rep []) = lifted_rep `hasKey` liftedRepDataConKey is_lifted _ = False @@ -713,9 +889,9 @@ isLiftedTypeKind = is_TYPE is_lifted -- Note that this returns False for levity-polymorphic kinds, which may -- be specialized to a kind that classifies unlifted types. isUnliftedTypeKind :: Kind -> Bool -isUnliftedTypeKind = is_TYPE is_unlifted +isUnliftedTypeKind = isTYPE is_unlifted where - is_unlifted (TyConApp rr _args) = not (rr `hasKey` liftedRepDataConKey) + is_unlifted (TyConApp rr _args) = elem (getUnique rr) unliftedRepDataConKeys is_unlifted _ = False -- | Is this the type 'RuntimeRep'? @@ -724,23 +900,10 @@ isRuntimeRepTy ty | Just ty' <- coreView ty = isRuntimeRepTy ty' isRuntimeRepTy (TyConApp tc []) = tc `hasKey` runtimeRepTyConKey isRuntimeRepTy _ = False --- | Is this a type of kind RuntimeRep? (e.g. LiftedRep) -isRuntimeRepKindedTy :: Type -> Bool -isRuntimeRepKindedTy = isRuntimeRepTy . typeKind - -- | Is a tyvar of type 'RuntimeRep'? isRuntimeRepVar :: TyVar -> Bool isRuntimeRepVar = isRuntimeRepTy . tyVarKind --- | Drops prefix of RuntimeRep constructors in 'TyConApp's. Useful for e.g. --- dropping 'LiftedRep arguments of unboxed tuple TyCon applications: --- --- dropRuntimeRepArgs [ 'LiftedRep, 'IntRep --- , String, Int# ] == [String, Int#] --- -dropRuntimeRepArgs :: [Type] -> [Type] -dropRuntimeRepArgs = dropWhile isRuntimeRepKindedTy - {- %************************************************************************ %* * @@ -764,8 +927,8 @@ data Coercion -- - _ stands for a parameter that is not a Role or Coercion. -- These ones mirror the shape of types - = -- Refl :: "e" -> _ -> e - Refl Role Type -- See Note [Refl invariant] + = -- Refl :: _ -> N + Refl Type -- See Note [Refl invariant] -- Invariant: applications of (Refl T) to a bunch of identity coercions -- always show up as Refl. -- For example (Refl T) (Refl a) (Refl b) shows up as (Refl (T a b)). @@ -776,7 +939,13 @@ data Coercion -- ConAppCo coercions (like all coercions other than Refl) -- are NEVER the identity. - -- Use (Refl Representational _), not (SubCo (Refl Nominal _)) + -- Use (GRefl Representational ty MRefl), not (SubCo (Refl ty)) + + -- GRefl :: "e" -> _ -> Maybe N -> e + -- See Note [Generalized reflexive coercion] + | GRefl Role Type MCoercionN -- See Note [Refl invariant] + -- Use (Refl ty), not (GRefl Nominal ty MRefl) + -- Use (GRefl Representational _ _), not (SubCo (GRefl Nominal _ _)) -- These ones simply lift the correspondingly-named -- Type constructors into Coercions @@ -792,7 +961,7 @@ data Coercion -- AppCo :: e -> N -> e -- See Note [Forall coercions] - | ForAllCo TyVar KindCoercion Coercion + | ForAllCo TyCoVar KindCoercion Coercion -- ForAllCo :: _ -> N -> e -> e | FunCo Role Coercion Coercion -- lift FunTy @@ -810,20 +979,25 @@ data Coercion -- any left over, we use AppCo. -- See [Coercion axioms applied to coercions] + | AxiomRuleCo CoAxiomRule [Coercion] + -- AxiomRuleCo is very like AxiomInstCo, but for a CoAxiomRule + -- The number coercions should match exactly the expectations + -- of the CoAxiomRule (i.e., the rule is fully saturated). + | UnivCo UnivCoProvenance Role Type Type -- :: _ -> "e" -> _ -> _ -> e | SymCo Coercion -- :: e -> e | TransCo Coercion Coercion -- :: e -> e -> e - -- The number coercions should match exactly the expectations - -- of the CoAxiomRule (i.e., the rule is fully saturated). - | AxiomRuleCo CoAxiomRule [Coercion] - - | NthCo Int Coercion -- Zero-indexed; decomposes (T t0 ... tn) - -- :: _ -> e -> ?? (inverse of TyConAppCo, see Note [TyConAppCo roles]) + | NthCo Role Int Coercion -- Zero-indexed; decomposes (T t0 ... tn) + -- :: "e" -> _ -> e0 -> e (inverse of TyConAppCo, see Note [TyConAppCo roles]) -- Using NthCo on a ForAllCo gives an N coercion always -- See Note [NthCo and newtypes] + -- + -- Invariant: (NthCo r i co), it is always the case that r = role of (Nth i co) + -- That is: the role of the entire coercion is redundantly cached here. + -- See Note [NthCo Cached Roles] | LRCo LeftOrRight CoercionN -- Decomposes (t_left t_right) -- :: _ -> N -> N @@ -831,11 +1005,6 @@ data Coercion -- :: e -> N -> e -- See Note [InstCo roles] - -- Coherence applies a coercion to the left-hand type of another coercion - -- See Note [Coherence] - | CoherenceCo Coercion KindCoercion - -- :: e -> N -> e - -- Extract a kind coercion from a (heterogeneous) type coercion -- NB: all kind coercions are Nominal | KindCo Coercion @@ -844,6 +1013,8 @@ data Coercion | SubCo CoercionN -- Turns a ~N into a ~R -- :: N -> R + | HoleCo CoercionHole -- ^ See Note [Coercion holes] + -- Only present during typechecking deriving Data.Data type CoercionN = Coercion -- always nominal @@ -851,13 +1022,28 @@ type CoercionR = Coercion -- always representational type CoercionP = Coercion -- always phantom type KindCoercion = CoercionN -- always nominal +-- | A semantically more meaningful type to represent what may or may not be a +-- useful 'Coercion'. +data MCoercion + = MRefl + -- A trivial Reflexivity coercion + | MCo Coercion + -- Other coercions + deriving Data.Data +type MCoercionR = MCoercion +type MCoercionN = MCoercion + +instance Outputable MCoercion where + ppr MRefl = text "MRefl" + ppr (MCo co) = text "MCo" <+> ppr co + {- Note [Refl invariant] ~~~~~~~~~~~~~~~~~~~~~ Invariant 1: Coercions have the following invariant - Refl is always lifted as far as possible. + Refl (similar for GRefl r ty MRefl) is always lifted as far as possible. You might think that a consequencs is: Every identity coercions has Refl at the root @@ -868,6 +1054,42 @@ But that's not quite true because of coercion variables. Consider etc. So the consequence is only true of coercions that have no coercion variables. +Note [Generalized reflexive coercion] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +GRefl is a generalized reflexive coercion (see Trac #15192). It wraps a kind +coercion, which might be reflexive (MRefl) or any coercion (MCo co). The typing +rules for GRefl: + + ty : k1 + ------------------------------------ + GRefl r ty MRefl: ty ~r ty + + ty : k1 co :: k1 ~ k2 + ------------------------------------ + GRefl r ty (MCo co) : ty ~r ty |> co + +Consider we have + + g1 :: s ~r t + s :: k1 + g2 :: k1 ~ k2 + +and we want to construct a coercions co which has type + + (s |> g2) ~r t + +We can define + + co = Sym (GRefl r s g2) ; g1 + +It is easy to see that + + Refl == GRefl Nominal ty MRefl :: ty ~n ty + +A nominal reflexive coercion is quite common, so we keep the special form Refl to +save allocation. + Note [Coercion axioms applied to coercions] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The reason coercion axioms can be applied to coercions and not just @@ -936,9 +1158,10 @@ The typing rule is: ForAllCo tv1 kind_co co : all tv1:k1. t1 ~ all tv1:k2. (t2[tv1 |-> tv1 |> sym kind_co]) -First, the TyVar stored in a ForAllCo is really an optimisation: this field +First, the TyCoVar stored in a ForAllCo is really an optimisation: this field should be a Name, as its kind is redundant. Thinking of the field as a Name is helpful in understanding what a ForAllCo means. +The kind of TyCoVar always matches the left-hand kind of the coercion. The idea is that kind_co gives the two kinds of the tyvar. See how, in the conclusion, tv1 is assigned kind k1 on the left but kind k2 on the right. @@ -959,19 +1182,6 @@ add Names to, e.g., VarSets, and there generally is just an impedance mismatch in a bunch of places. So we use tv1. When we need tv2, we can use setTyVarKind. -Note [Coherence] -~~~~~~~~~~~~~~~~ -The Coherence typing rule is thus: - - g1 : s ~ t s : k1 g2 : k1 ~ k2 - ------------------------------------ - CoherenceCo g1 g2 : (s |> g2) ~ t - -While this looks (and is) unsymmetric, a combination of other coercion -combinators can make the symmetric version. - -For role information, see Note [Roles and kind coercions]. - Note [Predicate coercions] ~~~~~~~~~~~~~~~~~~~~~~~~~~ Suppose we have @@ -1131,7 +1341,7 @@ We can then build for any `a` and `b`. Because of the role annotation on N, if we use NthCo, we'll get out a representational coercion. That is: - NthCo 0 co :: forall a b. a ~R b + NthCo r 0 co :: forall a b. a ~R b Yikes! Clearly, this is terrible. The solution is simple: forbid NthCo to be used on newtypes if the internal coercion is representational. @@ -1140,6 +1350,23 @@ This is not just some corner case discovered by a segfault somewhere; it was discovered in the proof of soundness of roles and described in the "Safe Coercions" paper (ICFP '14). +Note [NthCo Cached Roles] +~~~~~~~~~~~~~~~~~~~~~~~~~ +Why do we cache the role of NthCo in the NthCo constructor? +Because computing role(Nth i co) involves figuring out that + + co :: T tys1 ~ T tys2 + +using coercionKind, and finding (coercionRole co), and then looking +at the tyConRoles of T. Avoiding bad asymptotic behaviour here means +we have to compute the kind and role of a coercion simultaneously, +which makes the code complicated and inefficient. + +This only happens for NthCo. Caching the role solves the problem, and +allows coercionKind and coercionRole to be simple. + +See Trac #11735 + Note [InstCo roles] ~~~~~~~~~~~~~~~~~~~ Here is (essentially) the typing rule for InstCo: @@ -1197,7 +1424,6 @@ data UnivCoProvenance | PluginProv String -- ^ From a plugin, which asserts that this coercion -- is sound. The string is for the use of the plugin. - | HoleProv CoercionHole -- ^ See Note [Coercion holes] deriving Data.Data instance Outputable UnivCoProvenance where @@ -1205,14 +1431,21 @@ instance Outputable UnivCoProvenance where ppr (PhantomProv _) = text "(phantom)" ppr (ProofIrrelProv _) = text "(proof irrel.)" ppr (PluginProv str) = parens (text "plugin" <+> brackets (text str)) - ppr (HoleProv hole) = parens (text "hole" <> ppr hole) -- | A coercion to be filled in by the type-checker. See Note [Coercion holes] data CoercionHole - = CoercionHole { chUnique :: Unique -- ^ used only for debugging - , chCoercion :: IORef (Maybe Coercion) + = CoercionHole { ch_co_var :: CoVar + -- See Note [CoercionHoles and coercion free variables] + + , ch_ref :: IORef (Maybe Coercion) } +coHoleCoVar :: CoercionHole -> CoVar +coHoleCoVar = ch_co_var + +setCoHoleCoVar :: CoercionHole -> CoVar -> CoercionHole +setCoHoleCoVar h cv = h { ch_co_var = cv } + instance Data.Data CoercionHole where -- don't traverse? toConstr _ = abstractConstr "CoercionHole" @@ -1220,7 +1453,7 @@ instance Data.Data CoercionHole where dataTypeOf _ = mkNoRepType "CoercionHole" instance Outputable CoercionHole where - ppr (CoercionHole u _) = braces (ppr u) + ppr (CoercionHole { ch_co_var = cv }) = braces (ppr cv) {- Note [Phantom coercions] @@ -1247,7 +1480,7 @@ During typechecking, constraint solving for type classes works by For equality constraints we use a different strategy. See Note [The equality types story] in TysPrim for background on equality constraints. - - For boxed equality constraints, (t1 ~N t2) and (t1 ~R t2), it's just + - For /boxed/ equality constraints, (t1 ~N t2) and (t1 ~R t2), it's just like type classes above. (Indeed, boxed equality constraints *are* classes.) - But for /unboxed/ equality constraints (t1 ~R# t2) and (t1 ~N# t2) we use a different plan @@ -1256,40 +1489,61 @@ For unboxed equalities: - Generate a CoercionHole, a mutable variable just like a unification variable - Wrap the CoercionHole in a Wanted constraint; see TcRnTypes.TcEvDest - - Use the CoercionHole in a Coercion, via HoleProv + - Use the CoercionHole in a Coercion, via HoleCo - Solve the constraint later - When solved, fill in the CoercionHole by side effect, instead of doing the let-binding thing The main reason for all this is that there may be no good place to let-bind the evidence for unboxed equalities: - - We emit constraints for kind coercions, to be used - to cast a type's kind. These coercions then must be used in types. Because - they might appear in a top-level type, there is no place to bind these - (unlifted) coercions in the usual way. - - A coercion for (forall a. t1) ~ forall a. t2) will look like + - We emit constraints for kind coercions, to be used to cast a + type's kind. These coercions then must be used in types. Because + they might appear in a top-level type, there is no place to bind + these (unlifted) coercions in the usual way. + + - A coercion for (forall a. t1) ~ (forall a. t2) will look like forall a. (coercion for t1~t2) - But the coercion for (t1~t2) may mention 'a', and we don't have let-bindings - within coercions. We could add them, but coercion holes are easier. + But the coercion for (t1~t2) may mention 'a', and we don't have + let-bindings within coercions. We could add them, but coercion + holes are easier. + + - Moreover, nothing is lost from the lack of let-bindings. For + dicionaries want to achieve sharing to avoid recomoputing the + dictionary. But coercions are entirely erased, so there's little + benefit to sharing. Indeed, even if we had a let-binding, we + always inline types and coercions at every use site and drop the + binding. Other notes about HoleCo: - * INVARIANT: CoercionHole and HoleProv are used only during type checking, + * INVARIANT: CoercionHole and HoleCo are used only during type checking, and should never appear in Core. Just like unification variables; a Type can contain a TcTyVar, but only during type checking. If, one day, we use type-level information to separate out forms that can appear during type-checking vs forms that can appear in core proper, holes in Core will be ruled out. - * The Unique carried with a coercion hole is used solely for debugging. + * See Note [CoercionHoles and coercion free variables] - * Coercion holes can be compared for equality only like other coercions: - only by looking at the types coerced. + * Coercion holes can be compared for equality like other coercions: + by looking at the types coerced. + + +Note [CoercionHoles and coercion free variables] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Why does a CoercionHole contain a CoVar, as well as reference to +fill in? Because we want to treat that CoVar as a free variable of +the coercion. See Trac #14584, and Note [What prevents a +constraint from floating] in TcSimplify, item (4): + + forall k. [W] co1 :: t1 ~# t2 |> co2 + [W] co2 :: k ~# * + +Here co2 is a CoercionHole. But we /must/ know that it is free in +co1, because that's all that stops it floating outside the +implication. - * We don't use holes for other evidence because other evidence wants to - be /shared/. But coercions are entirely erased, so there's little - benefit to sharing. Note [ProofIrrelProv] ~~~~~~~~~~~~~~~~~~~~~ @@ -1304,7 +1558,7 @@ In core, we get MkG :: forall (a :: *). (a ~ Bool) -> G a Now, consider 'MkG -- that is, MkG used in a type -- and suppose we want -a proof that ('MkG co1 a1) ~ ('MkG co2 a2). This will have to be +a proof that ('MkG a1 co1) ~ ('MkG a2 co2). This will have to be TyConAppCo Nominal MkG [co3, co4] where @@ -1319,7 +1573,7 @@ Here, co3 = UnivCo (ProofIrrelProv co5) Nominal (CoercionTy co1) (CoercionTy co2) where co5 :: (a1 ~ Bool) ~ (a2 ~ Bool) - co5 = TyConAppCo Nominal (~) [<*>, <*>, co4, <Bool>] + co5 = TyConAppCo Nominal (~#) [<*>, <*>, co4, <Bool>] %************************************************************************ @@ -1386,10 +1640,10 @@ tyCoFVsOfType (ForAllTy bndr ty) a b c = tyCoFVsBndr bndr (tyCoFVsOfType ty) a tyCoFVsOfType (CastTy ty co) a b c = (tyCoFVsOfType ty `unionFV` tyCoFVsOfCo co) a b c tyCoFVsOfType (CoercionTy co) a b c = tyCoFVsOfCo co a b c -tyCoFVsBndr :: TyVarBinder -> FV -> FV +tyCoFVsBndr :: TyCoVarBinder -> FV -> FV -- Free vars of (forall b. <thing with fvs>) -tyCoFVsBndr (TvBndr tv _) fvs = (delFV tv fvs) - `unionFV` tyCoFVsOfType (tyVarKind tv) +tyCoFVsBndr (Bndr tv _) fvs = (delFV tv fvs) + `unionFV` tyCoFVsOfType (varType tv) -- | Returns free variables of types, including kind variables as -- a non-deterministic set. For type synonyms it does /not/ expand the @@ -1439,10 +1693,17 @@ tyCoVarsOfCoList :: Coercion -> [TyCoVar] -- See Note [Free variables of types] tyCoVarsOfCoList co = fvVarList $ tyCoFVsOfCo co +tyCoFVsOfMCo :: MCoercion -> FV +tyCoFVsOfMCo MRefl = emptyFV +tyCoFVsOfMCo (MCo co) = tyCoFVsOfCo co + tyCoFVsOfCo :: Coercion -> FV -- Extracts type and coercion variables from a coercion -- See Note [Free variables of types] -tyCoFVsOfCo (Refl _ ty) fv_cand in_scope acc = tyCoFVsOfType ty fv_cand in_scope acc +tyCoFVsOfCo (Refl ty) fv_cand in_scope acc + = tyCoFVsOfType ty fv_cand in_scope acc +tyCoFVsOfCo (GRefl _ ty mco) fv_cand in_scope acc + = (tyCoFVsOfType ty `unionFV` tyCoFVsOfMCo mco) fv_cand in_scope acc tyCoFVsOfCo (TyConAppCo _ _ cos) fv_cand in_scope acc = tyCoFVsOfCos cos fv_cand in_scope acc tyCoFVsOfCo (AppCo co arg) fv_cand in_scope acc = (tyCoFVsOfCo co `unionFV` tyCoFVsOfCo arg) fv_cand in_scope acc @@ -1451,21 +1712,27 @@ tyCoFVsOfCo (ForAllCo tv kind_co co) fv_cand in_scope acc tyCoFVsOfCo (FunCo _ co1 co2) fv_cand in_scope acc = (tyCoFVsOfCo co1 `unionFV` tyCoFVsOfCo co2) fv_cand in_scope acc tyCoFVsOfCo (CoVarCo v) fv_cand in_scope acc - = (unitFV v `unionFV` tyCoFVsOfType (varType v)) fv_cand in_scope acc + = tyCoFVsOfCoVar v fv_cand in_scope acc +tyCoFVsOfCo (HoleCo h) fv_cand in_scope acc + = tyCoFVsOfCoVar (coHoleCoVar h) fv_cand in_scope acc + -- See Note [CoercionHoles and coercion free variables] tyCoFVsOfCo (AxiomInstCo _ _ cos) fv_cand in_scope acc = tyCoFVsOfCos cos fv_cand in_scope acc tyCoFVsOfCo (UnivCo p _ t1 t2) fv_cand in_scope acc = (tyCoFVsOfProv p `unionFV` tyCoFVsOfType t1 - `unionFV` tyCoFVsOfType t2) fv_cand in_scope acc + `unionFV` tyCoFVsOfType t2) fv_cand in_scope acc tyCoFVsOfCo (SymCo co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc tyCoFVsOfCo (TransCo co1 co2) fv_cand in_scope acc = (tyCoFVsOfCo co1 `unionFV` tyCoFVsOfCo co2) fv_cand in_scope acc -tyCoFVsOfCo (NthCo _ co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc +tyCoFVsOfCo (NthCo _ _ co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc tyCoFVsOfCo (LRCo _ co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc tyCoFVsOfCo (InstCo co arg) fv_cand in_scope acc = (tyCoFVsOfCo co `unionFV` tyCoFVsOfCo arg) fv_cand in_scope acc -tyCoFVsOfCo (CoherenceCo c1 c2) fv_cand in_scope acc = (tyCoFVsOfCo c1 `unionFV` tyCoFVsOfCo c2) fv_cand in_scope acc tyCoFVsOfCo (KindCo co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc tyCoFVsOfCo (SubCo co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc tyCoFVsOfCo (AxiomRuleCo _ cs) fv_cand in_scope acc = tyCoFVsOfCos cs fv_cand in_scope acc +tyCoFVsOfCoVar :: CoVar -> FV +tyCoFVsOfCoVar v fv_cand in_scope acc + = (unitFV v `unionFV` tyCoFVsOfType (varType v)) fv_cand in_scope acc + tyCoVarsOfProv :: UnivCoProvenance -> TyCoVarSet tyCoVarsOfProv prov = fvVarSet $ tyCoFVsOfProv prov @@ -1474,7 +1741,6 @@ tyCoFVsOfProv UnsafeCoerceProv fv_cand in_scope acc = emptyFV fv_cand in_scop tyCoFVsOfProv (PhantomProv co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc tyCoFVsOfProv (ProofIrrelProv co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc tyCoFVsOfProv (PluginProv _) fv_cand in_scope acc = emptyFV fv_cand in_scope acc -tyCoFVsOfProv (HoleProv _) fv_cand in_scope acc = emptyFV fv_cand in_scope acc tyCoVarsOfCos :: [Coercion] -> TyCoVarSet tyCoVarsOfCos cos = fvVarSet $ tyCoFVsOfCos cos @@ -1494,42 +1760,50 @@ coVarsOfType (TyConApp _ tys) = coVarsOfTypes tys coVarsOfType (LitTy {}) = emptyVarSet coVarsOfType (AppTy fun arg) = coVarsOfType fun `unionVarSet` coVarsOfType arg coVarsOfType (FunTy arg res) = coVarsOfType arg `unionVarSet` coVarsOfType res -coVarsOfType (ForAllTy (TvBndr tv _) ty) +coVarsOfType (ForAllTy (Bndr tv _) ty) = (coVarsOfType ty `delVarSet` tv) - `unionVarSet` coVarsOfType (tyVarKind tv) + `unionVarSet` coVarsOfType (varType tv) coVarsOfType (CastTy ty co) = coVarsOfType ty `unionVarSet` coVarsOfCo co coVarsOfType (CoercionTy co) = coVarsOfCo co coVarsOfTypes :: [Type] -> TyCoVarSet coVarsOfTypes tys = mapUnionVarSet coVarsOfType tys +coVarsOfMCo :: MCoercion -> CoVarSet +coVarsOfMCo MRefl = emptyVarSet +coVarsOfMCo (MCo co) = coVarsOfCo co + coVarsOfCo :: Coercion -> CoVarSet -- Extract *coercion* variables only. Tiresome to repeat the code, but easy. -coVarsOfCo (Refl _ ty) = coVarsOfType ty +coVarsOfCo (Refl ty) = coVarsOfType ty +coVarsOfCo (GRefl _ ty co) = coVarsOfType ty `unionVarSet` coVarsOfMCo co coVarsOfCo (TyConAppCo _ _ args) = coVarsOfCos args coVarsOfCo (AppCo co arg) = coVarsOfCo co `unionVarSet` coVarsOfCo arg coVarsOfCo (ForAllCo tv kind_co co) = coVarsOfCo co `delVarSet` tv `unionVarSet` coVarsOfCo kind_co -coVarsOfCo (FunCo _ co1 co2) = coVarsOfCo co1 `unionVarSet` coVarsOfCo co2 -coVarsOfCo (CoVarCo v) = unitVarSet v `unionVarSet` coVarsOfType (varType v) -coVarsOfCo (AxiomInstCo _ _ args) = coVarsOfCos args -coVarsOfCo (UnivCo p _ t1 t2) = coVarsOfProv p `unionVarSet` coVarsOfTypes [t1, t2] -coVarsOfCo (SymCo co) = coVarsOfCo co -coVarsOfCo (TransCo co1 co2) = coVarsOfCo co1 `unionVarSet` coVarsOfCo co2 -coVarsOfCo (NthCo _ co) = coVarsOfCo co -coVarsOfCo (LRCo _ co) = coVarsOfCo co -coVarsOfCo (InstCo co arg) = coVarsOfCo co `unionVarSet` coVarsOfCo arg -coVarsOfCo (CoherenceCo c1 c2) = coVarsOfCos [c1, c2] -coVarsOfCo (KindCo co) = coVarsOfCo co -coVarsOfCo (SubCo co) = coVarsOfCo co -coVarsOfCo (AxiomRuleCo _ cs) = coVarsOfCos cs +coVarsOfCo (FunCo _ co1 co2) = coVarsOfCo co1 `unionVarSet` coVarsOfCo co2 +coVarsOfCo (CoVarCo v) = coVarsOfCoVar v +coVarsOfCo (HoleCo h) = coVarsOfCoVar (coHoleCoVar h) + -- See Note [CoercionHoles and coercion free variables] +coVarsOfCo (AxiomInstCo _ _ as) = coVarsOfCos as +coVarsOfCo (UnivCo p _ t1 t2) = coVarsOfProv p `unionVarSet` coVarsOfTypes [t1, t2] +coVarsOfCo (SymCo co) = coVarsOfCo co +coVarsOfCo (TransCo co1 co2) = coVarsOfCo co1 `unionVarSet` coVarsOfCo co2 +coVarsOfCo (NthCo _ _ co) = coVarsOfCo co +coVarsOfCo (LRCo _ co) = coVarsOfCo co +coVarsOfCo (InstCo co arg) = coVarsOfCo co `unionVarSet` coVarsOfCo arg +coVarsOfCo (KindCo co) = coVarsOfCo co +coVarsOfCo (SubCo co) = coVarsOfCo co +coVarsOfCo (AxiomRuleCo _ cs) = coVarsOfCos cs + +coVarsOfCoVar :: CoVar -> CoVarSet +coVarsOfCoVar v = unitVarSet v `unionVarSet` coVarsOfType (varType v) coVarsOfProv :: UnivCoProvenance -> CoVarSet coVarsOfProv UnsafeCoerceProv = emptyVarSet coVarsOfProv (PhantomProv co) = coVarsOfCo co coVarsOfProv (ProofIrrelProv co) = coVarsOfCo co coVarsOfProv (PluginProv _) = emptyVarSet -coVarsOfProv (HoleProv _) = emptyVarSet coVarsOfCos :: [Coercion] -> CoVarSet coVarsOfCos cos = mapUnionVarSet coVarsOfCo cos @@ -1558,6 +1832,41 @@ closeOverKindsList tvs = fvVarList $ closeOverKindsFV tvs closeOverKindsDSet :: DTyVarSet -> DTyVarSet closeOverKindsDSet = fvDVarSet . closeOverKindsFV . dVarSetElems +-- | Returns the free variables of a 'TyConBinder' that are in injective +-- positions. (See @Note [Kind annotations on TyConApps]@ in "TcSplice" for an +-- explanation of what an injective position is.) +injectiveVarsOfBinder :: TyConBinder -> FV +injectiveVarsOfBinder (Bndr tv vis) = + case vis of + AnonTCB -> injectiveVarsOfType (varType tv) + NamedTCB Required -> unitFV tv `unionFV` + injectiveVarsOfType (varType tv) + NamedTCB _ -> emptyFV + +-- | Returns the free variables of a 'Type' that are in injective positions. +-- (See @Note [Kind annotations on TyConApps]@ in "TcSplice" for an explanation +-- of what an injective position is.) +injectiveVarsOfType :: Type -> FV +injectiveVarsOfType = go + where + go ty | Just ty' <- coreView ty + = go ty' + go (TyVarTy v) = unitFV v `unionFV` go (tyVarKind v) + go (AppTy f a) = go f `unionFV` go a + go (FunTy ty1 ty2) = go ty1 `unionFV` go ty2 + go (TyConApp tc tys) = + case tyConInjectivityInfo tc of + NotInjective -> emptyFV + Injective inj -> mapUnionFV go $ + filterByList (inj ++ repeat True) tys + -- Oversaturated arguments to a tycon are + -- always injective, hence the repeat True + go (ForAllTy tvb ty) = tyCoFVsBndr tvb $ go (binderType tvb) + `unionFV` go ty + go LitTy{} = emptyFV + go (CastTy ty _) = go ty + go CoercionTy{} = emptyFV + -- | Returns True if this type has no free variables. Should be the same as -- isEmptyVarSet . tyCoVarsOfType, but faster in the non-forall case. noFreeVarsOfType :: Type -> Bool @@ -1570,25 +1879,33 @@ noFreeVarsOfType (LitTy _) = True noFreeVarsOfType (CastTy ty co) = noFreeVarsOfType ty && noFreeVarsOfCo co noFreeVarsOfType (CoercionTy co) = noFreeVarsOfCo co +noFreeVarsOfMCo :: MCoercion -> Bool +noFreeVarsOfMCo MRefl = True +noFreeVarsOfMCo (MCo co) = noFreeVarsOfCo co + +noFreeVarsOfTypes :: [Type] -> Bool +noFreeVarsOfTypes = all noFreeVarsOfType + -- | Returns True if this coercion has no free variables. Should be the same as -- isEmptyVarSet . tyCoVarsOfCo, but faster in the non-forall case. noFreeVarsOfCo :: Coercion -> Bool -noFreeVarsOfCo (Refl _ ty) = noFreeVarsOfType ty +noFreeVarsOfCo (Refl ty) = noFreeVarsOfType ty +noFreeVarsOfCo (GRefl _ ty co) = noFreeVarsOfType ty && noFreeVarsOfMCo co noFreeVarsOfCo (TyConAppCo _ _ args) = all noFreeVarsOfCo args noFreeVarsOfCo (AppCo c1 c2) = noFreeVarsOfCo c1 && noFreeVarsOfCo c2 noFreeVarsOfCo co@(ForAllCo {}) = isEmptyVarSet (tyCoVarsOfCo co) noFreeVarsOfCo (FunCo _ c1 c2) = noFreeVarsOfCo c1 && noFreeVarsOfCo c2 noFreeVarsOfCo (CoVarCo _) = False +noFreeVarsOfCo (HoleCo {}) = True -- I'm unsure; probably never happens noFreeVarsOfCo (AxiomInstCo _ _ args) = all noFreeVarsOfCo args noFreeVarsOfCo (UnivCo p _ t1 t2) = noFreeVarsOfProv p && noFreeVarsOfType t1 && noFreeVarsOfType t2 noFreeVarsOfCo (SymCo co) = noFreeVarsOfCo co noFreeVarsOfCo (TransCo co1 co2) = noFreeVarsOfCo co1 && noFreeVarsOfCo co2 -noFreeVarsOfCo (NthCo _ co) = noFreeVarsOfCo co +noFreeVarsOfCo (NthCo _ _ co) = noFreeVarsOfCo co noFreeVarsOfCo (LRCo _ co) = noFreeVarsOfCo co noFreeVarsOfCo (InstCo co1 co2) = noFreeVarsOfCo co1 && noFreeVarsOfCo co2 -noFreeVarsOfCo (CoherenceCo co1 co2) = noFreeVarsOfCo co1 && noFreeVarsOfCo co2 noFreeVarsOfCo (KindCo co) = noFreeVarsOfCo co noFreeVarsOfCo (SubCo co) = noFreeVarsOfCo co noFreeVarsOfCo (AxiomRuleCo _ cs) = all noFreeVarsOfCo cs @@ -1600,7 +1917,6 @@ noFreeVarsOfProv UnsafeCoerceProv = True noFreeVarsOfProv (PhantomProv co) = noFreeVarsOfCo co noFreeVarsOfProv (ProofIrrelProv co) = noFreeVarsOfCo co noFreeVarsOfProv (PluginProv {}) = True -noFreeVarsOfProv (HoleProv {}) = True -- matches with coVarsOfProv, but I'm unsure {- %************************************************************************ @@ -1628,7 +1944,7 @@ data TCvSubst = TCvSubst InScopeSet -- The in-scope type and kind variables TvSubstEnv -- Substitutes both type and kind variables CvSubstEnv -- Substitutes coercion variables - -- See Note [Apply Once] + -- See Note [Substitutions apply only once] -- and Note [Extending the TvSubstEnv] -- and Note [Substituting types and coercions] -- and Note [The substitution invariant] @@ -1636,21 +1952,51 @@ data TCvSubst -- | A substitution of 'Type's for 'TyVar's -- and 'Kind's for 'KindVar's type TvSubstEnv = TyVarEnv Type - -- A TvSubstEnv is used both inside a TCvSubst (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 + -- NB: A TvSubstEnv is used + -- both inside a TCvSubst (with the apply-once invariant + -- discussed in Note [Substitutions apply only 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 -- | A substitution of 'Coercion's for 'CoVar's type CvSubstEnv = CoVarEnv Coercion -{- -Note [Apply Once] -~~~~~~~~~~~~~~~~~ +{- Note [The substitution invariant] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +When calling (substTy subst ty) it should be the case that +the in-scope set in the substitution is a superset of both: + + (SIa) The free vars of the range of the substitution + (SIb) The free vars of ty minus the domain of the substitution + +The same rules apply to other substitutions (notably CoreSubst.Subst) + +* Reason for (SIa). Consider + substTy [a :-> Maybe b] (forall b. b->a) + we must rename the forall b, to get + forall b2. b2 -> Maybe b + Making 'b' part of the in-scope set forces this renaming to + take place. + +* Reason for (SIb). Consider + substTy [a :-> Maybe b] (forall b. (a,b,x)) + Then if we use the in-scope set {b}, satisfying (SIa), there is + a danger we will rename the forall'd variable to 'x' by mistake, + getting this: + forall x. (Maybe b, x, x) + Breaking (SIb) caused the bug from #11371. + +Note: if the free vars of the range of the substitution are freshly created, +then the problems of (SIa) can't happen, and so it would be sound to +ignore (SIa). + +Note [Substitutions apply only once] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We use TCvSubsts to instantiate things, and we might instantiate forall a b. ty -\with the types +with the types [a, b], or [b, a]. So the substitution might go [a->b, b->a]. A similar situation arises in Core when we find a beta redex like @@ -1658,9 +2004,9 @@ when we find a beta redex like Then we also end up with a substitution that permutes type variables. Other variations happen to; for example [a -> (a, b)]. - **************************************************** - *** So a TCvSubst must be applied precisely once *** - **************************************************** + ******************************************************** + *** So a substitution must be applied precisely once *** + ******************************************************** A TCvSubst is not idempotent, but, unlike the non-idempotent substitution we use during unifications, it must not be repeatedly applied. @@ -1680,7 +2026,7 @@ nevertheless we add 'b' to the TvSubstEnv, because b's kind does change This invariant has several crucial consequences: -* In substTyVarBndr, we need extend the TvSubstEnv +* In substVarBndr, we need extend the TvSubstEnv - if the unique has changed - or if the kind has changed @@ -1703,25 +2049,6 @@ Note that the TvSubstEnv should *never* map a CoVar (built with the Id constructor) and the CvSubstEnv should *never* map a TyVar. Furthermore, the range of the TvSubstEnv should *never* include a type headed with CoercionTy. - -Note [The substitution invariant] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -When calling (substTy subst ty) it should be the case that -the in-scope set in the substitution is a superset of both: - - * The free vars of the range of the substitution - * The free vars of ty minus the domain of the substitution - -If we want to substitute [a -> ty1, b -> ty2] I used to -think it was enough to generate an in-scope set that includes -fv(ty1,ty2). But that's not enough; we really should also take the -free vars of the type we are substituting into! Example: - (forall b. (a,b,x)) [a -> List b] -Then if we use the in-scope set {b}, there is a danger we will rename -the forall'd variable to 'x' by mistake, getting this: - (forall x. (List b, x, x)) - -Breaking this invariant caused the bug from #11371. -} emptyTvSubstEnv :: TvSubstEnv @@ -1773,6 +2100,10 @@ mkTvSubst :: InScopeSet -> TvSubstEnv -> TCvSubst -- ^ Make a TCvSubst with specified tyvar subst and empty covar subst mkTvSubst in_scope tenv = TCvSubst in_scope tenv emptyCvSubstEnv +mkCvSubst :: InScopeSet -> CvSubstEnv -> TCvSubst +-- ^ Make a TCvSubst with specified covar subst and empty tyvar subst +mkCvSubst in_scope cenv = TCvSubst in_scope emptyTvSubstEnv cenv + getTvSubstEnv :: TCvSubst -> TvSubstEnv getTvSubstEnv (TCvSubst _ env _) = env @@ -1831,14 +2162,20 @@ extendTCvSubst subst v ty | otherwise = pprPanic "extendTCvSubst" (ppr v <+> text "|->" <+> ppr ty) +extendTCvSubstWithClone :: TCvSubst -> TyCoVar -> TyCoVar -> TCvSubst +extendTCvSubstWithClone subst tcv + | isTyVar tcv = extendTvSubstWithClone subst tcv + | otherwise = extendCvSubstWithClone subst tcv + extendTvSubst :: TCvSubst -> TyVar -> Type -> TCvSubst extendTvSubst (TCvSubst in_scope tenv cenv) tv ty = TCvSubst in_scope (extendVarEnv tenv tv ty) cenv -extendTvSubstBinder :: TCvSubst -> TyBinder -> Type -> TCvSubst -extendTvSubstBinder subst (Named bndr) ty - = extendTvSubst subst (binderVar bndr) ty -extendTvSubstBinder subst (Anon _) _ +extendTvSubstBinderAndInScope :: TCvSubst -> TyCoBinder -> Type -> TCvSubst +extendTvSubstBinderAndInScope subst (Named (Bndr v _)) ty + = ASSERT( isTyVar v ) + extendTvSubstAndInScope subst v ty +extendTvSubstBinderAndInScope subst (Anon _) _ = subst extendTvSubstWithClone :: TCvSubst -> TyVar -> TyVar -> TCvSubst @@ -1873,6 +2210,10 @@ extendTvSubstList :: TCvSubst -> [Var] -> [Type] -> TCvSubst extendTvSubstList subst tvs tys = foldl2 extendTvSubst subst tvs tys +extendTCvSubstList :: TCvSubst -> [Var] -> [Type] -> TCvSubst +extendTCvSubstList subst tvs tys + = foldl2 extendTCvSubst subst tvs tys + unionTCvSubst :: TCvSubst -> TCvSubst -> TCvSubst -- Works when the ranges are disjoint unionTCvSubst (TCvSubst in_scope1 tenv1 cenv1) (TCvSubst in_scope2 tenv2 cenv2) @@ -1916,6 +2257,18 @@ zipCvSubst cvs cos where cenv = zipCoEnv cvs cos +zipTCvSubst :: [TyCoVar] -> [Type] -> TCvSubst +zipTCvSubst tcvs tys + | debugIsOn + , neLength tcvs tys + = pprTrace "zipTCvSubst" (ppr tcvs $$ ppr tys) emptyTCvSubst + | otherwise + = zip_tcvsubst tcvs tys (mkEmptyTCvSubst $ mkInScopeSet (tyCoVarsOfTypes tys)) + where zip_tcvsubst :: [TyCoVar] -> [Type] -> TCvSubst -> TCvSubst + zip_tcvsubst (tv:tvs) (ty:tys) subst + = zip_tcvsubst tvs tys (extendTCvSubst subst tv ty) + zip_tcvsubst _ _ subst = subst -- empty case + -- | Generates the in-scope set for the 'TCvSubst' from the types in the -- incoming environment. No CoVars, please! mkTvSubstPrs :: [(TyVar, Type)] -> TCvSubst @@ -2002,13 +2355,42 @@ sym (ForAllCo tv h g) ==> ForAllCo tv (sym h) (sym g[tv |-> tv |> sym h]) +Note [Substituting in a coercion hole] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +It seems highly suspicious to be substituting in a coercion that still +has coercion holes. Yet, this can happen in a situation like this: + + f :: forall k. k :~: Type -> () + f Refl = let x :: forall (a :: k). [a] -> ... + x = ... + +When we check x's type signature, we require that k ~ Type. We indeed +know this due to the Refl pattern match, but the eager unifier can't +make use of givens. So, when we're done looking at x's type, a coercion +hole will remain. Then, when we're checking x's definition, we skolemise +x's type (in order to, e.g., bring the scoped type variable `a` into scope). +This requires performing a substitution for the fresh skolem variables. + +This subsitution needs to affect the kind of the coercion hole, too -- +otherwise, the kind will have an out-of-scope variable in it. More problematically +in practice (we won't actually notice the out-of-scope variable ever), skolems +in the kind might have too high a level, triggering a failure to uphold the +invariant that no free variables in a type have a higher level than the +ambient level in the type checker. In the event of having free variables in the +hole's kind, I'm pretty sure we'll always have an erroneous program, so we +don't need to worry what will happen when the hole gets filled in. After all, +a hole relating a locally-bound type variable will be unable to be solved. This +is why it's OK not to look through the IORef of a coercion hole during +substitution. + -} -- | Type substitution, see 'zipTvSubst' substTyWith :: HasCallStack => [TyVar] -> [Type] -> Type -> Type -- Works only if the domain of the substitution is a -- superset of the type being substituted into -substTyWith tvs tys = ASSERT( tvs `equalLength` tys ) +substTyWith tvs tys = {-#SCC "substTyWith" #-} + ASSERT( tvs `equalLength` tys ) substTy (zipTvSubst tvs tys) -- | Type substitution, see 'zipTvSubst'. Disables sanity checks. @@ -2086,17 +2468,16 @@ isValidTCvSubst (TCvSubst in_scope tenv cenv) = -- Note [The substitution invariant]. checkValidSubst :: HasCallStack => TCvSubst -> [Type] -> [Coercion] -> a -> a checkValidSubst subst@(TCvSubst in_scope tenv cenv) tys cos a - = ASSERT2( isValidTCvSubst subst, +-- TODO (RAE): Change back to ASSERT + = WARN( not (isValidTCvSubst subst), text "in_scope" <+> ppr in_scope $$ text "tenv" <+> ppr tenv $$ - text "tenvFVs" - <+> ppr (tyCoVarsOfTypesSet tenv) $$ + text "tenvFVs" <+> ppr (tyCoVarsOfTypesSet tenv) $$ text "cenv" <+> ppr cenv $$ - text "cenvFVs" - <+> ppr (tyCoVarsOfCosSet cenv) $$ + text "cenvFVs" <+> ppr (tyCoVarsOfCosSet cenv) $$ text "tys" <+> ppr tys $$ text "cos" <+> ppr cos ) - ASSERT2( tysCosFVsInScope, + WARN( not tysCosFVsInScope, text "in_scope" <+> ppr in_scope $$ text "tenv" <+> ppr tenv $$ text "cenv" <+> ppr cenv $$ @@ -2181,10 +2562,10 @@ subst_ty subst ty go (TyConApp tc tys) = let args = map go tys in args `seqList` TyConApp tc args go (FunTy arg res) = (FunTy $! go arg) $! go res - go (ForAllTy (TvBndr tv vis) ty) - = case substTyVarBndrUnchecked subst tv of + go (ForAllTy (Bndr tv vis) ty) + = case substVarBndrUnchecked subst tv of (subst', tv') -> - (ForAllTy $! ((TvBndr $! tv') vis)) $! + (ForAllTy $! ((Bndr $! tv') vis)) $! (subst_ty subst' ty) go (LitTy n) = LitTy $! n go (CastTy ty co) = (mkCastTy $! (go ty)) $! (subst_co subst co) @@ -2200,6 +2581,14 @@ substTyVar (TCvSubst _ tenv _) tv substTyVars :: TCvSubst -> [TyVar] -> [Type] substTyVars subst = map $ substTyVar subst +substTyCoVars :: TCvSubst -> [TyCoVar] -> [Type] +substTyCoVars subst = map $ substTyCoVar subst + +substTyCoVar :: TCvSubst -> TyCoVar -> Type +substTyCoVar subst tv + | isTyVar tv = substTyVar subst tv + | otherwise = CoercionTy $ substCoVar subst tv + lookupTyVar :: TCvSubst -> TyVar -> Maybe Type -- See Note [Extending the TCvSubst] lookupTyVar (TCvSubst _ tenv _) tv @@ -2239,14 +2628,20 @@ subst_co subst co go_ty :: Type -> Type go_ty = subst_ty subst + go_mco :: MCoercion -> MCoercion + go_mco MRefl = MRefl + go_mco (MCo co) = MCo (go co) + go :: Coercion -> Coercion - go (Refl r ty) = mkReflCo r $! go_ty ty + go (Refl ty) = mkNomReflCo $! (go_ty ty) + go (GRefl r ty mco) = (mkGReflCo r $! (go_ty ty)) $! (go_mco mco) go (TyConAppCo r tc args)= let args' = map go args in args' `seqList` mkTyConAppCo r tc args' go (AppCo co arg) = (mkAppCo $! go co) $! go arg go (ForAllCo tv kind_co co) - = case substForAllCoBndrUnchecked subst tv kind_co of { (subst', tv', kind_co') -> - ((mkForAllCo $! tv') $! kind_co') $! subst_co subst' co } + = case substForAllCoBndrUnchecked subst tv kind_co of + (subst', tv', kind_co') -> + ((mkForAllCo $! tv') $! kind_co') $! subst_co subst' co go (FunCo r co1 co2) = (mkFunCo r $! go co1) $! go co2 go (CoVarCo cv) = substCoVar subst cv go (AxiomInstCo con ind cos) = mkAxiomInstCo con ind $! map go cos @@ -2254,51 +2649,60 @@ subst_co subst co (go_ty t1)) $! (go_ty t2) go (SymCo co) = mkSymCo $! (go co) go (TransCo co1 co2) = (mkTransCo $! (go co1)) $! (go co2) - go (NthCo d co) = mkNthCo d $! (go co) + go (NthCo r d co) = mkNthCo r d $! (go co) go (LRCo lr co) = mkLRCo lr $! (go co) go (InstCo co arg) = (mkInstCo $! (go co)) $! go arg - go (CoherenceCo co1 co2) = (mkCoherenceCo $! (go co1)) $! (go co2) go (KindCo co) = mkKindCo $! (go co) go (SubCo co) = mkSubCo $! (go co) go (AxiomRuleCo c cs) = let cs1 = map go cs in cs1 `seqList` AxiomRuleCo c cs1 + go (HoleCo h) = HoleCo $! go_hole h go_prov UnsafeCoerceProv = UnsafeCoerceProv go_prov (PhantomProv kco) = PhantomProv (go kco) go_prov (ProofIrrelProv kco) = ProofIrrelProv (go kco) go_prov p@(PluginProv _) = p - go_prov p@(HoleProv _) = p - -- NB: this last case is a little suspicious, but we need it. Originally, - -- there was a panic here, but it triggered from deeplySkolemise. Because - -- we only skolemise tyvars that are manually bound, this operation makes - -- sense, even over a coercion with holes. -substForAllCoBndr :: TCvSubst -> TyVar -> Coercion -> (TCvSubst, TyVar, Coercion) + -- See Note [Substituting in a coercion hole] + go_hole h@(CoercionHole { ch_co_var = cv }) + = h { ch_co_var = updateVarType go_ty cv } + +substForAllCoBndr :: TCvSubst -> TyCoVar -> KindCoercion + -> (TCvSubst, TyCoVar, Coercion) substForAllCoBndr subst - = substForAllCoBndrCallback False (substCo subst) subst + = substForAllCoBndrUsing False (substCo subst) subst -- | Like 'substForAllCoBndr', but disables sanity checks. -- The problems that the sanity checks in substCo catch are described in -- Note [The substitution invariant]. -- The goal of #11371 is to migrate all the calls of substCoUnchecked to -- substCo and remove this function. Please don't use in new code. -substForAllCoBndrUnchecked :: TCvSubst -> TyVar -> Coercion -> (TCvSubst, TyVar, Coercion) +substForAllCoBndrUnchecked :: TCvSubst -> TyCoVar -> KindCoercion + -> (TCvSubst, TyCoVar, Coercion) substForAllCoBndrUnchecked subst - = substForAllCoBndrCallback False (substCoUnchecked subst) subst + = substForAllCoBndrUsing False (substCoUnchecked subst) subst -- See Note [Sym and ForAllCo] -substForAllCoBndrCallback :: Bool -- apply sym to binder? - -> (Coercion -> Coercion) -- transformation to kind co - -> TCvSubst -> TyVar -> Coercion - -> (TCvSubst, TyVar, Coercion) -substForAllCoBndrCallback sym sco (TCvSubst in_scope tenv cenv) - old_var old_kind_co - = ( TCvSubst (in_scope `extendInScopeSet` new_var) new_env cenv +substForAllCoBndrUsing :: Bool -- apply sym to binder? + -> (Coercion -> Coercion) -- transformation to kind co + -> TCvSubst -> TyCoVar -> KindCoercion + -> (TCvSubst, TyCoVar, KindCoercion) +substForAllCoBndrUsing sym sco subst old_var + | isTyVar old_var = substForAllCoTyVarBndrUsing sym sco subst old_var + | otherwise = substForAllCoCoVarBndrUsing sym sco subst old_var + +substForAllCoTyVarBndrUsing :: Bool -- apply sym to binder? + -> (Coercion -> Coercion) -- transformation to kind co + -> TCvSubst -> TyVar -> KindCoercion + -> (TCvSubst, TyVar, KindCoercion) +substForAllCoTyVarBndrUsing sym sco (TCvSubst in_scope tenv cenv) old_var old_kind_co + = ASSERT( isTyVar old_var ) + ( TCvSubst (in_scope `extendInScopeSet` new_var) new_env cenv , new_var, new_kind_co ) where new_env | no_change && not sym = delVarEnv tenv old_var | sym = extendVarEnv tenv old_var $ - TyVarTy new_var `CastTy` new_kind_co + TyVarTy new_var `CastTy` new_kind_co | otherwise = extendVarEnv tenv old_var (TyVarTy new_var) no_kind_change = noFreeVarsOfCo old_kind_co @@ -2308,9 +2712,38 @@ substForAllCoBndrCallback sym sco (TCvSubst in_scope tenv cenv) | otherwise = sco old_kind_co Pair new_ki1 _ = coercionKind new_kind_co + -- We could do substitution to (tyVarKind old_var). We don't do so because + -- we already substituted new_kind_co, which contains the kind information + -- we want. We don't want to do substitution once more. Also, in most cases, + -- new_kind_co is a Refl, in which case coercionKind is really fast. new_var = uniqAway in_scope (setTyVarKind old_var new_ki1) +substForAllCoCoVarBndrUsing :: Bool -- apply sym to binder? + -> (Coercion -> Coercion) -- transformation to kind co + -> TCvSubst -> CoVar -> KindCoercion + -> (TCvSubst, CoVar, KindCoercion) +substForAllCoCoVarBndrUsing sym sco (TCvSubst in_scope tenv cenv) + old_var old_kind_co + = ASSERT( isCoVar old_var ) + ( TCvSubst (in_scope `extendInScopeSet` new_var) tenv new_cenv + , new_var, new_kind_co ) + where + new_cenv | no_change && not sym = delVarEnv cenv old_var + | otherwise = extendVarEnv cenv old_var (mkCoVarCo new_var) + + no_kind_change = noFreeVarsOfCo old_kind_co + no_change = no_kind_change && (new_var == old_var) + + new_kind_co | no_kind_change = old_kind_co + | otherwise = sco old_kind_co + + Pair h1 h2 = coercionKind new_kind_co + + new_var = uniqAway in_scope $ mkCoVar (varName old_var) new_var_type + new_var_type | sym = h2 + | otherwise = h1 + substCoVar :: TCvSubst -> CoVar -> Coercion substCoVar (TCvSubst _ _ cenv) cv = case lookupVarEnv cenv cv of @@ -2320,25 +2753,45 @@ substCoVar (TCvSubst _ _ cenv) cv substCoVars :: TCvSubst -> [CoVar] -> [Coercion] substCoVars subst cvs = map (substCoVar subst) cvs -lookupCoVar :: TCvSubst -> Var -> Maybe Coercion +lookupCoVar :: TCvSubst -> Var -> Maybe Coercion lookupCoVar (TCvSubst _ _ cenv) v = lookupVarEnv cenv v substTyVarBndr :: HasCallStack => TCvSubst -> TyVar -> (TCvSubst, TyVar) -substTyVarBndr = substTyVarBndrCallback substTy +substTyVarBndr = substTyVarBndrUsing substTy + +substTyVarBndrs :: HasCallStack => TCvSubst -> [TyVar] -> (TCvSubst, [TyVar]) +substTyVarBndrs = mapAccumL substTyVarBndr + +substVarBndr :: HasCallStack => TCvSubst -> TyCoVar -> (TCvSubst, TyCoVar) +substVarBndr = substVarBndrUsing substTy + +substVarBndrs :: HasCallStack => TCvSubst -> [TyCoVar] -> (TCvSubst, [TyCoVar]) +substVarBndrs = mapAccumL substVarBndr --- | Like 'substTyVarBndr' but disables sanity checks. +substCoVarBndr :: HasCallStack => TCvSubst -> CoVar -> (TCvSubst, CoVar) +substCoVarBndr = substCoVarBndrUsing substTy + +-- | Like 'substVarBndr', but disables sanity checks. -- The problems that the sanity checks in substTy catch are described in -- Note [The substitution invariant]. -- The goal of #11371 is to migrate all the calls of substTyUnchecked to -- substTy and remove this function. Please don't use in new code. -substTyVarBndrUnchecked :: TCvSubst -> TyVar -> (TCvSubst, TyVar) -substTyVarBndrUnchecked = substTyVarBndrCallback substTyUnchecked +substVarBndrUnchecked :: TCvSubst -> TyCoVar -> (TCvSubst, TyCoVar) +substVarBndrUnchecked = substVarBndrUsing substTyUnchecked + +substVarBndrUsing :: (TCvSubst -> Type -> Type) + -> TCvSubst -> TyCoVar -> (TCvSubst, TyCoVar) +substVarBndrUsing subst_fn subst v + | isTyVar v = substTyVarBndrUsing subst_fn subst v + | otherwise = substCoVarBndrUsing subst_fn subst v -- | Substitute a tyvar in a binding position, returning an -- extended subst and a new tyvar. -substTyVarBndrCallback :: (TCvSubst -> Type -> Type) -- ^ the subst function - -> TCvSubst -> TyVar -> (TCvSubst, TyVar) -substTyVarBndrCallback subst_fn subst@(TCvSubst in_scope tenv cenv) old_var +-- Use the supplied function to substitute in the kind +substTyVarBndrUsing + :: (TCvSubst -> Type -> Type) -- ^ Use this to substitute in the kind + -> TCvSubst -> TyVar -> (TCvSubst, TyVar) +substTyVarBndrUsing subst_fn subst@(TCvSubst in_scope tenv cenv) old_var = ASSERT2( _no_capture, pprTyVar old_var $$ pprTyVar new_var $$ ppr subst ) ASSERT( isTyVar old_var ) (TCvSubst (in_scope `extendInScopeSet` new_var) new_env cenv, new_var) @@ -2367,13 +2820,18 @@ substTyVarBndrCallback subst_fn subst@(TCvSubst in_scope tenv cenv) old_var setTyVarKind old_var (subst_fn subst old_ki) -- The uniqAway part makes sure the new variable is not already in scope -substCoVarBndr :: TCvSubst -> CoVar -> (TCvSubst, CoVar) -substCoVarBndr subst@(TCvSubst in_scope tenv cenv) old_var +-- | Substitute a covar in a binding position, returning an +-- extended subst and a new covar. +-- Use the supplied function to substitute in the kind +substCoVarBndrUsing + :: (TCvSubst -> Type -> Type) + -> TCvSubst -> CoVar -> (TCvSubst, CoVar) +substCoVarBndrUsing subst_fn subst@(TCvSubst in_scope tenv cenv) old_var = ASSERT( isCoVar old_var ) (TCvSubst (in_scope `extendInScopeSet` new_var) tenv new_cenv, new_var) where new_co = mkCoVarCo new_var - no_kind_change = all noFreeVarsOfType [t1, t2] + no_kind_change = noFreeVarsOfTypes [t1, t2] no_change = new_var == old_var && no_kind_change new_cenv | no_change = delVarEnv cenv old_var @@ -2383,8 +2841,8 @@ substCoVarBndr subst@(TCvSubst in_scope tenv cenv) old_var subst_old_var = mkCoVar (varName old_var) new_var_type (_, _, t1, t2, role) = coVarKindsTypesRole old_var - t1' = substTy subst t1 - t2' = substTy subst t2 + t1' = subst_fn subst t1 + t2' = subst_fn subst t2 new_var_type = mkCoercionType role t1' t2' -- It's important to do the substitution for coercions, -- because they can have free type variables @@ -2425,17 +2883,28 @@ defined to use this. @pprParendType@ is the same, except it puts parens around the type, except for the atomic cases. @pprParendType@ works just by setting the initial context precedence very high. +Note that any function which pretty-prints a @Type@ first converts the @Type@ +to an @IfaceType@. See Note [IfaceType and pretty-printing] in IfaceType. + See Note [Precedence in types] in BasicTypes. -} ------------------- +-------------------------------------------------------- +-- When pretty-printing types, we convert to IfaceType, +-- and pretty-print that. +-- See Note [Pretty printing via IfaceSyn] in PprTyThing +-------------------------------------------------------- pprType, pprParendType :: Type -> SDoc -pprType = pprPrecType TopPrec -pprParendType = pprPrecType TyConPrec +pprType = pprPrecType topPrec +pprParendType = pprPrecType appPrec -pprPrecType :: TyPrec -> Type -> SDoc -pprPrecType prec ty = pprPrecIfaceType prec (tidyToIfaceType ty) +pprPrecType :: PprPrec -> Type -> SDoc +pprPrecType prec ty + = getPprStyle $ \sty -> + if debugStyle sty -- Use pprDebugType when in + then debug_ppr_ty prec ty -- when in debug-style + else pprPrecIfaceType prec (tidyToIfaceTypeSty ty sty) pprTyLit :: TyLit -> SDoc pprTyLit = pprIfaceTyLit . toIfaceTyLit @@ -2444,6 +2913,12 @@ pprKind, pprParendKind :: Kind -> SDoc pprKind = pprType pprParendKind = pprParendType +tidyToIfaceTypeSty :: Type -> PprStyle -> IfaceType +tidyToIfaceTypeSty ty sty + | userStyle sty = tidyToIfaceType ty + | otherwise = toIfaceTypeX (tyCoVarsOfType ty) ty + -- in latter case, don't tidy, as we'll be printing uniques. + tidyToIfaceType :: Type -> IfaceType -- It's vital to tidy before converting to an IfaceType -- or nested binders will become indistinguishable! @@ -2457,15 +2932,38 @@ tidyToIfaceType ty = toIfaceTypeX (mkVarSet free_tcvs) (tidyType env ty) free_tcvs = tyCoVarsOfTypeWellScoped ty ------------ +pprCo, pprParendCo :: Coercion -> SDoc +pprCo co = getPprStyle $ \ sty -> pprIfaceCoercion (tidyToIfaceCoSty co sty) +pprParendCo co = getPprStyle $ \ sty -> pprParendIfaceCoercion (tidyToIfaceCoSty co sty) + +tidyToIfaceCoSty :: Coercion -> PprStyle -> IfaceCoercion +tidyToIfaceCoSty co sty + | userStyle sty = tidyToIfaceCo co + | otherwise = toIfaceCoercionX (tyCoVarsOfCo co) co + -- in latter case, don't tidy, as we'll be printing uniques. + +tidyToIfaceCo :: Coercion -> IfaceCoercion +-- It's vital to tidy before converting to an IfaceType +-- or nested binders will become indistinguishable! +-- +-- Also for the free type variables, tell toIfaceCoercionX to +-- leave them as IfaceFreeCoVar. This is super-important +-- for debug printing. +tidyToIfaceCo co = toIfaceCoercionX (mkVarSet free_tcvs) (tidyCo env co) + where + env = tidyFreeTyCoVars emptyTidyEnv free_tcvs + free_tcvs = toposortTyVars $ tyCoVarsOfCoList co + +------------ pprClassPred :: Class -> [Type] -> SDoc pprClassPred clas tys = pprTypeApp (classTyCon clas) tys ------------ pprTheta :: ThetaType -> SDoc -pprTheta = pprIfaceContext TopPrec . map tidyToIfaceType +pprTheta = pprIfaceContext topPrec . map tidyToIfaceType pprParendTheta :: ThetaType -> SDoc -pprParendTheta = pprIfaceContext TyConPrec . map tidyToIfaceType +pprParendTheta = pprIfaceContext appPrec . map tidyToIfaceType pprThetaArrowTy :: ThetaType -> SDoc pprThetaArrowTy = pprIfaceContextArr . map tidyToIfaceType @@ -2478,22 +2976,21 @@ instance Outputable TyLit where ppr = pprTyLit ------------------ - pprSigmaType :: Type -> SDoc pprSigmaType = pprIfaceSigmaType ShowForAllWhen . tidyToIfaceType -pprForAll :: [TyVarBinder] -> SDoc +pprForAll :: [TyCoVarBinder] -> SDoc pprForAll tvs = pprIfaceForAll (map toIfaceForAllBndr tvs) -- | Print a user-level forall; see Note [When to print foralls] -pprUserForAll :: [TyVarBinder] -> SDoc +pprUserForAll :: [TyCoVarBinder] -> SDoc pprUserForAll = pprUserIfaceForAll . map toIfaceForAllBndr -pprTvBndrs :: [TyVarBinder] -> SDoc -pprTvBndrs tvs = sep (map pprTvBndr tvs) +pprTCvBndrs :: [TyCoVarBinder] -> SDoc +pprTCvBndrs tvs = sep (map pprTCvBndr tvs) -pprTvBndr :: TyVarBinder -> SDoc -pprTvBndr = pprTyVar . binderVar +pprTCvBndr :: TyCoVarBinder -> SDoc +pprTCvBndr = pprTyVar . binderVar pprTyVars :: [TyVar] -> SDoc pprTyVars tvs = sep (map pprTyVar tvs) @@ -2509,16 +3006,67 @@ pprTyVar tv where kind = tyVarKind tv -instance Outputable TyBinder where +instance Outputable TyCoBinder where ppr (Anon ty) = text "[anon]" <+> ppr ty - ppr (Named (TvBndr v Required)) = ppr v - ppr (Named (TvBndr v Specified)) = char '@' <> ppr v - ppr (Named (TvBndr v Inferred)) = braces (ppr v) + ppr (Named (Bndr v Required)) = ppr v + ppr (Named (Bndr v Specified)) = char '@' <> ppr v + ppr (Named (Bndr v Inferred)) = braces (ppr v) ----------------- instance Outputable Coercion where -- defined here to avoid orphans ppr = pprCo +debugPprType :: Type -> SDoc +-- ^ debugPprType is a simple pretty printer that prints a type +-- without going through IfaceType. It does not format as prettily +-- as the normal route, but it's much more direct, and that can +-- be useful for debugging. E.g. with -dppr-debug it prints the +-- kind on type-variable /occurrences/ which the normal route +-- fundamentally cannot do. +debugPprType ty = debug_ppr_ty topPrec ty + +debug_ppr_ty :: PprPrec -> Type -> SDoc +debug_ppr_ty _ (LitTy l) + = ppr l + +debug_ppr_ty _ (TyVarTy tv) + = ppr tv -- With -dppr-debug we get (tv :: kind) + +debug_ppr_ty prec (FunTy arg res) + = maybeParen prec funPrec $ + sep [debug_ppr_ty funPrec arg, arrow <+> debug_ppr_ty prec res] + +debug_ppr_ty prec (TyConApp tc tys) + | null tys = ppr tc + | otherwise = maybeParen prec appPrec $ + hang (ppr tc) 2 (sep (map (debug_ppr_ty appPrec) tys)) + +debug_ppr_ty prec (AppTy t1 t2) + = hang (debug_ppr_ty prec t1) + 2 (debug_ppr_ty appPrec t2) + +debug_ppr_ty prec (CastTy ty co) + = maybeParen prec topPrec $ + hang (debug_ppr_ty topPrec ty) + 2 (text "|>" <+> ppr co) + +debug_ppr_ty _ (CoercionTy co) + = parens (text "CO" <+> ppr co) + +debug_ppr_ty prec ty@(ForAllTy {}) + | (tvs, body) <- split ty + = maybeParen prec funPrec $ + hang (text "forall" <+> fsep (map ppr tvs) <> dot) + -- The (map ppr tvs) will print kind-annotated + -- tvs, because we are (usually) in debug-style + 2 (ppr body) + where + split ty | ForAllTy tv ty' <- ty + , (tvs, body) <- split ty' + = (tv:tvs, body) + | otherwise + = ([], ty) + {- Note [When to print foralls] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -2536,7 +3084,7 @@ This catches common situations, such as a type siguature which means f :: forall k. forall (m :: k->*) (a :: k). m a We really want to see both the "forall k" and the kind signatures -on m and a. The latter comes from pprTvBndr. +on m and a. The latter comes from pprTCvBndr. Note [Infix type variables] ~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -2566,37 +3114,20 @@ pprDataCons = sepWithVBars . fmap pprDataConWithArgs . tyConDataCons pprDataConWithArgs :: DataCon -> SDoc pprDataConWithArgs dc = sep [forAllDoc, thetaDoc, ppr dc <+> argsDoc] where - (_univ_tvs, _ex_tvs, eq_spec, theta, arg_tys, _res_ty) = dataConFullSig dc - univ_bndrs = dataConUnivTyVarBinders dc - ex_bndrs = dataConExTyVarBinders dc - forAllDoc = pprUserForAll $ (filterEqSpec eq_spec univ_bndrs ++ ex_bndrs) - thetaDoc = pprThetaArrowTy theta - argsDoc = hsep (fmap pprParendType arg_tys) + (_univ_tvs, _ex_tvs, _eq_spec, theta, arg_tys, _res_ty) = dataConFullSig dc + user_bndrs = dataConUserTyVarBinders dc + forAllDoc = pprUserForAll user_bndrs + thetaDoc = pprThetaArrowTy theta + argsDoc = hsep (fmap pprParendType arg_tys) pprTypeApp :: TyCon -> [Type] -> SDoc pprTypeApp tc tys - = pprIfaceTypeApp TopPrec (toIfaceTyCon tc) + = pprIfaceTypeApp topPrec (toIfaceTyCon tc) (toIfaceTcArgs tc tys) -- TODO: toIfaceTcArgs seems rather wasteful here -pprTcAppCo :: TyPrec -> (TyPrec -> Coercion -> SDoc) - -> TyCon -> [Coercion] -> SDoc -pprTcAppCo p _pp tc cos - = pprIfaceCoTcApp p (toIfaceTyCon tc) (map toIfaceCoercion cos) - ------------------ - -pprPrefixApp :: TyPrec -> SDoc -> [SDoc] -> SDoc -pprPrefixApp = pprIfacePrefixApp - ----------------- -pprArrowChain :: TyPrec -> [SDoc] -> SDoc --- pprArrowChain p [a,b,c] generates a -> b -> c -pprArrowChain _ [] = empty -pprArrowChain p (arg:args) = maybeParen p FunPrec $ - sep [arg, sep (map (arrow <+>) args)] - ppSuggestExplicitKinds :: SDoc -- Print a helpful suggstion about -fprint-explicit-kinds, -- if it is not already on @@ -2617,32 +3148,32 @@ ppSuggestExplicitKinds -- an interface file. -- -- It doesn't change the uniques at all, just the print names. -tidyTyCoVarBndrs :: TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar]) -tidyTyCoVarBndrs (occ_env, subst) tvs - = mapAccumL tidyTyCoVarBndr tidy_env' tvs +tidyVarBndrs :: TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar]) +tidyVarBndrs (occ_env, subst) tvs + = mapAccumL tidyVarBndr tidy_env' tvs where -- Seed the occ_env with clashes among the names, see -- Node [Tidying multiple names at once] in OccName - -- Se still go through tidyTyCoVarBndr so that each kind variable is tidied + -- Se still go through tidyVarBndr so that each kind variable is tidied -- with the correct tidy_env occs = map getHelpfulOccName tvs tidy_env' = (avoidClashesOccEnv occ_env occs, subst) -tidyTyCoVarBndr :: TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar) -tidyTyCoVarBndr tidy_env@(occ_env, subst) tyvar - = case tidyOccName occ_env (getHelpfulOccName tyvar) of - (occ_env', occ') -> ((occ_env', subst'), tyvar') +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 tyvar tyvar' - tyvar' = setTyVarKind (setTyVarName tyvar name') kind' - kind' = tidyKind tidy_env (tyVarKind tyvar) + subst' = extendVarEnv subst var var' + var' = setVarType (setVarName var name') type' + type' = tidyType tidy_env (varType var) name' = tidyNameOcc name occ' - name = tyVarName tyvar + name = varName var getHelpfulOccName :: TyCoVar -> OccName -getHelpfulOccName tyvar = occ1 +getHelpfulOccName var = occ1 where - name = tyVarName tyvar + name = varName var occ = getOccName name -- A TcTyVar with a System Name is probably a unification variable; -- when we tidy them we give them a trailing "0" (or 1 etc) @@ -2650,21 +3181,21 @@ getHelpfulOccName tyvar = occ1 -- Plus, indicating a unification variable in this way is a -- helpful clue for users occ1 | isSystemName name - , isTcTyVar tyvar + , isTcTyVar var = mkTyVarOcc (occNameString occ ++ "0") | otherwise = occ -tidyTyVarBinder :: TidyEnv -> TyVarBndr TyVar vis - -> (TidyEnv, TyVarBndr TyVar vis) -tidyTyVarBinder tidy_env (TvBndr tv vis) - = (tidy_env', TvBndr tv' vis) +tidyTyCoVarBinder :: TidyEnv -> VarBndr TyCoVar vis + -> (TidyEnv, VarBndr TyCoVar vis) +tidyTyCoVarBinder tidy_env (Bndr tv vis) + = (tidy_env', Bndr tv' vis) where - (tidy_env', tv') = tidyTyCoVarBndr tidy_env tv + (tidy_env', tv') = tidyVarBndr tidy_env tv -tidyTyVarBinders :: TidyEnv -> [TyVarBndr TyVar vis] - -> (TidyEnv, [TyVarBndr TyVar vis]) -tidyTyVarBinders = mapAccumL tidyTyVarBinder +tidyTyCoVarBinders :: TidyEnv -> [VarBndr TyCoVar vis] + -> (TidyEnv, [VarBndr TyCoVar vis]) +tidyTyCoVarBinders = mapAccumL tidyTyCoVarBinder --------------- tidyFreeTyCoVars :: TidyEnv -> [TyCoVar] -> TidyEnv @@ -2673,7 +3204,7 @@ tidyFreeTyCoVars :: TidyEnv -> [TyCoVar] -> TidyEnv 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 @@ -2681,19 +3212,19 @@ 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 'tidyTyCoVarBndr' +-- 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 tidyTyCoVarBndr env' tyvar -- Treat it as a binder + in tidyVarBndr env' tyvar -- Treat it as a binder --------------- -tidyTyVarOcc :: TidyEnv -> TyVar -> TyVar -tidyTyVarOcc env@(_, subst) tv +tidyTyCoVarOcc :: TidyEnv -> TyCoVar -> TyCoVar +tidyTyCoVarOcc env@(_, subst) tv = case lookupVarEnv subst tv of - Nothing -> updateTyVarKind (tidyType env) tv + Nothing -> updateVarType (tidyType env) tv Just tv' -> tv' --------------- @@ -2703,7 +3234,7 @@ tidyTypes env tys = map (tidyType env) tys --------------- tidyType :: TidyEnv -> Type -> Type tidyType _ (LitTy n) = LitTy n -tidyType env (TyVarTy tv) = TyVarTy (tidyTyVarOcc env tv) +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) @@ -2711,7 +3242,7 @@ tidyType env (FunTy fun arg) = (FunTy $! (tidyType env fun)) $! (tidyType e tidyType env (ty@(ForAllTy{})) = mkForAllTys' (zip tvs' vis) $! tidyType env' body_ty where (tvs, vis, body_ty) = splitForAllTys' ty - (env', tvs') = tidyTyCoVarBndrs env tvs + (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) @@ -2719,16 +3250,16 @@ 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' :: [(TyVar, ArgFlag)] -> Type -> Type +mkForAllTys' :: [(TyCoVar, ArgFlag)] -> Type -> Type mkForAllTys' tvvs ty = foldr strictMkForAllTy ty tvvs where - strictMkForAllTy (tv,vis) ty = (ForAllTy $! ((TvBndr $! tv) $! vis)) $! ty + strictMkForAllTy (tv,vis) ty = (ForAllTy $! ((Bndr $! tv) $! vis)) $! ty -splitForAllTys' :: Type -> ([TyVar], [ArgFlag], Type) +splitForAllTys' :: Type -> ([TyCoVar], [ArgFlag], Type) splitForAllTys' ty = go ty [] [] where - go (ForAllTy (TvBndr tv vis) ty) tvs viss = go ty (tv:tvs) (vis:viss) - go ty tvs viss = (reverse tvs, reverse viss, ty) + go (ForAllTy (Bndr tv vis) ty) tvs viss = go ty (tv:tvs) (vis:viss) + go ty tvs viss = (reverse tvs, reverse viss, ty) --------------- @@ -2767,28 +3298,32 @@ tidyCo :: TidyEnv -> Coercion -> Coercion tidyCo env@(_, subst) co = go co where - go (Refl r ty) = Refl r (tidyType env ty) + 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) = tidyTyCoVarBndr env tv + 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 d co) = NthCo d $! go co + 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 (CoherenceCo co1 co2) = (CoherenceCo $! go co1) $! go co2 go (KindCo co) = KindCo $! go co go (SubCo co) = SubCo $! go co go (AxiomRuleCo ax cos) = let cos1 = tidyCos env cos @@ -2798,7 +3333,6 @@ tidyCo env@(_, subst) co go_prov (PhantomProv co) = PhantomProv (go co) go_prov (ProofIrrelProv co) = ProofIrrelProv (go co) go_prov p@(PluginProv _) = p - go_prov p@(HoleProv _) = p tidyCos :: TidyEnv -> [Coercion] -> [Coercion] tidyCos env = map (tidyCo env) @@ -2828,26 +3362,28 @@ typeSize (LitTy {}) = 1 typeSize (TyVarTy {}) = 1 typeSize (AppTy t1 t2) = typeSize t1 + typeSize t2 typeSize (FunTy t1 t2) = typeSize t1 + typeSize t2 -typeSize (ForAllTy (TvBndr tv _) t) = typeSize (tyVarKind tv) + typeSize t +typeSize (ForAllTy (Bndr tv _) t) = typeSize (varType tv) + typeSize t typeSize (TyConApp _ ts) = 1 + sum (map typeSize ts) typeSize (CastTy ty co) = typeSize ty + coercionSize co typeSize (CoercionTy co) = coercionSize co coercionSize :: Coercion -> Int -coercionSize (Refl _ ty) = typeSize ty +coercionSize (Refl ty) = typeSize ty +coercionSize (GRefl _ ty MRefl) = typeSize ty +coercionSize (GRefl _ ty (MCo co)) = 1 + typeSize ty + coercionSize co coercionSize (TyConAppCo _ _ args) = 1 + sum (map coercionSize args) coercionSize (AppCo co arg) = coercionSize co + coercionSize arg coercionSize (ForAllCo _ h co) = 1 + coercionSize co + coercionSize h coercionSize (FunCo _ co1 co2) = 1 + coercionSize co1 + coercionSize co2 coercionSize (CoVarCo _) = 1 +coercionSize (HoleCo _) = 1 coercionSize (AxiomInstCo _ _ args) = 1 + sum (map coercionSize args) coercionSize (UnivCo p _ t1 t2) = 1 + provSize p + typeSize t1 + typeSize t2 coercionSize (SymCo co) = 1 + coercionSize co coercionSize (TransCo co1 co2) = 1 + coercionSize co1 + coercionSize co2 -coercionSize (NthCo _ co) = 1 + coercionSize co +coercionSize (NthCo _ _ co) = 1 + coercionSize co coercionSize (LRCo _ co) = 1 + coercionSize co coercionSize (InstCo co arg) = 1 + coercionSize co + coercionSize arg -coercionSize (CoherenceCo c1 c2) = 1 + coercionSize c1 + coercionSize c2 coercionSize (KindCo co) = 1 + coercionSize co coercionSize (SubCo co) = 1 + coercionSize co coercionSize (AxiomRuleCo _ cs) = 1 + sum (map coercionSize cs) @@ -2857,4 +3393,3 @@ provSize UnsafeCoerceProv = 1 provSize (PhantomProv co) = 1 + coercionSize co provSize (ProofIrrelProv co) = 1 + coercionSize co provSize (PluginProv _) = 1 -provSize (HoleProv h) = pprPanic "provSize hits a hole" (ppr h) |