diff options
Diffstat (limited to 'compiler/GHC/Tc/Utils')
| -rw-r--r-- | compiler/GHC/Tc/Utils/Concrete.hs | 497 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Utils/Instantiate.hs | 4 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Utils/Monad.hs | 14 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Utils/TcMType.hs | 247 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Utils/TcType.hs | 123 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Utils/Unify.hs | 300 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Utils/Unify.hs-boot | 6 |
7 files changed, 826 insertions, 365 deletions
diff --git a/compiler/GHC/Tc/Utils/Concrete.hs b/compiler/GHC/Tc/Utils/Concrete.hs index 22ba6b45e3..da9efb7ef3 100644 --- a/compiler/GHC/Tc/Utils/Concrete.hs +++ b/compiler/GHC/Tc/Utils/Concrete.hs @@ -7,32 +7,45 @@ module GHC.Tc.Utils.Concrete ( -- * Ensuring that a type has a fixed runtime representation hasFixedRuntimeRep - , hasFixedRuntimeRep_MustBeRefl + , hasFixedRuntimeRep_syntactic + + -- * Making a type concrete + , makeTypeConcrete ) where import GHC.Prelude -import GHC.Builtin.Types ( unliftedTypeKindTyCon, liftedTypeKindTyCon ) - -import GHC.Core.Coercion ( Role(..) ) -import GHC.Core.Predicate ( mkIsReflPrimPred ) -import GHC.Core.TyCo.Rep ( Type(TyConApp), mkTyVarTy ) -import GHC.Core.Type ( isConcrete, typeKind ) - -import GHC.Tc.Types ( TcM, ThStage(Brack), PendingStuff(TcPending) ) -import GHC.Tc.Types.Constraint ( mkNonCanonical ) -import GHC.Tc.Types.Evidence ( TcCoercion ) -import GHC.Tc.Types.Origin ( CtOrigin(..), FRROrigin(..) ) -import GHC.Tc.Utils.Monad ( emitSimple, getStage ) -import GHC.Tc.Utils.TcType ( TcType, TcKind, TcTyVar, MetaInfo(ConcreteTv) ) -import GHC.Tc.Utils.TcMType ( newAnonMetaTyVar, newWanted, emitWantedEq ) +import GHC.Builtin.Types ( liftedTypeKindTyCon, unliftedTypeKindTyCon ) + +import GHC.Core.Coercion ( coToMCo, mkCastTyMCo ) +import GHC.Core.TyCo.Rep ( Type(..), MCoercion(..) ) +import GHC.Core.TyCon ( isConcreteTyCon ) +import GHC.Core.Type ( isConcrete, typeKind, tyVarKind, tcView + , mkTyVarTy, mkTyConApp, mkFunTy, mkAppTy ) + +import GHC.Tc.Types ( TcM, ThStage(..), PendingStuff(..) ) +import GHC.Tc.Types.Constraint ( NotConcreteError(..), NotConcreteReason(..) ) +import GHC.Tc.Types.Evidence ( Role(..), TcCoercionN, TcMCoercionN + , mkTcGReflRightMCo, mkTcNomReflCo ) +import GHC.Tc.Types.Origin ( CtOrigin(..), FixedRuntimeRepContext, FixedRuntimeRepOrigin(..) ) +import GHC.Tc.Utils.Monad ( emitNotConcreteError, setTcLevel, getCtLocM, getStage, traceTc ) +import GHC.Tc.Utils.TcType ( TcType, TcKind, TcTypeFRR + , MetaInfo(..), ConcreteTvOrigin(..) + , isMetaTyVar, metaTyVarInfo, tcTyVarLevel ) +import GHC.Tc.Utils.TcMType ( newConcreteTyVar, isFilledMetaTyVar_maybe, writeMetaTyVar + , emitWantedEq ) import GHC.Types.Basic ( TypeOrKind(..) ) - import GHC.Utils.Misc ( HasDebugCallStack ) import GHC.Utils.Outputable -import GHC.Utils.Panic ( assertPpr ) + +import Control.Monad ( void ) +import Data.Functor ( ($>) ) +import Data.List.NonEmpty ( NonEmpty((:|)) ) + +import Control.Monad.Trans.Class ( lift ) +import Control.Monad.Trans.Writer.CPS ( WriterT, runWriterT, tell ) {- Note [Concrete overview] ~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -109,8 +122,8 @@ as a central point of reference for this topic. Note [Reporting representation-polymorphism errors] in GHC.Tc.Types.Origin When we emit a constraint to enforce a fixed representation, we also provide - a 'FRROrigin' which gives context about the check being done. This origin gets - reported to the user if we end up with such an an unsolved Wanted constraint. + a 'FixedRuntimeRepOrigin' which gives context about the check being done. + This origin gets reported to the user if we end up with such an an unsolved Wanted constraint. Note [Representation polymorphism checking] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -166,7 +179,7 @@ Definition: a type is /concrete/ iff it is: - a concrete type constructor (as defined below), or - a concrete type variable (see Note [ConcreteTv] below), or - an application of a concrete type to another concrete type - See GHC.Core.Type.isConcrete +GHC.Core.Type.isConcrete checks whether a type meets this definition. Definition: a /concrete type constructor/ is defined by - a promoted data constructor @@ -175,7 +188,7 @@ Definition: a /concrete type constructor/ is defined by - an abstract type as defined in a Backpack signature file (see Note [Synonyms implement abstract data] in GHC.Tc.Module) In particular, type and data families are not concrete. - See GHC.Core.TyCon.isConcreteTyCon. +GHC.Core.TyCon.isConcreteTyCon checks whether a TyCon meets this definition. Examples of concrete types: Lifted, BoxedRep Lifted, TYPE (BoxedRep Lifted) are all concrete @@ -194,9 +207,6 @@ concrete metavariable is itself concrete (see Note [ConcreteTv]): Concrete Kinds Property (CKP) The kind of a concrete type is concrete. -The CCP and the CKP taken together mean that we never have to inspect -in kinds to check concreteness. - Note [ConcreteTv] ~~~~~~~~~~~~~~~~~ A concrete metavariable is a metavariable whose 'MetaInfo' is 'ConcreteTv'. @@ -224,8 +234,9 @@ To check (ty :: ki) has a fixed runtime representation, we proceed as follows: ki ~# concrete_tv The origin for such an equality constraint uses - `GHC.Tc.Types.Origin.FRROrigin`, so that we can report the appropriate - representation-polymorphism error if any such constraint goes unsolved. + `GHC.Tc.Types.Origin.FixedRuntimeRepOrigin`, so that we can report the + appropriate representation-polymorphism error if any such constraint + goes unsolved. To solve `ki ~# concrete_ki`, we must unify `concrete_tv := concrete_ki`, where `concrete_ki` is some concrete type. We can then compute `kindPrimRep` @@ -238,19 +249,16 @@ has a fixed runtime representation. The Concrete mechanism is being implemented in two separate phases. -In PHASE 1 (currently implemented), we enforce that we only solve the emitted -constraints `co :: ki ~# concrete_tv` with `Refl`. This forbids any program +In PHASE 1, we enforce that we only solve the emitted constraints +`co :: ki ~# concrete_tv` with `Refl`. This forbids any program which requires type family evaluation in order to determine that a 'RuntimeRep' -is fixed. We do this using the `IsRefl#` special predicate (see Note [IsRefl#]); -we only solve `IsRefl# a b` if `a` and `b` are equal (after zonking, but not rewriting). -This means that it is safe to not use the coercion `co` anywhere in the program. -PHASE 1 corresponds to calls to `hasFixedRuntimeRep_MustBeRefl` in the code: on top -of emitting a constraint of the form `ki ~# concrete_tv`, we also emit -`IsRefl# ki concrete_tv` to ensure we only solve the equality constraint using -reflexivity. +is fixed. +To achieve this, instead of creating a new concrete metavariable, we directly +ensure that 'ki' is concrete, using 'makeTypeConcrete'. If it fails, then +we report an error (even though rewriting might have allowed us to proceed). In PHASE 2, we lift this restriction. This means we replace a call to -`hasFixedRuntimeRep_MustBeRefl` with a call to `hasFixedRuntimeRep`, and insert the +`hasFixedRuntimeRep_syntactic` with a call to `hasFixedRuntimeRep`, and insert the obtained coercion in the typechecked result. To illustrate what this entails, recall that the code generator needs to be able to compute 'PrimRep's, so that it can put function arguments in the correct registers, etc. @@ -274,17 +282,37 @@ this would be: As `( a |> kco ) :: TYPE Int#`, the code generator knows to use a machine-sized integer register for `x`, and all is good again. +Because we can convert calls from hasFixedRuntimeRep_syntactic to +hasFixedRuntimeRep one at a time, we can migrate from PHASE 1 to PHASE 2 +incrementally. + Example test cases that require PHASE 2: T13105, T17021, T20363b. Note [Fixed RuntimeRep] ~~~~~~~~~~~~~~~~~~~~~~~ -Definition: - a type `ty :: ki` has a /fixed RuntimeRep/ - <=> - there exists a concrete type `concrete_ty` (in the sense of Note [Concrete types]) - such that we can solve `ki ~# concrete_ty`. +Definitions: -This definition is crafted to be useful to satisfy the invariants of + FRR. + + The type `ty :: ki` has a /syntactically fixed RuntimeRep/ + (we also say that `ty` is an `FRRType`) + <=> + the kind `ki` is concrete (in the sense of Note [Concrete types]) + <=> + `typePrimRep ty` (= `kindPrimRep ki`) does not crash + (assuming that typechecking succeeded, so that all metavariables + in `ty` have been filled) + + Fixed RuntimeRep. + + The type `ty :: ki` has a /fixed RuntimeRep/ + <=> + there exists an FRR type `ty'` with `ty ~# ty'` + <=> + there exists a concrete type `concrete_ki` such that + `ki ~ concrete_ki` + +These definitions are crafted to be useful to satisfy the invariants of Core; see Note [Representation polymorphism invariants] in GHC.Core. Notice that "fixed RuntimeRep" means (for now anyway) that @@ -307,6 +335,16 @@ To do so, we compute the kind 'ki' of 'ty', create a new concrete metavariable `concrete_tv` of kind `ki`, and emit a constraint `ki ~# concrete_tv`, which will only be solved if we can prove that 'ty' indeed has a fixed RuntimeRep. +If we can solve the equality constraint, i.e. produce a coercion +`kco :: ki ~# concrete_tv`, then 'hasFixedRuntimeRep' returns the coercion + + co = GRefl ty kco :: ty ~# ty |> kco + +The RHS of the coercion `co` is `ty |> kco`. The kind of this type is +concrete (by construction), which means that `ty |> kco` is an FRRType +in the sense of Note [Fixed RuntimeRep], so that we can directely compute +its runtime representation using `typePrimRep`. + [Wrinkle: Typed Template Haskell] We don't perform any checks when type-checking a typed Template Haskell quote: we want to allow representation polymorphic quotes, as long as they are @@ -338,132 +376,309 @@ which will only be solved if we can prove that 'ty' indeed has a fixed RuntimeRe this shouldn't cause any problems in practice. See ticket #18170. Test case: rep-poly/T18170a. - -Note [IsRefl#] -~~~~~~~~~~~~~~ -`IsRefl# :: forall k. k -> k -> TYPE (TupleRep '[])` is a constraint with no -evidence. `IsRefl# a b' can be solved precisely when `a` and `b` are equal (up to zonking, -but __without__ any rewriting). - -That is, if we have a type family `F` with `F Int` reducing to `Int`, we __cannot__ solve -`IsRefl# (F Int) Int`. - -What is the point of such a constraint? As outlined in Note [The Concrete mechanism], -to check `ty :: ki` has a fixed RuntimeRep we create a concrete metavariable `concrete_tv` -and emit a Wanted equality constraint - - {co_hole} :: ki ~# concrete_tv - -Then, when we fill in the coercion hole with a coercion `co`, we must make use of it -(as that Note explains). If we don't, then we can only safely discard it if it is -reflexive. Therefore, whenever we perform a representation polymorphism check but also -discard the resulting coercion, we also emit a special constraint `IsRefl# ki concrete_tv`. -See 'hasFixedRuntimeRep_MustBeRefl', which calls 'hasFixedRuntimeRep', and thenemits -an 'IsRefl#' constraint to ensure that discarding the coercion is safe. -} --- | Like 'hasFixedRuntimeRep', but we insist that the obtained coercion must be 'Refl'. +-- | Given a type @ty :: ki@, this function ensures that @ty@ +-- has a __fixed__ 'RuntimeRep', by emitting a new equality constraint +-- @ki ~ concrete_tv@ for a concrete metavariable @concrete_tv@. +-- +-- Returns a coercion @co :: ty ~# concrete_ty@ as evidence. +-- If @ty@ obviously has a fixed 'RuntimeRep', e.g @ki = IntRep@, +-- then this function immediately returns 'MRefl', +-- without emitting any constraints. +hasFixedRuntimeRep :: HasDebugCallStack + => FixedRuntimeRepContext + -- ^ Context to be reported to the user + -- if the type ends up not having a fixed + -- 'RuntimeRep'. + -> TcType + -- ^ The type to check (we only look at its kind). + -> TcM (TcCoercionN, TcTypeFRR) + -- ^ @(co, ty')@ where @ty' :: ki'@, + -- @ki@ is concrete, and @co :: ty ~# ty'@. + -- That is, @ty'@ has a syntactically fixed RuntimeRep + -- in the sense of Note [Fixed RuntimeRep]. +hasFixedRuntimeRep frr_ctxt ty = checkFRR_with unifyConcrete frr_ctxt ty + +-- | Like 'hasFixedRuntimeRep', but we perform an eager syntactic check. +-- +-- Throws an error in the 'TcM' monad if the check fails. -- -- This is useful if we are not actually going to use the coercion returned -- from 'hasFixedRuntimeRep'; it would generally be unsound to allow a non-reflexive --- coercion but not actually make use of it in a cast. See Note [IsRefl#]. +-- coercion but not actually make use of it in a cast. -- -- The goal is to eliminate all uses of this function and replace them with --- 'hasFixedRuntimeRep', making use of the returned coercion. -hasFixedRuntimeRep_MustBeRefl :: FRROrigin -> TcType -> TcM () -hasFixedRuntimeRep_MustBeRefl frr_orig ty - = do { -- STEP 1: check that the type has a fixed 'RuntimeRep'. - mb_co <- hasFixedRuntimeRep frr_orig ty - -- STEP 2: ensure that we only solve using a reflexive coercion. - ; case mb_co of - -- If the coercion is immediately reflexive: we're OK. - { Nothing -> return () - -- Otherwise: emit an @IsRefl#@ constraint. - -- This means we are free to discard the coercion. - ; Just (ki, _co, concrete_kv) -> - do { isRefl_ctev <- newWanted (FixedRuntimeRepOrigin ty frr_orig) - (Just KindLevel) $ - mkIsReflPrimPred ki (mkTyVarTy concrete_kv) - ; emitSimple $ mkNonCanonical isRefl_ctev } } } - --- | Given a type @ty :: ki@, this function ensures that @ty@ --- has a __fixed__ 'RuntimeRep', by emitting a new equality constraint --- @ki ~ concrete_tv@ for a concrete metavariable @concrete_tv@. +-- 'hasFixedRuntimeRep', making use of the returned coercion. This is what +-- is meant by going from PHASE 1 to PHASE 2, in Note [The Concrete mechanism]. +hasFixedRuntimeRep_syntactic :: HasDebugCallStack + => FixedRuntimeRepContext + -- ^ Context to be reported to the user + -- if the type does not have a syntactically + -- fixed 'RuntimeRep'. + -> TcType + -- ^ The type to check (we only look at its kind). + -> TcM () +hasFixedRuntimeRep_syntactic frr_ctxt ty + = void $ checkFRR_with ensure_conc frr_ctxt ty + where + ensure_conc :: FixedRuntimeRepOrigin -> TcKind -> TcM TcMCoercionN + ensure_conc frr_orig ki = ensureConcrete frr_orig ki $> MRefl + +-- | Internal function to check whether the given type has a fixed 'RuntimeRep'. -- --- Returns a coercion @co :: ki ~# concrete_tv@ as evidence. --- If @ty@ obviously has a fixed 'RuntimeRep', e.g @ki = IntRep@, --- then this function immediately returns 'Nothing' --- instead of emitting a new constraint. -hasFixedRuntimeRep :: FRROrigin -- ^ Context to be reported to the user - -- if the type ends up not having a fixed - -- 'RuntimeRep' (unsolved Wanted constraint). - -> TcType -- ^ The type to check (we only look at its kind). - -> TcM (Maybe (TcType, TcCoercion, TcTyVar) ) - -- ^ @Just ( ki, co, concrete_tv )@ - -- where @co :: ki ~# concrete_ty@ is evidence that - -- the type @ty :: ki@ has a fixed 'RuntimeRep', - -- or 'Nothing' if 'ki' responds 'True' to 'isConcrete', - -- (i.e. we can take @co = Refl@). -hasFixedRuntimeRep frr_orig ty +-- Use 'hasFixedRuntimeRep' to allow rewriting, or 'hasFixedRuntimeRep_syntactic' +-- to perform a syntactic check. +checkFRR_with :: HasDebugCallStack + => (FixedRuntimeRepOrigin -> TcKind -> TcM TcMCoercionN) + -- ^ The check to perform on the kind. + -> FixedRuntimeRepContext + -- ^ The context which required a fixed 'RuntimeRep', + -- e.g. an application, a lambda abstraction, ... + -> TcType + -- ^ The type @ty@ to check (the check itself only looks at its kind). + -> TcM (TcCoercionN, TcTypeFRR) + -- ^ Returns @(co, frr_ty)@ with @co :: ty ~# frr_ty@ + -- and @frr_@ty has a fixed 'RuntimeRep'. +checkFRR_with check_kind frr_ctxt ty = do { th_stage <- getStage ; if -- Shortcut: check for 'Type' and 'UnliftedType' type synonyms. | TyConApp tc [] <- ki , tc == liftedTypeKindTyCon || tc == unliftedTypeKindTyCon - -> return Nothing + -> return refl -- See [Wrinkle: Typed Template Haskell] in Note [hasFixedRuntimeRep]. | Brack _ (TcPending {}) <- th_stage - -> return Nothing + -> return refl + -- Otherwise: ensure that the kind 'ki' of 'ty' is concrete. | otherwise - -- Ensure that the kind 'ki' of 'ty' is concrete. - -> emitNewConcreteWantedEq_maybe orig ki - -- NB: the kind of 'ki' is 'Data.Kind.Type', which is concrete. - -- This means that the invariant required to call - -- 'newConcreteTyVar' is satisfied. - } + -> do { kco <- check_kind frr_orig ki + ; return ( mkTcGReflRightMCo Nominal ty kco + , mkCastTyMCo ty kco ) } } + where + refl :: (TcCoercionN, TcType) + refl = (mkTcNomReflCo ty, ty) ki :: TcKind ki = typeKind ty - orig :: CtOrigin - orig = FixedRuntimeRepOrigin ty frr_orig + frr_orig :: FixedRuntimeRepOrigin + frr_orig = FixedRuntimeRepOrigin { frr_type = ty, frr_context = frr_ctxt } --- | Create a new metavariable, of the given kind, which can only be unified --- with a concrete type. +-- | Ensure that the given type @ty@ can unify with a concrete type, +-- in the sense of Note [Concrete types]. -- --- Invariant: the kind must be concrete, as per Note [ConcreteTv]. --- This is checked with an assertion. -newConcreteTyVar :: HasDebugCallStack => TcKind -> TcM TcTyVar -newConcreteTyVar kind = - assertPpr (isConcrete kind) - (text "newConcreteTyVar: non-concrete kind" <+> ppr kind) - $ newAnonMetaTyVar ConcreteTv kind - --- | Create a new concrete metavariable @concrete_tv@ and emit a new non-canonical Wanted --- equality constraint @ty ~# concrete_tv@ with the given 'CtOrigin'. +-- Returns a coercion @co :: ty ~# conc_ty@, where @conc_ty@ is +-- concrete. -- --- Short-cut: if the type responds 'True' to 'isConcrete', then --- we already know it is concrete, so don't emit any new constraints, --- and return 'Nothing'. +-- If the type is already syntactically concrete, this +-- immediately returns a reflexive coercion. Otherwise, +-- it creates a new concrete metavariable @concrete_tv@ +-- and emits an equality constraint @ty ~# concrete_tv@, +-- to be handled by the constraint solver. -- -- Invariant: the kind of the supplied type must be concrete. -- --- We also assume the provided type is already at the kind-level. ---(This only matters for error messages.) -emitNewConcreteWantedEq_maybe :: CtOrigin -> TcType -> TcM (Maybe (TcType, TcCoercion, TcTyVar)) -emitNewConcreteWantedEq_maybe orig ty - -- The input type is already concrete: no need to do anything. - -- Return 'Nothing', indicating that reflexivity is valid evidence. - | isConcrete ty - = return Nothing - -- Otherwise: create a new concrete metavariable and emit a new Wanted equality constraint. - | otherwise - = do { concrete_tv <- newConcreteTyVar ki - ; co <- emitWantedEq orig KindLevel Nominal ty (mkTyVarTy concrete_tv) - -- ^^^^^^^^^ we assume 'ty' is at the kind level. - -- (For representation polymorphism checks, we are always checking a kind.) - ; return $ Just (ty, co, concrete_tv) } +-- We assume the provided type is already at the kind-level +-- (this only matters for error messages). +unifyConcrete :: HasDebugCallStack + => FixedRuntimeRepOrigin -> TcType -> TcM TcMCoercionN +unifyConcrete frr_orig ty + = do { (ty, errs) <- makeTypeConcrete (ConcreteFRR frr_orig) ty + ; case errs of + -- We were able to make the type fully concrete. + { [] -> return MRefl + -- The type could not be made concrete; perhaps it contains + -- a skolem type variable, a type family application, ... + -- + -- Create a new ConcreteTv metavariable @concrete_tv@ + -- and unify @ty ~# concrete_tv@. + ; _ -> + do { conc_tv <- newConcreteTyVar (ConcreteFRR frr_orig) ki + -- NB: newConcreteTyVar asserts that 'ki' is concrete. + ; coToMCo <$> emitWantedEq orig KindLevel Nominal ty (mkTyVarTy conc_tv) } } } where ki :: TcKind ki = typeKind ty + orig :: CtOrigin + orig = FRROrigin frr_orig + +-- | Ensure that the given type is concrete. +-- +-- This is an eager syntactic check, and never defers +-- any work to the constraint solver. +-- +-- Invariant: the kind of the supplied type must be concrete. +-- Invariant: the output type is equal to the input type, +-- up to zonking. +-- +-- We assume the provided type is already at the kind-level +-- (this only matters for error messages). +ensureConcrete :: HasDebugCallStack + => FixedRuntimeRepOrigin + -> TcType + -> TcM TcType +ensureConcrete frr_orig ty + = do { (ty', errs) <- makeTypeConcrete conc_orig ty + ; case errs of + { err:errs -> + do { traceTc "ensureConcrete } failure" $ + vcat [ text "ty:" <+> ppr ty + , text "ty':" <+> ppr ty' ] + ; loc <- getCtLocM (FRROrigin frr_orig) (Just KindLevel) + ; emitNotConcreteError $ + NCE_FRR + { nce_loc = loc + , nce_frr_origin = frr_orig + , nce_reasons = err :| errs } + } + ; [] -> + traceTc "ensureConcrete } success" $ + vcat [ text "ty: " <+> ppr ty + , text "ty':" <+> ppr ty' ] } + ; return ty' } + where + conc_orig :: ConcreteTvOrigin + conc_orig = ConcreteFRR frr_orig + +{-*********************************************************************** +%* * + Making a type concrete +%* * +%************************************************************************ + +Note [Unifying concrete metavariables] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Unifying concrete metavariables (as defined in Note [ConcreteTv]) is not +an all-or-nothing affair as it is for other sorts of metavariables. + +Consider the following unification problem in which all metavariables +are unfilled (and ignoring any TcLevel considerations): + + alpha[conc] ~# TYPE (TupleRep '[ beta[conc], IntRep, gamma[tau] ]) + +We can't immediately unify `alpha` with the RHS, because the RHS is not +a concrete type (in the sense of Note [Concrete types]). Instead, we +proceed as follows: + + - create a fresh concrete metavariable variable `gamma'[conc]`, + - write gamma[tau] := gamma'[conc], + - write alpha[conc] := TYPE (TupleRep '[ beta[conc], IntRep, gamma'[conc] ]). + +Thus, in general, to unify `alpha[conc] ~# rhs`, we first try to turn +`rhs` into a concrete type (see the 'makeTypeConcrete' function). +If this succeeds, resulting in a concrete type `rhs'`, we simply fill +`alpha[conc] := rhs'`. If it fails, then syntactic unification fails. + +Example 1: + + alpha[conc] ~# TYPE (TupleRep '[ beta[conc], IntRep, gamma[tau] ]) + + We proceed by filling metavariables: + + gamma[tau] := gamma[conc] + alpha[conc] := TYPE (TupleRep '[ beta[conc], IntRep, gamma[conc] ]) + + This successfully unifies alpha. + +Example 2: + + For a type family `F :: Type -> Type`: + + delta[conc] ~# TYPE (SumRep '[ zeta[tau], a[sk], F omega[tau] ]) + + We write zeta[tau] := zeta[conc], and then fail, providing the following + two reasons: + + - `a[sk]` is not a concrete type variable, so the overall type + cannot be concrete + - `F` is not a concrete type constructor, in the sense of + Note [Concrete types]. So we keep it as is; in particular, + we /should not/ try to make its argument `omega[tau]` into + a ConcreteTv. + + Note that making zeta concrete allows us to propagate information. + For example, after more typechecking, we might try to unify + `zeta ~# rr[sk]`. If we made zeta a ConcreteTv, we will report + this unsolved equality using the 'ConcreteTvOrigin' stored in zeta[conc]. + This allows us to report ALL the problems in a representation-polymorphism + check (instead of only a non-empty subset). +-} + +-- | Try to turn the provided type into a concrete type, by ensuring +-- unfilled metavariables are appropriately marked as concrete. +-- +-- Returns a zonked type which is "as concrete as possible", and +-- a list of problems encountered when trying to make it concrete. +-- +-- INVARIANT: the returned type is equal to the input type, up to zonking. +-- INVARIANT: if this function returns an empty list of 'NotConcreteReasons', +-- then the returned type is concrete, in the sense of Note [Concrete types]. +makeTypeConcrete :: ConcreteTvOrigin -> TcType -> TcM (TcType, [NotConcreteReason]) +-- TODO: it could be worthwhile to return enough information to continue solving. +-- Consider unifying `alpha[conc] ~# TupleRep '[ beta[tau], F Int ]` for +-- a type family 'F'. +-- This function will concretise `beta[tau] := beta[conc]` and return +-- that `TupleRep '[ beta[conc], F Int ]` is not concrete because of the +-- type family application `F Int`. But we could decompose by setting +-- alpha := TupleRep '[ beta, gamma[conc] ] and emitting `[W] gamma[conc] ~ F Int`. +-- +-- This would be useful in startSolvingByUnification. +makeTypeConcrete conc_orig ty = + do { res@(ty', _) <- runWriterT $ go ty + ; traceTc "makeTypeConcrete" $ + vcat [ text "ty:" <+> ppr ty + , text "ty':" <+> ppr ty' ] + ; return res } + where + go :: TcType -> WriterT [NotConcreteReason] TcM TcType + go ty + | Just ty <- tcView ty + = go ty + | isConcrete ty + = pure ty + go ty@(TyVarTy tv) -- not a ConcreteTv (already handled above) + = do { mb_filled <- lift $ isFilledMetaTyVar_maybe tv + ; case mb_filled of + { Just ty -> go ty + ; Nothing + | isMetaTyVar tv + , TauTv <- metaTyVarInfo tv + -> -- Change the MetaInfo to ConcreteTv, but retain the TcLevel + do { kind <- go (tyVarKind tv) + ; lift $ + do { conc_tv <- setTcLevel (tcTyVarLevel tv) $ + newConcreteTyVar conc_orig kind + ; let conc_ty = mkTyVarTy conc_tv + ; writeMetaTyVar tv conc_ty + ; return conc_ty } } + | otherwise + -- Don't attempt to make other type variables concrete + -- (e.g. SkolemTv, TyVarTv, CycleBreakerTv, RuntimeUnkTv). + -> bale_out ty (NonConcretisableTyVar tv) } } + go ty@(TyConApp tc tys) + | isConcreteTyCon tc + = mkTyConApp tc <$> mapM go tys + | otherwise + = bale_out ty (NonConcreteTyCon tc tys) + go (FunTy af w ty1 ty2) + = do { w <- go w + ; ty1 <- go ty1 + ; ty2 <- go ty2 + ; return $ mkFunTy af w ty1 ty2 } + go (AppTy ty1 ty2) + = do { ty1 <- go ty1 + ; ty2 <- go ty2 + ; return $ mkAppTy ty1 ty2 } + go ty@(LitTy {}) + = return ty + go ty@(CastTy cast_ty kco) + = bale_out ty (ContainsCast cast_ty kco) + go ty@(ForAllTy tcv body) + = bale_out ty (ContainsForall tcv body) + go ty@(CoercionTy co) + = bale_out ty (ContainsCoercionTy co) + + bale_out :: TcType -> NotConcreteReason -> WriterT [NotConcreteReason] TcM TcType + bale_out ty reason = do { tell [reason]; return ty } diff --git a/compiler/GHC/Tc/Utils/Instantiate.hs b/compiler/GHC/Tc/Utils/Instantiate.hs index 78c7ad4c12..4284b35d5e 100644 --- a/compiler/GHC/Tc/Utils/Instantiate.hs +++ b/compiler/GHC/Tc/Utils/Instantiate.hs @@ -70,7 +70,7 @@ import GHC.Tc.Types.Origin import GHC.Tc.Utils.Env import GHC.Tc.Types.Evidence import GHC.Tc.Instance.FunDeps -import GHC.Tc.Utils.Concrete +import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep_syntactic ) import GHC.Tc.Utils.TcMType import GHC.Tc.Utils.TcType import GHC.Tc.Errors.Types @@ -825,7 +825,7 @@ hasFixedRuntimeRepRes std_nm user_expr ty = mapM_ do_check mb_arity do_check :: Arity -> TcM () do_check arity = let res_ty = nTimes arity (snd . splitPiTy) ty - in hasFixedRuntimeRep_MustBeRefl (FRRArrow $ ArrowFun user_expr) res_ty + in hasFixedRuntimeRep_syntactic (FRRArrow $ ArrowFun user_expr) res_ty mb_arity :: Maybe Arity mb_arity -- arity of the arrow operation, counting type-level arguments | std_nm == arrAName -- result used as an argument in, e.g., do_premap diff --git a/compiler/GHC/Tc/Utils/Monad.hs b/compiler/GHC/Tc/Utils/Monad.hs index dada2c8041..571e02c7cf 100644 --- a/compiler/GHC/Tc/Utils/Monad.hs +++ b/compiler/GHC/Tc/Utils/Monad.hs @@ -106,7 +106,7 @@ module GHC.Tc.Utils.Monad( getConstraintVar, setConstraintVar, emitConstraints, emitStaticConstraints, emitSimple, emitSimples, emitImplication, emitImplications, emitInsoluble, - emitHole, emitHoles, + emitDelayedErrors, emitHole, emitHoles, emitNotConcreteError, discardConstraints, captureConstraints, tryCaptureConstraints, pushLevelAndCaptureConstraints, pushTcLevelM_, pushTcLevelM, @@ -1816,6 +1816,12 @@ emitInsoluble ct ; lie_var <- getConstraintVar ; updTcRef lie_var (`addInsols` unitBag ct) } +emitDelayedErrors :: Bag DelayedError -> TcM () +emitDelayedErrors errs + = do { traceTc "emitDelayedErrors" (ppr errs) + ; lie_var <- getConstraintVar + ; updTcRef lie_var (`addDelayedErrors` errs)} + emitHole :: Hole -> TcM () emitHole hole = do { traceTc "emitHole" (ppr hole) @@ -1828,6 +1834,12 @@ emitHoles holes ; lie_var <- getConstraintVar ; updTcRef lie_var (`addHoles` holes) } +emitNotConcreteError :: NotConcreteError -> TcM () +emitNotConcreteError err + = do { traceTc "emitNotConcreteError" (ppr err) + ; lie_var <- getConstraintVar + ; updTcRef lie_var (`addNotConcreteError` err) } + -- | Throw out any constraints emitted by the thing_inside discardConstraints :: TcM a -> TcM a discardConstraints thing_inside = fst <$> captureConstraints thing_inside diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs index 8c59e30d95..1206b95da7 100644 --- a/compiler/GHC/Tc/Utils/TcMType.hs +++ b/compiler/GHC/Tc/Utils/TcMType.hs @@ -25,7 +25,7 @@ module GHC.Tc.Utils.TcMType ( newOpenFlexiTyVar, newOpenFlexiTyVarTy, newOpenTypeKind, newOpenBoxedTypeKind, newMetaKindVar, newMetaKindVars, newMetaTyVarTyAtLevel, - newAnonMetaTyVar, cloneMetaTyVar, + newAnonMetaTyVar, newConcreteTyVar, cloneMetaTyVar, newCycleBreakerTyVar, newMultiplicityVar, @@ -60,16 +60,18 @@ module GHC.Tc.Utils.TcMType ( -------------------------------- -- Expected types ExpType(..), ExpSigmaType, ExpRhoType, - mkCheckExpType, newInferExpType, tcInfer, + mkCheckExpType, newInferExpType, newInferExpTypeFRR, + tcInfer, tcInferFRR, readExpType, readExpType_maybe, readScaledExpType, expTypeToType, scaledExpTypeToType, checkingExpType_maybe, checkingExpType, - inferResultToType, fillInferResult, promoteTcType, + inferResultToType, ensureMonoType, promoteTcType, -------------------------------- -- Zonking and tidying zonkTidyTcType, zonkTidyTcTypes, zonkTidyOrigin, zonkTidyOrigins, - tidyEvVar, tidyCt, tidyHole, + zonkTidyFRRInfos, + tidyEvVar, tidyCt, tidyHole, tidyDelayedError, zonkTcTyVar, zonkTcTyVars, zonkTcTyVarToTcTyVar, zonkTcTyVarsToTcTyVars, zonkInvisTVBinder, @@ -113,7 +115,6 @@ import GHC.Tc.Types.Origin import GHC.Tc.Utils.Monad -- TcType, amongst others import GHC.Tc.Types.Constraint import GHC.Tc.Types.Evidence -import {-# SOURCE #-} GHC.Tc.Utils.Unify( unifyType {- , unifyKind -} ) import GHC.Tc.Utils.TcType import GHC.Tc.Errors.Types import GHC.Tc.Errors.Ppr @@ -198,12 +199,8 @@ newEvVar ty = do { name <- newSysName (predTypeOccName ty) newWantedWithLoc :: CtLoc -> PredType -> TcM CtEvidence newWantedWithLoc loc pty = do dst <- case classifyPredType pty of - EqPred {} - -> HoleDest <$> newCoercionHole pty - SpecialPred s - -> case s of - IsReflPrimPred {} -> return NoDest - _ -> EvVarDest <$> newEvVar pty + EqPred {} -> HoleDest <$> newCoercionHole pty + _ -> EvVarDest <$> newEvVar pty return $ CtWanted { ctev_dest = dst , ctev_pred = pty , ctev_loc = loc @@ -332,9 +329,6 @@ predTypeOccName ty = case classifyPredType ty of EqPred {} -> mkVarOccFS (fsLit "co") IrredPred {} -> mkVarOccFS (fsLit "irred") ForAllPred {} -> mkVarOccFS (fsLit "df") - SpecialPred s -> - case s of - IsReflPrimPred {} -> mkVarOccFS (fsLit "rfl") -- | Create a new 'Implication' with as many sensible defaults for its fields -- as possible. Note that the 'ic_tclvl', 'ic_binds', and 'ic_info' fields do @@ -482,18 +476,42 @@ the ExpType with a tau-tv at the low TcLevel, hopefully to be worked out later by some means -- see fillInferResult, and Note [fillInferResult] This behaviour triggered in test gadt/gadt-escape1. + +Note [FixedRuntimeRep context in ExpType] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Sometimes, we want to be sure that we fill an ExpType with a type +that has a syntactically fixed RuntimeRep (in the sense of +Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete). + +Example: + + pattern S a = (a :: (T :: TYPE R)) + +We have to infer a type for `a` which has a syntactically fixed RuntimeRep. +When it comes time to filling in the inferred type, we do the appropriate +representation-polymorphism check, much like we do a level check +as explained in Note [TcLevel of ExpType]. + +See test case T21325. -} -- actual data definition is in GHC.Tc.Utils.TcType newInferExpType :: TcM ExpType -newInferExpType +newInferExpType = new_inferExpType Nothing + +newInferExpTypeFRR :: FixedRuntimeRepContext -> TcM ExpTypeFRR +newInferExpTypeFRR frr_orig = new_inferExpType (Just frr_orig) + +new_inferExpType :: Maybe FixedRuntimeRepContext -> TcM ExpType +new_inferExpType mb_frr_orig = do { u <- newUnique ; tclvl <- getTcLevel ; traceTc "newInferExpType" (ppr u <+> ppr tclvl) ; ref <- newMutVar Nothing ; return (Infer (IR { ir_uniq = u, ir_lvl = tclvl - , ir_ref = ref })) } + , ir_ref = ref + , ir_frr = mb_frr_orig })) } -- | Extract a type out of an ExpType, if one exists. But one should always -- exist. Unless you're quite sure you know what you're doing. @@ -563,119 +581,30 @@ order-independence we check for mono-type-ness even if it *is* filled in already. See also Note [TcLevel of ExpType] above, and -Note [fillInferResult]. +Note [fillInferResult] in GHC.Tc.Utils.Unify. -} -- | Infer a type using a fresh ExpType -- See also Note [ExpType] in "GHC.Tc.Utils.TcMType" +-- +-- Use 'tcInferFRR' if you require the type to have a fixed +-- runtime representation. tcInfer :: (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType) -tcInfer tc_check - = do { res_ty <- newInferExpType +tcInfer = tc_infer Nothing + +-- | Like 'tcInfer', except it ensures that the resulting type +-- has a syntactically fixed RuntimeRep as per Note [Fixed RuntimeRep] in +-- GHC.Tc.Utils.Concrete. +tcInferFRR :: FixedRuntimeRepContext -> (ExpSigmaTypeFRR -> TcM a) -> TcM (a, TcSigmaTypeFRR) +tcInferFRR frr_orig = tc_infer (Just frr_orig) + +tc_infer :: Maybe FixedRuntimeRepContext -> (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType) +tc_infer mb_frr tc_check + = do { res_ty <- new_inferExpType mb_frr ; result <- tc_check res_ty ; res_ty <- readExpType res_ty ; return (result, res_ty) } -fillInferResult :: TcType -> InferResult -> TcM TcCoercionN --- If co = fillInferResult t1 t2 --- => co :: t1 ~ t2 --- See Note [fillInferResult] -fillInferResult act_res_ty (IR { ir_uniq = u, ir_lvl = res_lvl - , ir_ref = ref }) - = do { mb_exp_res_ty <- readTcRef ref - ; case mb_exp_res_ty of - Just exp_res_ty - -> do { traceTc "Joining inferred ExpType" $ - ppr u <> colon <+> ppr act_res_ty <+> char '~' <+> ppr exp_res_ty - ; cur_lvl <- getTcLevel - ; unless (cur_lvl `sameDepthAs` res_lvl) $ - ensureMonoType act_res_ty - ; unifyType Nothing act_res_ty exp_res_ty } - Nothing - -> do { traceTc "Filling inferred ExpType" $ - ppr u <+> text ":=" <+> ppr act_res_ty - ; (prom_co, act_res_ty) <- promoteTcType res_lvl act_res_ty - ; writeTcRef ref (Just act_res_ty) - ; return prom_co } - } - - -{- Note [fillInferResult] -~~~~~~~~~~~~~~~~~~~~~~~~~ -When inferring, we use fillInferResult to "fill in" the hole in InferResult - data InferResult = IR { ir_uniq :: Unique - , ir_lvl :: TcLevel - , ir_ref :: IORef (Maybe TcType) } - -There are two things to worry about: - -1. What if it is under a GADT or existential pattern match? - - GADTs: a unification variable (and Infer's hole is similar) is untouchable - - Existentials: be careful about skolem-escape - -2. What if it is filled in more than once? E.g. multiple branches of a case - case e of - T1 -> e1 - T2 -> e2 - -Our typing rules are: - -* The RHS of a existential or GADT alternative must always be a - monotype, regardless of the number of alternatives. - -* Multiple non-existential/GADT branches can have (the same) - higher rank type (#18412). E.g. this is OK: - case e of - True -> hr - False -> hr - where hr:: (forall a. a->a) -> Int - c.f. Section 7.1 of "Practical type inference for arbitrary-rank types" - We use choice (2) in that Section. - (GHC 8.10 and earlier used choice (1).) - - But note that - case e of - True -> hr - False -> \x -> hr x - will fail, because we still /infer/ both branches, so the \x will get - a (monotype) unification variable, which will fail to unify with - (forall a. a->a) - -For (1) we can detect the GADT/existential situation by seeing that -the current TcLevel is greater than that stored in ir_lvl of the Infer -ExpType. We bump the level whenever we go past a GADT/existential match. - -Then, before filling the hole use promoteTcType to promote the type -to the outer ir_lvl. promoteTcType does this - - create a fresh unification variable alpha at level ir_lvl - - emits an equality alpha[ir_lvl] ~ ty - - fills the hole with alpha -That forces the type to be a monotype (since unification variables can -only unify with monotypes); and catches skolem-escapes because the -alpha is untouchable until the equality floats out. - -For (2), we simply look to see if the hole is filled already. - - if not, we promote (as above) and fill the hole - - if it is filled, we simply unify with the type that is - already there - -There is one wrinkle. Suppose we have - case e of - T1 -> e1 :: (forall a. a->a) -> Int - G2 -> e2 -where T1 is not GADT or existential, but G2 is a GADT. Then supppose the -T1 alternative fills the hole with (forall a. a->a) -> Int, which is fine. -But now the G2 alternative must not *just* unify with that else we'd risk -allowing through (e2 :: (forall a. a->a) -> Int). If we'd checked G2 first -we'd have filled the hole with a unification variable, which enforces a -monotype. - -So if we check G2 second, we still want to emit a constraint that restricts -the RHS to be a monotype. This is done by ensureMonoType, and it works -by simply generating a constraint (alpha ~ ty), where alpha is a fresh -unification variable. We discard the evidence. - --} - {- ********************************************************************* * * Promoting types @@ -864,7 +793,7 @@ metaInfoToTyVarName meta_info = TyVarTv -> fsLit "a" RuntimeUnkTv -> fsLit "r" CycleBreakerTv -> fsLit "b" - ConcreteTv -> fsLit "c" + ConcreteTv {} -> fsLit "c" newAnonMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar newAnonMetaTyVar mi = newNamedAnonMetaTyVar (metaInfoToTyVarName mi) mi @@ -909,6 +838,17 @@ cloneTyVarTyVar name kind ; traceTc "cloneTyVarTyVar" (ppr tyvar) ; return tyvar } +-- | Create a new metavariable, of the given kind, which can only be unified +-- with a concrete type. +-- +-- Invariant: the kind must be concrete, as per Note [ConcreteTv]. +-- This is checked with an assertion. +newConcreteTyVar :: HasDebugCallStack => ConcreteTvOrigin -> TcKind -> TcM TcTyVar +newConcreteTyVar reason kind = + assertPpr (isConcrete kind) + (text "newConcreteTyVar: non-concrete kind" <+> ppr kind) + $ newAnonMetaTyVar (ConcreteTv reason) kind + newPatSigTyVar :: Name -> Kind -> TcM TcTyVar newPatSigTyVar name kind = do { details <- newMetaDetails TauTv @@ -1863,9 +1803,7 @@ defaultTyVar :: DefaultingStrategy -> TcM Bool -- True <=> defaulted away altogether defaultTyVar def_strat tv | not (isMetaTyVar tv) - = return False - - | isTyVarTyVar tv + || isTyVarTyVar tv -- Do not default TyVarTvs. Doing so would violate the invariants -- on TyVarTvs; see Note [TyVarTv] in GHC.Tc.Utils.TcMType. -- #13343 is an example; #14555 is another @@ -1874,8 +1812,6 @@ defaultTyVar def_strat tv | isRuntimeRepVar tv , default_ns_vars - -- Do not quantify over a RuntimeRep var - -- unless it is a TyVarTv, handled earlier = do { traceTc "Defaulting a RuntimeRep var to LiftedRep" (ppr tv) ; writeMetaTyVar tv liftedRepTy ; return True } @@ -2414,22 +2350,38 @@ zonkWC :: WantedConstraints -> TcM WantedConstraints zonkWC wc = zonkWCRec wc zonkWCRec :: WantedConstraints -> TcM WantedConstraints -zonkWCRec (WC { wc_simple = simple, wc_impl = implic, wc_holes = holes }) +zonkWCRec (WC { wc_simple = simple, wc_impl = implic, wc_errors = errs }) = do { simple' <- zonkSimples simple ; implic' <- mapBagM zonkImplication implic - ; holes' <- mapBagM zonkHole holes - ; return (WC { wc_simple = simple', wc_impl = implic', wc_holes = holes' }) } + ; errs' <- mapBagM zonkDelayedError errs + ; return (WC { wc_simple = simple', wc_impl = implic', wc_errors = errs' }) } zonkSimples :: Cts -> TcM Cts zonkSimples cts = do { cts' <- mapBagM zonkCt cts ; traceTc "zonkSimples done:" (ppr cts') ; return cts' } +zonkDelayedError :: DelayedError -> TcM DelayedError +zonkDelayedError (DE_Hole hole) + = DE_Hole <$> zonkHole hole +zonkDelayedError (DE_NotConcrete err) + = DE_NotConcrete <$> zonkNotConcreteError err + zonkHole :: Hole -> TcM Hole zonkHole hole@(Hole { hole_ty = ty }) = do { ty' <- zonkTcType ty ; return (hole { hole_ty = ty' }) } +zonkNotConcreteError :: NotConcreteError -> TcM NotConcreteError +zonkNotConcreteError err@(NCE_FRR { nce_frr_origin = frr_orig }) + = do { frr_orig <- zonkFRROrigin frr_orig + ; return $ err { nce_frr_origin = frr_orig } } + +zonkFRROrigin :: FixedRuntimeRepOrigin -> TcM FixedRuntimeRepOrigin +zonkFRROrigin (FixedRuntimeRepOrigin ty orig) + = do { ty' <- zonkTcType ty + ; return $ FixedRuntimeRepOrigin ty' orig } + {- Note [zonkCt behaviour] ~~~~~~~~~~~~~~~~~~~~~~~~~~ zonkCt tries to maintain the canonical form of a Ct. For example, @@ -2667,9 +2619,6 @@ zonkTidyOrigin env (CycleBreakerOrigin orig) zonkTidyOrigin env (InstProvidedOrigin mod cls_inst) = do { (env1, is_tys') <- mapAccumLM zonkTidyTcType env (is_tys cls_inst) ; return (env1, InstProvidedOrigin mod (cls_inst {is_tys = is_tys'})) } -zonkTidyOrigin env (FixedRuntimeRepOrigin ty frr_orig) - = do { (env1, ty') <- zonkTidyTcType env ty - ; return (env1, FixedRuntimeRepOrigin ty' frr_orig)} zonkTidyOrigin env (WantedSuperclassOrigin pty orig) = do { (env1, pty') <- zonkTidyTcType env pty ; (env2, orig') <- zonkTidyOrigin env1 orig @@ -2679,6 +2628,26 @@ zonkTidyOrigin env orig = return (env, orig) zonkTidyOrigins :: TidyEnv -> [CtOrigin] -> TcM (TidyEnv, [CtOrigin]) zonkTidyOrigins = mapAccumLM zonkTidyOrigin +zonkTidyFRRInfos :: TidyEnv + -> [FixedRuntimeRepErrorInfo] + -> TcM (TidyEnv, [FixedRuntimeRepErrorInfo]) +zonkTidyFRRInfos = go [] + where + go zs env [] = return (env, reverse zs) + go zs env (FRR_Info { frr_info_origin = FixedRuntimeRepOrigin ty orig + , frr_info_not_concrete = mb_not_conc } : tys) + = do { (env, ty) <- zonkTidyTcType env ty + ; (env, mb_not_conc) <- go_mb_not_conc env mb_not_conc + ; let info = FRR_Info { frr_info_origin = FixedRuntimeRepOrigin ty orig + , frr_info_not_concrete = mb_not_conc } + ; go (info:zs) env tys } + + go_mb_not_conc env Nothing = return (env, Nothing) + go_mb_not_conc env (Just (tv, ty)) + = do { (env, tv) <- return $ tidyOpenTyCoVar env tv + ; (env, ty) <- zonkTidyTcType env ty + ; return (env, Just (tv, ty)) } + ---------------- tidyCt :: TidyEnv -> Ct -> Ct -- Used only in error reporting @@ -2694,6 +2663,20 @@ tidyCtEvidence env ctev = ctev { ctev_pred = tidyType env ty } tidyHole :: TidyEnv -> Hole -> Hole tidyHole env h@(Hole { hole_ty = ty }) = h { hole_ty = tidyType env ty } +tidyDelayedError :: TidyEnv -> DelayedError -> DelayedError +tidyDelayedError env (DE_Hole hole) + = DE_Hole $ tidyHole env hole +tidyDelayedError env (DE_NotConcrete err) + = DE_NotConcrete $ tidyConcreteError env err + +tidyConcreteError :: TidyEnv -> NotConcreteError -> NotConcreteError +tidyConcreteError env err@(NCE_FRR { nce_frr_origin = frr_orig }) + = err { nce_frr_origin = tidyFRROrigin env frr_orig } + +tidyFRROrigin :: TidyEnv -> FixedRuntimeRepOrigin -> FixedRuntimeRepOrigin +tidyFRROrigin env (FixedRuntimeRepOrigin ty orig) + = FixedRuntimeRepOrigin (tidyType env ty) orig + ---------------- tidyEvVar :: TidyEnv -> EvVar -> EvVar tidyEvVar env var = updateIdTypeAndMult (tidyType env) var diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs index 57f2dcd358..9caf6c9f5b 100644 --- a/compiler/GHC/Tc/Utils/TcType.hs +++ b/compiler/GHC/Tc/Utils/TcType.hs @@ -1,6 +1,7 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TupleSections #-} {-# OPTIONS_GHC -Wno-incomplete-record-updates #-} @@ -22,14 +23,14 @@ module GHC.Tc.Utils.TcType ( -------------------------------- -- Types - TcType, TcSigmaType, TcSigmaTypeFRR, + TcType, TcSigmaType, TcTypeFRR, TcSigmaTypeFRR, TcRhoType, TcTauType, TcPredType, TcThetaType, TcTyVar, TcTyVarSet, TcDTyVarSet, TcTyCoVarSet, TcDTyCoVarSet, TcKind, TcCoVar, TcTyCoVar, TcTyVarBinder, TcInvisTVBinder, TcReqTVBinder, TcTyCon, MonoTcTyCon, PolyTcTyCon, TcTyConBinder, KnotTied, ExpType(..), InferResult(..), - ExpSigmaType, ExpSigmaTypeFRR, + ExpTypeFRR, ExpSigmaType, ExpSigmaTypeFRR, ExpRhoType, mkCheckExpType, @@ -45,7 +46,8 @@ module GHC.Tc.Utils.TcType ( MetaDetails(Flexi, Indirect), MetaInfo(..), skolemSkolInfo, isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isMetaTyVarTy, isTyVarTy, tcIsTcTyVar, isTyVarTyVar, isOverlappableTyVar, isTyConableTyVar, - isConcreteTyVar, + ConcreteTvOrigin(..), isConcreteTyVar_maybe, isConcreteTyVar, + isConcreteTyVarTy, isConcreteTyVarTy_maybe, isAmbiguousTyVar, isCycleBreakerTyVar, metaTyVarRef, metaTyVarInfo, isFlexi, isIndirect, isRuntimeUnkSkol, metaTyVarTcLevel, setMetaTyVarTcLevel, metaTyVarTcLevel_maybe, @@ -216,6 +218,10 @@ import GHC.Core.Predicate import GHC.Types.RepType import GHC.Core.TyCon +import {-# SOURCE #-} GHC.Tc.Types.Origin + ( SkolemInfo, unkSkol + , FixedRuntimeRepOrigin, FixedRuntimeRepContext ) + -- others: import GHC.Driver.Session import GHC.Core.FVs @@ -240,7 +246,6 @@ import qualified GHC.LanguageExtensions as LangExt import Data.IORef import Data.List.NonEmpty( NonEmpty(..) ) import Data.List ( partition ) -import {-# SOURCE #-} GHC.Tc.Types.Origin ( unkSkol, SkolemInfo ) {- @@ -346,6 +351,11 @@ type TcCoVar = CoVar -- Used only during type inference type TcType = Type -- A TcType can have mutable type variables type TcTyCoVar = Var -- Either a TcTyVar or a CoVar +-- | A type which has a syntactically fixed RuntimeRep as per +-- Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete. +type TcTypeFRR = TcType + -- TODO: consider making this a newtype. + type TcTyVarBinder = TyVarBinder type TcInvisTVBinder = InvisTVBinder type TcReqTVBinder = ReqTVBinder @@ -361,8 +371,9 @@ type TcPredType = PredType type TcThetaType = ThetaType type TcSigmaType = TcType --- | A 'TcSigmaTypeFRR' is a 'TcSigmaType' which has a fixed 'RuntimeRep' --- in the sense of Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete. +-- | A 'TcSigmaTypeFRR' is a 'TcSigmaType' which has a syntactically +-- fixed 'RuntimeRep' in the sense of Note [Fixed RuntimeRep] +-- in GHC.Tc.Utils.Concrete. -- -- In particular, this means that: -- @@ -373,6 +384,8 @@ type TcSigmaType = TcType -- we want to provide argument types which have a known runtime representation. -- See Note [Return arguments with a fixed RuntimeRep. type TcSigmaTypeFRR = TcSigmaType + -- TODO: consider making this a newtype. + type TcRhoType = TcType -- Note [TcRhoType] type TcTauType = TcType type TcKind = Kind @@ -438,17 +451,38 @@ data ExpType = Check TcType | Infer !InferResult data InferResult - = IR { ir_uniq :: Unique -- For debugging only + = IR { ir_uniq :: Unique + -- ^ This 'Unique' is for debugging only - , ir_lvl :: TcLevel -- See Note [TcLevel of ExpType] in GHC.Tc.Utils.TcMType + , ir_lvl :: TcLevel + -- ^ See Note [TcLevel of ExpType] in GHC.Tc.Utils.TcMType + + , ir_frr :: Maybe FixedRuntimeRepContext + -- ^ See Note [FixedRuntimeRep context in ExpType] in GHC.Tc.Utils.TcMType , ir_ref :: IORef (Maybe TcType) } - -- The type that fills in this hole should be a Type, - -- that is, its kind should be (TYPE rr) for some rr + -- ^ The type that fills in this hole should be a @Type@, + -- that is, its kind should be @TYPE rr@ for some @rr :: RuntimeRep@. + -- + -- Additionally, if the 'ir_frr' field is @Just frr_orig@ then + -- @rr@ must be concrete, in the sense of Note [Concrete types] + -- in GHC.Tc.Utils.Concrete. type ExpSigmaType = ExpType + +-- | An 'ExpType' which has a fixed RuntimeRep. +-- +-- For a 'Check' 'ExpType', the stored 'TcType' must have +-- a fixed RuntimeRep. For an 'Infer' 'ExpType', the 'ir_frr' +-- field must be of the form @Just frr_orig@. +type ExpTypeFRR = ExpType + -- | Like 'TcSigmaTypeFRR', but for an expected type. -type ExpSigmaTypeFRR = ExpType +-- +-- See 'ExpTypeFRR'. +type ExpSigmaTypeFRR = ExpTypeFRR + -- TODO: consider making this a newtype. + type ExpRhoType = ExpType instance Outputable ExpType where @@ -456,8 +490,12 @@ instance Outputable ExpType where ppr (Infer ir) = ppr ir instance Outputable InferResult where - ppr (IR { ir_uniq = u, ir_lvl = lvl }) - = text "Infer" <> braces (ppr u <> comma <> ppr lvl) + ppr (IR { ir_uniq = u, ir_lvl = lvl, ir_frr = mb_frr }) + = text "Infer" <> mb_frr_text <> braces (ppr u <> comma <> ppr lvl) + where + mb_frr_text = case mb_frr of + Just _ -> text "FRR" + Nothing -> empty -- | Make an 'ExpType' suitable for checking. mkCheckExpType :: TcType -> ExpType @@ -587,6 +625,8 @@ data MetaDetails = Flexi -- Flexi type variables unify to become Indirects | Indirect TcType +-- | What restrictions are on this metavariable around unification? +-- These are checked in GHC.Tc.Utils.Unify.startSolvingByUnification. data MetaInfo = TauTv -- ^ This MetaTv is an ordinary unification variable -- A TauTv is always filled in with a tau-type, which @@ -603,22 +643,32 @@ data MetaInfo -- See Note [Type variable cycles] in -- GHC.Tc.Solver.Canonical - | ConcreteTv + | ConcreteTv ConcreteTvOrigin -- ^ A unification variable that can only be unified -- with a concrete type, in the sense of -- Note [Concrete types] in GHC.Tc.Utils.Concrete. -- See Note [ConcreteTv] in GHC.Tc.Utils.Concrete. + -- See also Note [The Concrete mechanism] in GHC.Tc.Utils.Concrete + -- for an overview of how this works in context. instance Outputable MetaDetails where ppr Flexi = text "Flexi" ppr (Indirect ty) = text "Indirect" <+> ppr ty instance Outputable MetaInfo where - ppr TauTv = text "tau" - ppr TyVarTv = text "tyv" - ppr RuntimeUnkTv = text "rutv" - ppr CycleBreakerTv = text "cbv" - ppr ConcreteTv = text "conc" + ppr TauTv = text "tau" + ppr TyVarTv = text "tyv" + ppr RuntimeUnkTv = text "rutv" + ppr CycleBreakerTv = text "cbv" + ppr (ConcreteTv {}) = text "conc" + +-- | What caused us to create a 'ConcreteTv' metavariable? +-- See Note [ConcreteTv] in GHC.Tc.Utils.Concrete. +data ConcreteTvOrigin + -- | A 'ConcreteTv' used to enforce the representation-polymorphism invariants. + -- + -- See 'FixedRuntimeRepOrigin' for more information. + = ConcreteFRR FixedRuntimeRepOrigin {- ********************************************************************* * * @@ -1091,7 +1141,7 @@ isMetaTyVar tv -- isAmbiguousTyVar is used only when reporting type errors -- It picks out variables that are unbound, namely meta --- type variables and the RuntimUnk variables created by +-- type variables and the RuntimeUnk variables created by -- GHC.Runtime.Heap.Inspect.zonkRTTIType. These are "ambiguous" in -- the sense that they stand for an as-yet-unknown type isAmbiguousTyVar tv @@ -1113,14 +1163,31 @@ isCycleBreakerTyVar tv -- | Is this type variable a concrete type variable, i.e. -- it is a metavariable with 'ConcreteTv' 'MetaInfo'? -- --- Works with both 'TyVar' and 'TcTyVar'. -isConcreteTyVar :: TcTyVar -> Bool -isConcreteTyVar tv +-- Returns the 'ConcreteTvOrigin' stored in the type variable +-- if so, or 'Nothing' otherwise. +isConcreteTyVar_maybe :: TcTyVar -> Maybe ConcreteTvOrigin +isConcreteTyVar_maybe tv | isTcTyVar tv - , MetaTv { mtv_info = ConcreteTv } <- tcTyVarDetails tv - = True + , MetaTv { mtv_info = ConcreteTv conc_orig } <- tcTyVarDetails tv + = Just conc_orig | otherwise - = False + = Nothing + +-- | Is this type variable a concrete type variable, i.e. +-- it is a metavariable with 'ConcreteTv' 'MetaInfo'? +isConcreteTyVar :: TcTyVar -> Bool +isConcreteTyVar = isJust . isConcreteTyVar_maybe + +-- | Is this type concrete type variable, i.e. +-- a metavariable with 'ConcreteTv' 'MetaInfo'? +isConcreteTyVarTy :: TcType -> Bool +isConcreteTyVarTy = isJust . isConcreteTyVarTy_maybe + +-- | Is this type a concrete type variable? If so, return +-- the associated 'TcTyVar' and 'ConcreteTvOrigin'. +isConcreteTyVarTy_maybe :: TcType -> Maybe (TcTyVar, ConcreteTvOrigin) +isConcreteTyVarTy_maybe (TyVarTy tv) = (tv, ) <$> isConcreteTyVar_maybe tv +isConcreteTyVarTy_maybe _ = Nothing isMetaTyVarTy :: TcType -> Bool isMetaTyVarTy (TyVarTy tv) = isMetaTyVar tv @@ -1933,9 +2000,6 @@ isImprovementPred ty ClassPred cls _ -> classHasFds cls IrredPred {} -> True -- Might have equalities after reduction? ForAllPred {} -> False - SpecialPred s -> - case s of - IsReflPrimPred {} -> False {- Note [Expanding superclasses] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -2077,7 +2141,6 @@ isRigidTy ty | isForAllTy ty = True | otherwise = False - {- ************************************************************************ * * diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs index c19b592765..8ffbfb959b 100644 --- a/compiler/GHC/Tc/Utils/Unify.hs +++ b/compiler/GHC/Tc/Utils/Unify.hs @@ -1,6 +1,6 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TupleSections #-} -{-# LANGUAGE RecursiveDo #-} +{-# LANGUAGE RecursiveDo #-} {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} {-# OPTIONS_GHC -Wno-incomplete-record-updates #-} @@ -23,7 +23,7 @@ module GHC.Tc.Utils.Unify ( -- Various unifications unifyType, unifyKind, unifyExpectedType, uType, promoteTcType, - swapOverTyVars, canSolveByUnification, + swapOverTyVars, startSolvingByUnification, -------------------------------- -- Holes @@ -44,7 +44,7 @@ import GHC.Prelude import GHC.Hs import GHC.Core.TyCo.Rep import GHC.Core.TyCo.Ppr( debugPprType ) -import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep_MustBeRefl ) +import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep, makeTypeConcrete, hasFixedRuntimeRep_syntactic ) import GHC.Tc.Utils.Env import GHC.Tc.Utils.Instantiate import GHC.Tc.Utils.Monad @@ -88,8 +88,10 @@ import qualified Data.Semigroup as S ( (<>) ) -- | 'matchActualFunTySigma' looks for just one function arrow, -- returning an uninstantiated sigma-type. -- --- Invariant: the returned argument type has a fixed RuntimeRep --- as per Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete. +-- Invariant: the returned argument type has a syntactically fixed +-- RuntimeRep in the sense of Note [Fixed RuntimeRep] +-- in GHC.Tc.Utils.Concrete. +-- -- See Note [Return arguments with a fixed RuntimeRep]. matchActualFunTySigma :: ExpectedFunTyOrigin @@ -100,7 +102,7 @@ matchActualFunTySigma -- ^ Total number of value args in the call, and -- types of values args to which function has -- been applied already (reversed) - -- Both are used only for error messages) + -- (Both are used only for error messages) -> TcRhoType -- ^ Type to analyse: a TcRhoType -> TcM (HsWrapper, Scaled TcSigmaTypeFRR, TcSigmaType) @@ -126,13 +128,13 @@ matchActualFunTySigma herald mb_thing err_info fun_ty -- If allocated (fresh-meta-var1 -> fresh-meta-var2) and unified, we'd -- hide the forall inside a meta-variable go :: TcRhoType -- The type we're processing, perhaps after - -- expanding any type synonym + -- expanding type synonyms -> TcM (HsWrapper, Scaled TcSigmaTypeFRR, TcSigmaType) go ty | Just ty' <- tcView ty = go ty' go (FunTy { ft_af = af, ft_mult = w, ft_arg = arg_ty, ft_res = res_ty }) = assert (af == VisArg) $ - do { hasFixedRuntimeRep_MustBeRefl (FRRExpectedFunTy herald 0) arg_ty + do { hasFixedRuntimeRep_syntactic (FRRExpectedFunTy herald 1) arg_ty ; return (idHsWrapper, Scaled w arg_ty, res_ty) } go ty@(TyVarTy tv) @@ -166,7 +168,7 @@ matchActualFunTySigma herald mb_thing err_info fun_ty ; mult <- newFlexiTyVarTy multiplicityTy ; let unif_fun_ty = mkVisFunTy mult arg_ty res_ty ; co <- unifyType mb_thing fun_ty unif_fun_ty - ; hasFixedRuntimeRep_MustBeRefl (FRRExpectedFunTy herald 0) arg_ty + ; hasFixedRuntimeRep_syntactic (FRRExpectedFunTy herald 1) arg_ty ; return (mkWpCastN co, Scaled mult arg_ty, res_ty) } ------------ @@ -201,7 +203,7 @@ Ugh! -- | Like 'matchExpectedFunTys', but used when you have an "actual" type, -- for example in function application. -- --- INVARIANT: the returned arguemnt types all have a fixed RuntimeRep +-- INVARIANT: the returned arguemnt types all have a syntactically fixed RuntimeRep -- in the sense of Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete. -- See Note [Return arguments with a fixed RuntimeRep]. matchActualFunTysRho :: ExpectedFunTyOrigin -- ^ See Note [Herald for matchExpectedFunTys] @@ -233,7 +235,7 @@ matchActualFunTysRho herald ct_orig mb_thing n_val_args_wanted fun_ty ; (wrap_res, arg_tys, res_ty) <- go (n-1) (arg_ty1:so_far) res_ty1 ; let wrap_fun2 = mkWpFun idHsWrapper wrap_res arg_ty1 res_ty -- NB: arg_ty1 comes from matchActualFunTySigma, so it has - -- a fixed RuntimeRep as neede to call mkWpFun. + -- a syntactically fixed RuntimeRep as needed to call mkWpFun. ; return (wrap_fun2 <.> wrap_fun1, arg_ty1:arg_tys, res_ty) } {- @@ -313,7 +315,7 @@ of the representation-polymorphism invariants of Note [Representation polymorphism invariants] in GHC.Core. This is why all these functions have an additional invariant, -that the argument types they return all have a fixed RuntimeRep, +that the argument types they return all have a syntactically fixed RuntimeRep, in the sense of Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete. Example: @@ -356,7 +358,7 @@ Example: -- This function skolemises at each polytype. -- -- Invariant: this function only applies the provided function --- to a list of argument types which all have a fixed RuntimeRep +-- to a list of argument types which all have a syntactically fixed RuntimeRep -- in the sense of Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete. -- See Note [Return arguments with a fixed RuntimeRep]. matchExpectedFunTys :: forall a. @@ -366,7 +368,7 @@ matchExpectedFunTys :: forall a. -> ExpRhoType -- Skolemised -> ([Scaled ExpSigmaTypeFRR] -> ExpRhoType -> TcM a) -> TcM (HsWrapper, a) --- If matchExpectedFunTys n ty = (_, wrap) +-- If matchExpectedFunTys n ty = (wrap, _) -- then wrap : (t1 -> ... -> tn -> ty_r) ~> ty, -- where [t1, ..., tn], ty_r are passed to the thing_inside matchExpectedFunTys herald ctx arity orig_ty thing_inside @@ -394,14 +396,13 @@ matchExpectedFunTys herald ctx arity orig_ty thing_inside go acc_arg_tys n (FunTy { ft_mult = mult, ft_af = af, ft_arg = arg_ty, ft_res = res_ty }) = assert (af == VisArg) $ - do { let arg_pos = length acc_arg_tys -- for error messages only - ; hasFixedRuntimeRep_MustBeRefl (FRRExpectedFunTy herald arg_pos) arg_ty + do { let arg_pos = 1 + length acc_arg_tys -- for error messages only + ; (arg_co, arg_ty) <- hasFixedRuntimeRep (FRRExpectedFunTy herald arg_pos) arg_ty ; (wrap_res, result) <- go ((Scaled mult $ mkCheckExpType arg_ty) : acc_arg_tys) (n-1) res_ty - ; let fun_wrap = mkWpFun idHsWrapper wrap_res (Scaled mult arg_ty) res_ty - -- NB: we are ensuring that arg_ty has a fixed RuntimeRep, - -- so we satisfy the precondition that mkWpFun requires. - ; return ( fun_wrap, result ) } + ; let wrap_arg = mkWpCastN arg_co + fun_wrap = mkWpFun wrap_arg wrap_res (Scaled mult arg_ty) res_ty + ; return (fun_wrap, result) } go acc_arg_tys n ty@(TyVarTy tv) | isMetaTyVar tv @@ -431,21 +432,22 @@ matchExpectedFunTys herald ctx arity orig_ty thing_inside ------------ defer :: [Scaled ExpSigmaTypeFRR] -> Arity -> ExpRhoType -> TcM (HsWrapper, a) defer acc_arg_tys n fun_ty - = do { more_arg_tys <- replicateM n (mkScaled <$> newFlexiTyVarTy multiplicityTy <*> newInferExpType) + = do { let last_acc_arg_pos = length acc_arg_tys + ; more_arg_tys <- mapM new_exp_arg_ty [last_acc_arg_pos + 1 .. last_acc_arg_pos + n] ; res_ty <- newInferExpType ; result <- thing_inside (reverse acc_arg_tys ++ more_arg_tys) res_ty ; more_arg_tys <- mapM (\(Scaled m t) -> Scaled m <$> readExpType t) more_arg_tys - ; zipWithM_ - ( \ i (Scaled _ arg_ty) -> - hasFixedRuntimeRep_MustBeRefl (FRRExpectedFunTy herald i) arg_ty ) - [0..] - more_arg_tys ; res_ty <- readExpType res_ty ; let unif_fun_ty = mkVisFunTys more_arg_tys res_ty ; wrap <- tcSubType AppOrigin ctx unif_fun_ty fun_ty -- Not a good origin at all :-( ; return (wrap, result) } + new_exp_arg_ty :: Int -> TcM (Scaled ExpSigmaTypeFRR) + new_exp_arg_ty arg_pos -- position for error messages only + = mkScaled <$> newFlexiTyVarTy multiplicityTy + <*> newInferExpTypeFRR (FRRExpectedFunTy herald arg_pos) + ------------ mk_ctxt :: [Scaled ExpSigmaTypeFRR] -> TcType -> TidyEnv -> TcM (TidyEnv, SDoc) mk_ctxt arg_tys res_ty env @@ -572,6 +574,167 @@ matchExpectedAppTy orig_ty kind2 = liftedTypeKind -- m :: * -> k -- arg type :: * +{- ********************************************************************** +* + fillInferResult +* +********************************************************************** -} + +{- Note [inferResultToType] +~~~~~~~~~~~~~~~~~~~~~~~~~~~ +expTypeToType and inferResultType convert an InferResult to a monotype. +It must be a monotype because if the InferResult isn't already filled in, +we fill it in with a unification variable (hence monotype). So to preserve +order-independence we check for mono-type-ness even if it *is* filled in +already. + +See also Note [TcLevel of ExpType] in GHC.Tc.Utils.TcType, and +Note [fillInferResult]. +-} + +-- | Fill an 'InferResult' with the given type. +-- +-- If @co = fillInferResult t1 infer_res@, then @co :: t1 ~# t2@, +-- where @t2@ is the type stored in the 'ir_ref' field of @infer_res@. +-- +-- This function enforces the following invariants: +-- +-- - Level invariant. +-- The stored type @t2@ is at the same level as given by the +-- 'ir_lvl' field. +-- - FRR invariant. +-- Whenever the 'ir_frr' field is not @Nothing@, @t2@ is guaranteed +-- to have a syntactically fixed RuntimeRep, in the sense of +-- Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete. +fillInferResult :: TcType -> InferResult -> TcM TcCoercionN +fillInferResult act_res_ty (IR { ir_uniq = u + , ir_lvl = res_lvl + , ir_frr = mb_frr + , ir_ref = ref }) + = do { mb_exp_res_ty <- readTcRef ref + ; case mb_exp_res_ty of + Just exp_res_ty + -- We progressively refine the type stored in 'ref', + -- for example when inferring types across multiple equations. + -- + -- Example: + -- + -- \ x -> case y of { True -> x ; False -> 3 :: Int } + -- + -- When inferring the return type of this function, we will create + -- an 'Infer' 'ExpType', which will first be filled by the type of 'x' + -- after typechecking the first equation, and then filled again with + -- the type 'Int', at which point we want to ensure that we unify + -- the type of 'x' with 'Int'. This is what is happening below when + -- we are "joining" several inferred 'ExpType's. + -> do { traceTc "Joining inferred ExpType" $ + ppr u <> colon <+> ppr act_res_ty <+> char '~' <+> ppr exp_res_ty + ; cur_lvl <- getTcLevel + ; unless (cur_lvl `sameDepthAs` res_lvl) $ + ensureMonoType act_res_ty + ; unifyType Nothing act_res_ty exp_res_ty } + Nothing + -> do { traceTc "Filling inferred ExpType" $ + ppr u <+> text ":=" <+> ppr act_res_ty + + -- Enforce the level invariant: ensure the TcLevel of + -- the type we are writing to 'ref' matches 'ir_lvl'. + ; (prom_co, act_res_ty) <- promoteTcType res_lvl act_res_ty + + -- Enforce the FRR invariant: ensure the type has a syntactically + -- fixed RuntimeRep (if necessary, i.e. 'mb_frr' is not 'Nothing'). + ; (frr_co, act_res_ty) <- + case mb_frr of + Nothing -> return (mkNomReflCo act_res_ty, act_res_ty) + Just frr_orig -> hasFixedRuntimeRep frr_orig act_res_ty + + -- Compose the two coercions. + ; let final_co = prom_co `mkTcTransCo` frr_co + + ; writeTcRef ref (Just act_res_ty) + + ; return final_co } + } + +{- Note [fillInferResult] +~~~~~~~~~~~~~~~~~~~~~~~~~ +When inferring, we use fillInferResult to "fill in" the hole in InferResult + data InferResult = IR { ir_uniq :: Unique + , ir_lvl :: TcLevel + , ir_ref :: IORef (Maybe TcType) } + +There are two things to worry about: + +1. What if it is under a GADT or existential pattern match? + - GADTs: a unification variable (and Infer's hole is similar) is untouchable + - Existentials: be careful about skolem-escape + +2. What if it is filled in more than once? E.g. multiple branches of a case + case e of + T1 -> e1 + T2 -> e2 + +Our typing rules are: + +* The RHS of a existential or GADT alternative must always be a + monotype, regardless of the number of alternatives. + +* Multiple non-existential/GADT branches can have (the same) + higher rank type (#18412). E.g. this is OK: + case e of + True -> hr + False -> hr + where hr:: (forall a. a->a) -> Int + c.f. Section 7.1 of "Practical type inference for arbitrary-rank types" + We use choice (2) in that Section. + (GHC 8.10 and earlier used choice (1).) + + But note that + case e of + True -> hr + False -> \x -> hr x + will fail, because we still /infer/ both branches, so the \x will get + a (monotype) unification variable, which will fail to unify with + (forall a. a->a) + +For (1) we can detect the GADT/existential situation by seeing that +the current TcLevel is greater than that stored in ir_lvl of the Infer +ExpType. We bump the level whenever we go past a GADT/existential match. + +Then, before filling the hole use promoteTcType to promote the type +to the outer ir_lvl. promoteTcType does this + - create a fresh unification variable alpha at level ir_lvl + - emits an equality alpha[ir_lvl] ~ ty + - fills the hole with alpha +That forces the type to be a monotype (since unification variables can +only unify with monotypes); and catches skolem-escapes because the +alpha is untouchable until the equality floats out. + +For (2), we simply look to see if the hole is filled already. + - if not, we promote (as above) and fill the hole + - if it is filled, we simply unify with the type that is + already there + +There is one wrinkle. Suppose we have + case e of + T1 -> e1 :: (forall a. a->a) -> Int + G2 -> e2 +where T1 is not GADT or existential, but G2 is a GADT. Then supppose the +T1 alternative fills the hole with (forall a. a->a) -> Int, which is fine. +But now the G2 alternative must not *just* unify with that else we'd risk +allowing through (e2 :: (forall a. a->a) -> Int). If we'd checked G2 first +we'd have filled the hole with a unification variable, which enforces a +monotype. + +So if we check G2 second, we still want to emit a constraint that restricts +the RHS to be a monotype. This is done by ensureMonoType, and it works +by simply generating a constraint (alpha ~ ty), where alpha is a fresh +unification variable. We discard the evidence. + +-} + + + {- ************************************************************************ * * @@ -1451,7 +1614,6 @@ If available, we defer original types (rather than those where closed type synonyms have already been expanded via tcCoreView). This is, as usual, to improve error messages. - ************************************************************************ * * uUnfilledVar and friends @@ -1533,10 +1695,13 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2 go cur_lvl | isTouchableMetaTyVar cur_lvl tv1 -- See Note [Unification preconditions], (UNTOUCHABLE) wrinkles - , canSolveByUnification (metaTyVarInfo tv1) ty2 , cterHasNoProblem (checkTyVarEq tv1 ty2) -- See Note [Prevent unification with type families] - = do { co_k <- uType KindLevel kind_origin (tcTypeKind ty2) (tyVarKind tv1) + = do { can_continue_solving <- startSolvingByUnification (metaTyVarInfo tv1) ty2 + ; if not can_continue_solving + then not_ok_so_defer + else + do { co_k <- uType KindLevel kind_origin (tcTypeKind ty2) (tyVarKind tv1) ; traceTc "uUnfilledVar2 ok" $ vcat [ ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1) , ppr ty2 <+> dcolon <+> ppr (tcTypeKind ty2) @@ -1549,46 +1714,61 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2 then do { writeMetaTyVar tv1 ty2 ; return (mkTcNomReflCo ty2) } - else defer } -- This cannot be solved now. See GHC.Tc.Solver.Canonical - -- Note [Equalities with incompatible kinds] for how - -- this will be dealt with in the solver + else defer }} -- This cannot be solved now. See GHC.Tc.Solver.Canonical + -- Note [Equalities with incompatible kinds] for how + -- this will be dealt with in the solver | otherwise - = do { traceTc "uUnfilledVar2 not ok" (ppr tv1 $$ ppr ty2) - -- Occurs check or an untouchable: just defer - -- NB: occurs check isn't necessarily fatal: - -- eg tv1 occurred in type family parameter - ; defer } + = not_ok_so_defer ty1 = mkTyVarTy tv1 kind_origin = KindEqOrigin ty1 ty2 origin (Just t_or_k) defer = unSwap swapped (uType_defer t_or_k origin) ty1 ty2 + not_ok_so_defer = + do { traceTc "uUnfilledVar2 not ok" (ppr tv1 $$ ppr ty2) + -- Occurs check or an untouchable: just defer + -- NB: occurs check isn't necessarily fatal: + -- eg tv1 occurred in type family parameter + ; defer } + -- | Checks (TYVAR-TV), (COERCION-HOLE) and (CONCRETE) of -- Note [Unification preconditions]; returns True if these conditions -- are satisfied. But see the Note for other preconditions, too. -canSolveByUnification :: MetaInfo -> TcType -- zonked - -> Bool -canSolveByUnification _ xi - | hasCoercionHoleTy xi -- (COERCION-HOLE) check - = False -canSolveByUnification info xi +startSolvingByUnification :: MetaInfo -> TcType -- zonked + -> TcM Bool +startSolvingByUnification _ xi + | hasCoercionHoleTy xi -- (COERCION-HOLE) check + = return False +startSolvingByUnification info xi = case info of - CycleBreakerTv -> False - ConcreteTv -> isConcrete xi -- (CONCRETE) check + CycleBreakerTv -> return False + ConcreteTv conc_orig -> + do { (_, not_conc_reasons) <- makeTypeConcrete conc_orig xi + -- NB: makeTypeConcrete has the side-effect of turning + -- some TauTvs into ConcreteTvs, e.g. + -- alpha[conc] ~# TYPE (TupleRep '[ beta[tau], IntRep ]) + -- will write `beta[tau] := beta[conc]`. + -- + -- We don't need to track these unifications for the purposes + -- of constraint solving (e.g. updating tcs_unified or tcs_unif_lvl), + -- as they don't unlock any further progress. + ; case not_conc_reasons of + [] -> return True + _ -> return False } TyVarTv -> case tcGetTyVar_maybe xi of - Nothing -> False + Nothing -> return False Just tv -> case tcTyVarDetails tv of -- (TYVAR-TV) wrinkle - SkolemTv {} -> True - RuntimeUnk -> True + SkolemTv {} -> return True + RuntimeUnk -> return True MetaTv { mtv_info = info } -> case info of - TyVarTv -> True - _ -> False - _ -> True + TyVarTv -> return True + _ -> return False + _ -> return True swapOverTyVars :: Bool -> TcTyVar -> TcTyVar -> Bool swapOverTyVars is_given tv1 tv2 @@ -1630,7 +1810,7 @@ lhsPriority tv MetaTv { mtv_info = info } -> case info of CycleBreakerTv -> 0 TyVarTv -> 1 - ConcreteTv -> 2 + ConcreteTv {} -> 2 TauTv -> 3 RuntimeUnkTv -> 4 @@ -1689,6 +1869,14 @@ There are five reasons not to unify: if we can rewrite `F Int` to a concrete type, say `FloatRep`, then we will have `rr[conc] ~ FloatRep` and we can unify `rr ~ FloatRep`. + Note that we can still make progress on unification even if + we can't fully solve an equality, e.g. + + alpha[conc] ~# TupleRep '[ beta[tau], F gamma[tau] ] + + we can fill beta[tau] := beta[conc]. This is why we call + 'makeTypeConcrete' in startSolvingByUnification. + 5. (COERCION-HOLE) Confusing coercion holes Suppose our equality is (alpha :: k) ~ (Int |> {co}) @@ -2071,10 +2259,10 @@ checkTypeEq :: CanEqLHS -> TcType -> CheckTyEqResult checkTypeEq lhs ty = go ty where - impredicative = cteProblem cteImpredicative - type_family = cteProblem cteTypeFamily - insoluble_occurs = cteProblem cteInsolubleOccurs - soluble_occurs = cteProblem cteSolubleOccurs + impredicative = cteProblem cteImpredicative + type_family = cteProblem cteTypeFamily + insoluble_occurs = cteProblem cteInsolubleOccurs + soluble_occurs = cteProblem cteSolubleOccurs -- The GHCi runtime debugger does its type-matching with -- unification variables that can unify with a polytype diff --git a/compiler/GHC/Tc/Utils/Unify.hs-boot b/compiler/GHC/Tc/Utils/Unify.hs-boot index dc8bcce6e8..8afdbcd5ed 100644 --- a/compiler/GHC/Tc/Utils/Unify.hs-boot +++ b/compiler/GHC/Tc/Utils/Unify.hs-boot @@ -1,15 +1,15 @@ module GHC.Tc.Utils.Unify where import GHC.Prelude +import GHC.Core.Type ( Mult ) import GHC.Tc.Utils.TcType ( TcTauType ) import GHC.Tc.Types ( TcM ) import GHC.Tc.Types.Evidence ( TcCoercion, HsWrapper ) -import GHC.Tc.Types.Origin ( CtOrigin, TypedThing ) -import GHC.Hs.Type ( Mult ) +import GHC.Tc.Types.Origin ( CtOrigin, TypedThing ) -- This boot file exists only to tie the knot between --- GHC.Tc.Utils.Unify and Inst +-- GHC.Tc.Utils.Unify and GHC.Tc.Utils.Instantiate unifyType :: Maybe TypedThing -> TcTauType -> TcTauType -> TcM TcCoercion unifyKind :: Maybe TypedThing -> TcTauType -> TcTauType -> TcM TcCoercion |