diff options
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/GHC/Core/Opt/Simplify/Iteration.hs | 6 | ||||
| -rw-r--r-- | compiler/GHC/Core/TyCo/FVs.hs | 65 | ||||
| -rw-r--r-- | compiler/GHC/Core/TyCo/Rep.hs | 9 | ||||
| -rw-r--r-- | compiler/GHC/Core/TyCon.hs | 62 | ||||
| -rw-r--r-- | compiler/GHC/Core/Type.hs | 72 | ||||
| -rw-r--r-- | compiler/GHC/Core/Type.hs-boot | 3 | ||||
| -rw-r--r-- | compiler/GHC/Data/Bag.hs | 13 | ||||
| -rw-r--r-- | compiler/GHC/Data/Maybe.hs | 3 | ||||
| -rw-r--r-- | compiler/GHC/Hs/Expr.hs | 2 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Errors.hs | 85 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Errors/Ppr.hs | 10 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Solver.hs | 371 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Solver/Equality.hs | 864 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Solver/InertSet.hs | 35 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Solver/Monad.hs | 437 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Types/Constraint.hs | 180 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Utils/Concrete.hs | 10 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Utils/TcMType.hs | 31 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Utils/TcType.hs | 16 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Utils/Unify.hs | 952 |
20 files changed, 2061 insertions, 1165 deletions
diff --git a/compiler/GHC/Core/Opt/Simplify/Iteration.hs b/compiler/GHC/Core/Opt/Simplify/Iteration.hs index ae667676d6..1ecfa632e1 100644 --- a/compiler/GHC/Core/Opt/Simplify/Iteration.hs +++ b/compiler/GHC/Core/Opt/Simplify/Iteration.hs @@ -597,9 +597,9 @@ tryCastWorkerWrapper env bind_cxt old_bndr occ_info bndr (Cast rhs co) -- a DFunUnfolding in mk_worker_unfolding , not (exprIsTrivial rhs) -- Not x = y |> co; Wrinkle 1 , not (hasInlineUnfolding info) -- Not INLINE things: Wrinkle 4 - , isConcrete (typeKind work_ty) -- Don't peel off a cast if doing so would - -- lose the underlying runtime representation. - -- See Note [Preserve RuntimeRep info in cast w/w] + , isConcreteType (typeKind work_ty) -- Don't peel off a cast if doing so would + -- lose the underlying runtime representation. + -- See Note [Preserve RuntimeRep info in cast w/w] , not (isOpaquePragma (idInlinePragma old_bndr)) -- Not for OPAQUE bindings -- See Note [OPAQUE pragma] = do { uniq <- getUniqueM diff --git a/compiler/GHC/Core/TyCo/FVs.hs b/compiler/GHC/Core/TyCo/FVs.hs index 689503ef89..aa9c04c46b 100644 --- a/compiler/GHC/Core/TyCo/FVs.hs +++ b/compiler/GHC/Core/TyCo/FVs.hs @@ -1,4 +1,4 @@ - +{-# LANGUAGE MultiWayIf #-} module GHC.Core.TyCo.FVs ( shallowTyCoVarsOfType, shallowTyCoVarsOfTypes, @@ -23,7 +23,7 @@ module GHC.Core.TyCo.FVs almostDevoidCoVarOfCo, -- Injective free vars - injectiveVarsOfType, injectiveVarsOfTypes, + injectiveVarsOfType, injectiveVarsOfTypes, isInjectiveInType, invisibleVarsOfType, invisibleVarsOfTypes, -- Any and No Free vars @@ -53,7 +53,7 @@ module GHC.Core.TyCo.FVs import GHC.Prelude -import {-# SOURCE #-} GHC.Core.Type( partitionInvisibleTypes, coreView ) +import {-# SOURCE #-} GHC.Core.Type( partitionInvisibleTypes, coreView, rewriterView ) import {-# SOURCE #-} GHC.Core.Coercion( coercionLKind ) import GHC.Builtin.Types.Prim( funTyFlagTyCon ) @@ -806,6 +806,28 @@ visVarsOfTypes = foldMap visVarsOfType * * ********************************************************************* -} +isInjectiveInType :: TyVar -> Type -> Bool +-- True <=> tv /definitely/ appears injectively in ty +-- A bit more efficient that (tv `elemVarSet` injectiveTyVarsOfType ty) +-- Ignore occurence in coercions, and even in injective positions of +-- type families. +isInjectiveInType tv ty + = go ty + where + go ty | Just ty' <- rewriterView ty = go ty' + go (TyVarTy tv') = tv' == tv + go (AppTy f a) = go f || go a + go (FunTy _ w ty1 ty2) = go w || go ty1 || go ty2 + go (TyConApp tc tys) = go_tc tc tys + go (ForAllTy (Bndr tv' _) ty) = go (tyVarKind tv') + || (tv /= tv' && go ty) + go LitTy{} = False + go (CastTy ty _) = go ty + go CoercionTy{} = False + + go_tc tc tys | isTypeFamilyTyCon tc = False + | otherwise = any go tys + -- | Returns the free variables of a 'Type' that are in injective positions. -- Specifically, it finds the free variables while: -- @@ -836,24 +858,29 @@ injectiveVarsOfType :: Bool -- ^ Should we look under injective type families? -> Type -> FV injectiveVarsOfType look_under_tfs = 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 _ w ty1 ty2) = go w `unionFV` go ty1 `unionFV` go ty2 - go (TyConApp tc tys) = - case tyConInjectivityInfo tc of - Injective inj - | look_under_tfs || not (isTypeFamilyTyCon tc) - -> mapUnionFV go $ - filterByList (inj ++ repeat True) tys + go ty | Just ty' <- rewriterView ty = go ty' + go (TyVarTy v) = unitFV v `unionFV` go (tyVarKind v) + go (AppTy f a) = go f `unionFV` go a + go (FunTy _ w ty1 ty2) = go w `unionFV` go ty1 `unionFV` go ty2 + go (TyConApp tc tys) = go_tc tc tys + go (ForAllTy (Bndr tv _) ty) = go (tyVarKind tv) `unionFV` delFV tv (go ty) + go LitTy{} = emptyFV + go (CastTy ty _) = go ty + go CoercionTy{} = emptyFV + + go_tc tc tys + | isTypeFamilyTyCon tc + = if | look_under_tfs + , Injective flags <- tyConInjectivityInfo tc + -> mapUnionFV go $ + filterByList (flags ++ repeat True) tys -- Oversaturated arguments to a tycon are -- always injective, hence the repeat True - _ -> emptyFV - go (ForAllTy (Bndr tv _) ty) = go (tyVarKind tv) `unionFV` delFV tv (go ty) - go LitTy{} = emptyFV - go (CastTy ty _) = go ty - go CoercionTy{} = emptyFV + | otherwise -- No injectivity info for this type family + -> emptyFV + + | otherwise -- Data type, injective in all positions + = mapUnionFV go tys -- | Returns the free variables of a 'Type' that are in injective positions. -- Specifically, it finds the free variables while: diff --git a/compiler/GHC/Core/TyCo/Rep.hs b/compiler/GHC/Core/TyCo/Rep.hs index c90ff3b3c9..8417ded123 100644 --- a/compiler/GHC/Core/TyCo/Rep.hs +++ b/compiler/GHC/Core/TyCo/Rep.hs @@ -61,7 +61,7 @@ module GHC.Core.TyCo.Rep ( TyCoFolder(..), foldTyCo, noView, -- * Sizes - typeSize, coercionSize, provSize, + typeSize, typesSize, coercionSize, provSize, -- * Multiplicities Scaled(..), scaledMult, scaledThing, mapScaledType, Mult @@ -1786,15 +1786,20 @@ noView _ = Nothing -- function is used only in reporting, not decision-making. typeSize :: Type -> Int +-- The size of the syntax tree of a type. No special treatment +-- for type synonyms or type families. typeSize (LitTy {}) = 1 typeSize (TyVarTy {}) = 1 typeSize (AppTy t1 t2) = typeSize t1 + typeSize t2 typeSize (FunTy _ _ t1 t2) = typeSize t1 + typeSize t2 typeSize (ForAllTy (Bndr tv _) t) = typeSize (varType tv) + typeSize t -typeSize (TyConApp _ ts) = 1 + sum (map typeSize ts) +typeSize (TyConApp _ ts) = 1 + typesSize ts typeSize (CastTy ty co) = typeSize ty + coercionSize co typeSize (CoercionTy co) = coercionSize co +typesSize :: [Type] -> Int +typesSize tys = foldr ((+) . typeSize) 0 tys + coercionSize :: Coercion -> Int coercionSize (Refl ty) = typeSize ty coercionSize (GRefl _ ty MRefl) = typeSize ty diff --git a/compiler/GHC/Core/TyCon.hs b/compiler/GHC/Core/TyCon.hs index d06565deec..01197061bb 100644 --- a/compiler/GHC/Core/TyCon.hs +++ b/compiler/GHC/Core/TyCon.hs @@ -833,11 +833,17 @@ data TyConDetails = -- any type synonym families (data families -- are fine), again after expanding any -- nested synonyms - synIsForgetful :: Bool -- True <= at least one argument is not mentioned + + synIsForgetful :: Bool, -- True <= at least one argument is not mentioned -- in the RHS (or is mentioned only under -- forgetful synonyms) -- Test is conservative, so True does not guarantee - -- forgetfulness. + -- forgetfulness. False conveys definite information + -- (definitely not forgetful); True is always safe. + + synIsConcrete :: Bool -- True <= If 'tys' are concrete then the expansion + -- of (S tys) is definitely concrete + -- But False is always safe } -- | Represents families (both type and data) @@ -1873,13 +1879,17 @@ mkPrimTyCon name binders res_kind roles -- | Create a type synonym 'TyCon' mkSynonymTyCon :: Name -> [TyConBinder] -> Kind -- ^ /result/ kind - -> [Role] -> Type -> Bool -> Bool -> Bool -> TyCon -mkSynonymTyCon name binders res_kind roles rhs is_tau is_fam_free is_forgetful + -> [Role] -> Type + -> Bool -> Bool -> Bool -> Bool + -> TyCon +mkSynonymTyCon name binders res_kind roles rhs is_tau + is_fam_free is_forgetful is_concrete = mkTyCon name binders res_kind roles $ SynonymTyCon { synTcRhs = rhs , synIsTau = is_tau , synIsFamFree = is_fam_free - , synIsForgetful = is_forgetful } + , synIsForgetful = is_forgetful + , synIsConcrete = is_concrete } -- | Create a type family 'TyCon' mkFamilyTyCon :: Name -> [TyConBinder] -> Kind -- ^ /result/ kind @@ -1976,11 +1986,10 @@ isInjectiveTyCon (TyCon { tyConDetails = details }) role where go _ Phantom = True -- Vacuously; (t1 ~P t2) holds for all t1, t2! go (AlgTyCon {}) Nominal = True - go (AlgTyCon {algTcRhs = rhs}) Representational - = isGenInjAlgRhs rhs + go (AlgTyCon {algTcRhs = rhs}) Representational = isGenInjAlgRhs rhs go (SynonymTyCon {}) _ = False go (FamilyTyCon { famTcFlav = DataFamilyTyCon _ }) - Nominal = True + Nominal = True go (FamilyTyCon { famTcInj = Injective inj }) Nominal = and inj go (FamilyTyCon {}) _ = False go (PrimTyCon {}) _ = True @@ -1995,6 +2004,10 @@ isInjectiveTyCon (TyCon { tyConDetails = details }) role -- (where r is the role passed in): -- If (T tys ~r t), then (t's head ~r T). -- See also Note [Decomposing TyConApp equalities] in "GHC.Tc.Solver.Canonical" +-- +-- NB: at Nominal role, isGenerativeTyCon is simple: +-- isGenerativeTyCon tc Nominal +-- = not (isTypeFamilyTyCon tc || isSynonymTyCon tc) isGenerativeTyCon :: TyCon -> Role -> Bool isGenerativeTyCon tc@(TyCon { tyConDetails = details }) role = go role details @@ -2348,28 +2361,23 @@ tcHasFixedRuntimeRep tc@(TyCon { tyConDetails = details }) | TcTyCon{} <- details = False | PromotedDataCon{} <- details = pprPanic "tcHasFixedRuntimeRep datacon" (ppr tc) --- | Is this 'TyCon' concrete (i.e. not a synonym/type family)? --- +-- | Is this 'TyCon' concrete? +-- More specifically, if 'tys' are all concrete, is (T tys) concrete? +-- (for synonyms this requires us to look at the RHS) -- Used for representation polymorphism checks. +-- See Note [Concrete types] in GHC.Tc.Utils.Concrete isConcreteTyCon :: TyCon -> Bool -isConcreteTyCon = isConcreteTyConFlavour . tyConFlavour +isConcreteTyCon tc@(TyCon { tyConDetails = details }) + = case details of + AlgTyCon {} -> True -- Includes AbstractTyCon + PrimTyCon {} -> True + PromotedDataCon {} -> True + FamilyTyCon {} -> False --- | Is this 'TyConFlavour' concrete (i.e. not a synonym/type family)? --- --- Used for representation polymorphism checks. -isConcreteTyConFlavour :: TyConFlavour tc -> Bool -isConcreteTyConFlavour = \case - ClassFlavour -> True - TupleFlavour {} -> True - SumFlavour -> True - DataTypeFlavour -> True - NewtypeFlavour -> True - AbstractTypeFlavour -> True -- See Note [Concrete types] in GHC.Tc.Utils.Concrete - OpenFamilyFlavour {} -> False - ClosedTypeFamilyFlavour -> False - TypeSynonymFlavour -> False - BuiltInTypeFlavour -> True - PromotedDataConFlavour -> True + SynonymTyCon { synIsConcrete = is_conc } -> is_conc + + TcTyCon {} -> pprPanic "isConcreteTyCon" (ppr tc) + -- isConcreteTyCon is only used on "real" tycons {- ----------------------------------------------- diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs index 7474630c83..40fa1ea2df 100644 --- a/compiler/GHC/Core/Type.hs +++ b/compiler/GHC/Core/Type.hs @@ -184,7 +184,7 @@ module GHC.Core.Type ( seqType, seqTypes, -- * Other views onto Types - coreView, + coreView, coreFullView, rewriterView, tyConsOfType, @@ -233,7 +233,7 @@ module GHC.Core.Type ( -- * Kinds isTYPEorCONSTRAINT, - isConcrete, isFixedRuntimeRepKind, + isConcreteType, isFixedRuntimeRepKind, ) where import GHC.Prelude @@ -361,6 +361,19 @@ import GHC.Data.Maybe ( orElse, isJust ) ************************************************************************ -} +rewriterView :: Type -> Maybe Type +-- Unwrap a type synonym only when either: +-- The type synonym is forgetful, or +-- the type synonym mentions a type family in its expansion +-- See Note [Rewriting synonyms] +{-# INLINE rewriterView #-} +rewriterView (TyConApp tc tys) + | isTypeSynonymTyCon tc + , isForgetfulSynTyCon tc || not (isFamFreeTyCon tc) + = expandSynTyConApp_maybe tc tys +rewriterView _other + = Nothing + coreView :: Type -> Maybe Type -- ^ This function strips off the /top layer only/ of a type synonym -- application (if any) its underlying representation type. @@ -402,7 +415,11 @@ expandSynTyConApp_maybe :: TyCon -> [Type] -> Maybe Type expandSynTyConApp_maybe tc arg_tys | Just (tvs, rhs) <- synTyConDefn_maybe tc , arg_tys `saturates` tyConArity tc - = Just (expand_syn tvs rhs arg_tys) + = Just $! (expand_syn tvs rhs arg_tys) + -- Why strict application? Because every client of this function will evaluat + -- that (expand_syn ...) thunk, so it's more efficient not to build a thunk. + -- Mind you, this function is always INLINEd, so the client context is probably + -- enough to avoid thunk construction and so the $! is just belt-and-braces. | otherwise = Nothing @@ -2204,15 +2221,28 @@ buildSynTyCon :: Name -> [KnotTied TyConBinder] -> Kind -- ^ /result/ kind -- This function is here because here is where we have -- isFamFree and isTauTy buildSynTyCon name binders res_kind roles rhs - = mkSynonymTyCon name binders res_kind roles rhs is_tau is_fam_free is_forgetful + = mkSynonymTyCon name binders res_kind roles rhs + is_tau is_fam_free is_forgetful is_concrete where is_tau = isTauTy rhs is_fam_free = isFamFreeTy rhs - is_forgetful = any (not . (`elemVarSet` tyCoVarsOfType rhs) . binderVar) binders || - uniqSetAny isForgetfulSynTyCon (tyConsOfType rhs) - -- NB: This is allowed to be conservative, returning True more often + is_concrete = uniqSetAll isConcreteTyCon rhs_tycons + -- NB: is_concrete is allowed to be conservative, returning False + -- more often than it could. e.g. + -- type S a b = b + -- type family F a + -- type T a = S (F a) a + -- We will mark T as not-concrete, even though (since S ignore its first + -- argument, it could be marked concrete. + + is_forgetful = not (all ((`elemVarSet` rhs_tyvars) . binderVar) binders) || + uniqSetAny isForgetfulSynTyCon rhs_tycons + -- NB: is_forgetful is allowed to be conservative, returning True more often -- than it should. See comments on GHC.Core.TyCon.isForgetfulSynTyCon + rhs_tycons = tyConsOfType rhs + rhs_tyvars = tyCoVarsOfType rhs + {- ************************************************************************ * * @@ -2750,29 +2780,26 @@ argsHaveFixedRuntimeRep ty (bndrs, _) = splitPiTys ty -- | Checks that a kind of the form 'Type', 'Constraint' --- or @'TYPE r@ is concrete. See 'isConcrete'. +-- or @'TYPE r@ is concrete. See 'isConcreteType'. -- -- __Precondition:__ The type has kind `TYPE blah` or `CONSTRAINT blah` isFixedRuntimeRepKind :: HasDebugCallStack => Kind -> Bool isFixedRuntimeRepKind k = assertPpr (isTYPEorCONSTRAINT k) (ppr k) $ -- the isLiftedTypeKind check is necessary b/c of Constraint - isConcrete k + isConcreteType k -- | Tests whether the given type is concrete, i.e. it -- whether it consists only of concrete type constructors, -- concrete type variables, and applications. -- -- See Note [Concrete types] in GHC.Tc.Utils.Concrete. -isConcrete :: Type -> Bool -isConcrete = go +isConcreteType :: Type -> Bool +isConcreteType = go where - go ty | Just ty' <- coreView ty = go ty' go (TyVarTy tv) = isConcreteTyVar tv go (AppTy ty1 ty2) = go ty1 && go ty2 - go (TyConApp tc tys) - | isConcreteTyCon tc = all go tys - | otherwise = False + go (TyConApp tc tys) = go_tc tc tys go ForAllTy{} = False go (FunTy _ w t1 t2) = go w && go (typeKind t1) && go t1 @@ -2781,6 +2808,21 @@ isConcrete = go go CastTy{} = False go CoercionTy{} = False + go_tc tc tys + | isForgetfulSynTyCon tc -- E.g. type S a = Int + -- Then (S x) is concrete even if x isn't + , Just ty' <- expandSynTyConApp_maybe tc tys + = go ty' + + -- Apart from forgetful synonyms, isConcreteTyCon + -- is enough; no need to expand. This is good for e.g + -- type LiftedRep = BoxedRep Lifted + | isConcreteTyCon tc + = all go tys + + | otherwise -- E.g. type families + = False + {- %************************************************************************ diff --git a/compiler/GHC/Core/Type.hs-boot b/compiler/GHC/Core/Type.hs-boot index 7b14a22fc1..b4cf5d8a22 100644 --- a/compiler/GHC/Core/Type.hs-boot +++ b/compiler/GHC/Core/Type.hs-boot @@ -21,7 +21,8 @@ piResultTy :: HasDebugCallStack => Type -> Type -> Type typeKind :: HasDebugCallStack => Type -> Type typeTypeOrConstraint :: HasDebugCallStack => Type -> TypeOrConstraint -coreView :: Type -> Maybe Type +coreView :: Type -> Maybe Type +rewriterView :: Type -> Maybe Type isRuntimeRepTy :: Type -> Bool isLevityTy :: Type -> Bool isMultiplicityTy :: Type -> Bool diff --git a/compiler/GHC/Data/Bag.hs b/compiler/GHC/Data/Bag.hs index 5ace42ba13..a9b8a669de 100644 --- a/compiler/GHC/Data/Bag.hs +++ b/compiler/GHC/Data/Bag.hs @@ -19,7 +19,7 @@ module GHC.Data.Bag ( isEmptyBag, isSingletonBag, consBag, snocBag, anyBag, allBag, listToBag, nonEmptyToBag, bagToList, headMaybe, mapAccumBagL, concatMapBag, concatMapBagPair, mapMaybeBag, unzipBag, - mapBagM, mapBagM_, + mapBagM, mapBagM_, lookupBag, flatMapBagM, flatMapBagPairM, mapAndUnzipBagM, mapAccumBagLM, anyBagM, filterBagM @@ -38,6 +38,7 @@ import Data.List ( partition, mapAccumL ) import Data.List.NonEmpty ( NonEmpty(..) ) import qualified Data.List.NonEmpty as NE import qualified Data.Semigroup ( (<>) ) +import Control.Applicative( Alternative( (<|>) ) ) infixr 3 `consBag` infixl 3 `snocBag` @@ -115,6 +116,16 @@ filterBagM pred (ListBag vs) = do sat <- filterM pred (toList vs) return (listToBag sat) +lookupBag :: Eq a => a -> Bag (a,b) -> Maybe b +lookupBag _ EmptyBag = Nothing +lookupBag k (UnitBag kv) = lookup_one k kv +lookupBag k (TwoBags b1 b2) = lookupBag k b1 <|> lookupBag k b2 +lookupBag k (ListBag xs) = foldr ((<|>) . lookup_one k) Nothing xs + +lookup_one :: Eq a => a -> (a,b) -> Maybe b +lookup_one k (k',v) | k==k' = Just v + | otherwise = Nothing + allBag :: (a -> Bool) -> Bag a -> Bool allBag _ EmptyBag = True allBag p (UnitBag v) = p v diff --git a/compiler/GHC/Data/Maybe.hs b/compiler/GHC/Data/Maybe.hs index 6e68ef7d0a..1e8424c0a4 100644 --- a/compiler/GHC/Data/Maybe.hs +++ b/compiler/GHC/Data/Maybe.hs @@ -35,6 +35,7 @@ import Data.Maybe import Data.Foldable ( foldlM, for_ ) import GHC.Utils.Misc (HasCallStack) import Data.List.NonEmpty ( NonEmpty ) +import Control.Applicative( Alternative( (<|>) ) ) infixr 4 `orElse` @@ -47,7 +48,7 @@ infixr 4 `orElse` -} firstJust :: Maybe a -> Maybe a -> Maybe a -firstJust a b = firstJusts [a, b] +firstJust = (<|>) -- | Takes a list of @Maybes@ and returns the first @Just@ if there is one, or -- @Nothing@ otherwise. diff --git a/compiler/GHC/Hs/Expr.hs b/compiler/GHC/Hs/Expr.hs index 4a8abe8404..be7af5002a 100644 --- a/compiler/GHC/Hs/Expr.hs +++ b/compiler/GHC/Hs/Expr.hs @@ -893,12 +893,14 @@ isAtomicHsExpr (XExpr x) | GhcTc <- ghcPass @p = go_x_tc x | GhcRn <- ghcPass @p = go_x_rn x where + go_x_tc :: XXExprGhcTc -> Bool go_x_tc (WrapExpr (HsWrap _ e)) = isAtomicHsExpr e go_x_tc (ExpansionExpr (HsExpanded a _)) = isAtomicHsExpr a go_x_tc (ConLikeTc {}) = True go_x_tc (HsTick {}) = False go_x_tc (HsBinTick {}) = False + go_x_rn :: HsExpansion (HsExpr GhcRn) (HsExpr GhcRn) -> Bool go_x_rn (HsExpanded a _) = isAtomicHsExpr a isAtomicHsExpr _ = False diff --git a/compiler/GHC/Tc/Errors.hs b/compiler/GHC/Tc/Errors.hs index 60f87f2bc7..cb23c835dc 100644 --- a/compiler/GHC/Tc/Errors.hs +++ b/compiler/GHC/Tc/Errors.hs @@ -32,7 +32,6 @@ import GHC.Tc.Types.Constraint import GHC.Tc.Utils.TcMType import GHC.Tc.Utils.Env( tcInitTidyEnv ) import GHC.Tc.Utils.TcType -import GHC.Tc.Utils.Unify ( checkTyVarEq ) import GHC.Tc.Types.Origin import GHC.Tc.Types.Evidence import GHC.Tc.Types.EvTerm @@ -1532,13 +1531,9 @@ any more. So we don't assert that it is. -- Don't have multiple equality errors from the same location -- E.g. (Int,Bool) ~ (Bool,Int) one error will do! mkEqErr :: SolverReportErrCtxt -> NonEmpty ErrorItem -> TcM SolverReport -mkEqErr ctxt items@(item:|_) - | item:_ <- filter (not . ei_suppress) (toList items) - = mkEqErr1 ctxt item - - | otherwise -- they're all suppressed. still need an error message - -- for -fdefer-type-errors though - = mkEqErr1 ctxt item +mkEqErr ctxt items + | item1 :| _ <- tryFilter (not . ei_suppress) items + = mkEqErr1 ctxt item1 mkEqErr1 :: SolverReportErrCtxt -> ErrorItem -> TcM SolverReport mkEqErr1 ctxt item -- Wanted only @@ -1601,12 +1596,14 @@ mkEqErr_help :: SolverReportErrCtxt mkEqErr_help ctxt item ty1 ty2 | Just casted_tv1 <- getCastedTyVar_maybe ty1 = mkTyVarEqErr ctxt item casted_tv1 ty2 + + -- ToDo: explain.. Cf T2627b Dual (Dual a) ~ a | Just casted_tv2 <- getCastedTyVar_maybe ty2 = mkTyVarEqErr ctxt item casted_tv2 ty1 + | otherwise - = do - err <- reportEqErr ctxt item ty1 ty2 - return (err, noHints) + = do { err <- reportEqErr ctxt item ty1 ty2 + ; return (err, noHints) } reportEqErr :: SolverReportErrCtxt -> ErrorItem @@ -1614,16 +1611,16 @@ reportEqErr :: SolverReportErrCtxt -> TcM TcSolverReportMsg reportEqErr ctxt item ty1 ty2 = do - mb_coercible_info <- - if errorItemEqRel item == ReprEq - then coercible_msg ty1 ty2 - else return Nothing - return $ - Mismatch - { mismatchMsg = mismatch - , mismatchTyVarInfo = Nothing - , mismatchAmbiguityInfo = eqInfos - , mismatchCoercibleInfo = mb_coercible_info } + mb_coercible_info <- if errorItemEqRel item == ReprEq + then coercible_msg ty1 ty2 + else return Nothing + tv_info <- case getTyVar_maybe ty2 of + Nothing -> return Nothing + Just tv2 -> Just <$> extraTyVarEqInfo (tv2, Nothing) ty1 + return $ Mismatch { mismatchMsg = mismatch + , mismatchTyVarInfo = tv_info + , mismatchAmbiguityInfo = eqInfos + , mismatchCoercibleInfo = mb_coercible_info } where mismatch = misMatchOrCND False ctxt item ty1 ty2 eqInfos = eqInfoMsgs ty1 ty2 @@ -1653,8 +1650,8 @@ mkTyVarEqErr' ctxt item (tv1, co1) ty2 (_, infos) <- zonkTidyFRRInfos (cec_tidy ctxt) [frr_info] return (FixedRuntimeRepError infos, []) - -- Impredicativity is a simple error to understand; try it before - -- anything more complicated. + -- Impredicativity is a simple error to understand; + -- try it before anything more complicated. | check_eq_result `cterHasProblem` cteImpredicative = do tyvar_eq_info <- extraTyVarEqInfo (tv1, Nothing) ty2 @@ -1674,6 +1671,12 @@ mkTyVarEqErr' ctxt item (tv1, co1) ty2 -- to be helpful since this is just an unimplemented feature. return (main_msg, []) + -- Incompatible kinds + -- This is wrinkle (4) in Note [Equalities with incompatible kinds] in + -- GHC.Tc.Solver.Canonical + | hasCoercionHoleCo co1 || hasCoercionHoleTy ty2 + = return (mkBlockedEqErr item, []) + | isSkolemTyVar tv1 -- ty2 won't be a meta-tyvar; we would have -- swapped in Solver.Canonical.canEqTyVarHomo || isTyVarTyVar tv1 && not (isTyVarTy ty2) @@ -1681,20 +1684,21 @@ mkTyVarEqErr' ctxt item (tv1, co1) ty2 -- The cases below don't really apply to ReprEq (except occurs check) = do tv_extra <- extraTyVarEqInfo (tv1, Nothing) ty2 - reason <- - if errorItemEqRel item == ReprEq - then RepresentationalEq tv_extra <$> coercible_msg ty1 ty2 - else return $ DifferentTyVars tv_extra - let main_msg = - CannotUnifyVariable - { mismatchMsg = headline_msg - , cannotUnifyReason = reason } + reason <- if errorItemEqRel item == ReprEq + then RepresentationalEq tv_extra <$> coercible_msg ty1 ty2 + else return $ DifferentTyVars tv_extra + let main_msg = CannotUnifyVariable + { mismatchMsg = headline_msg + , cannotUnifyReason = reason } return (main_msg, add_sig) - | cterHasOccursCheck check_eq_result + | tv1 `elemVarSet` tyCoVarsOfType ty2 -- We report an "occurs check" even for a ~ F t a, where F is a type -- function; it's not insoluble (because in principle F could reduce) -- but we have certainly been unable to solve it + -- + -- Use tyCoVarsOfType because it might have begun as the canonical + -- constraint (Dual (Dual a)) ~ a, and been swizzled by mkEqnErr_help = let ambiguity_infos = eqInfoMsgs ty1 ty2 interesting_tyvars = filter (not . noFreeVarsOfType . tyVarKind) $ @@ -1713,11 +1717,6 @@ mkTyVarEqErr' ctxt item (tv1, co1) ty2 in return (main_msg, []) - -- This is wrinkle (4) in Note [Equalities with incompatible kinds] in - -- GHC.Tc.Solver.Canonical - | hasCoercionHoleCo co1 || hasCoercionHoleTy ty2 - = return (mkBlockedEqErr item, []) - -- If the immediately-enclosing implication has 'tv' a skolem, and -- we know by now its an InferSkol kind of skolem, then presumably -- it started life as a TyVarTv, else it'd have been unified, given @@ -1765,9 +1764,8 @@ mkTyVarEqErr' ctxt item (tv1, co1) ty2 return (msg, add_sig) | otherwise - = do - err <- reportEqErr ctxt item (mkTyVarTy tv1) ty2 - return (err, []) + = do { err <- reportEqErr ctxt item (mkTyVarTy tv1) ty2 + ; return (err, []) } -- This *can* happen (#6123) -- Consider an ambiguous top-level constraint (a ~ F a) -- Not an occurs check, because F is a type function. @@ -1781,7 +1779,7 @@ mkTyVarEqErr' ctxt item (tv1, co1) ty2 -- there is an error is not sufficient. See #21430. mb_concrete_reason | Just frr_orig <- isConcreteTyVar_maybe tv1 - , not (isConcrete ty2) + , not (isConcreteType ty2) = Just $ frr_reason frr_orig tv1 ty2 | Just (tv2, frr_orig) <- isConcreteTyVarTy_maybe ty2 , not (isConcreteTyVar tv1) @@ -1799,10 +1797,7 @@ mkTyVarEqErr' ctxt item (tv1, co1) ty2 check_eq_result = case ei_m_reason item of Just (NonCanonicalReason result) -> result - _ -> checkTyVarEq tv1 ty2 - -- in T2627b, we report an error for F (F a0) ~ a0. Note that the type - -- variable is on the right, so we don't get useful info for the CIrredCan, - -- and have to compute the result of checkTyVarEq here. + _ -> cteOK insoluble_occurs_check = check_eq_result `cterHasProblem` cteInsolubleOccurs diff --git a/compiler/GHC/Tc/Errors/Ppr.hs b/compiler/GHC/Tc/Errors/Ppr.hs index f4024fe68f..d4e0ba15a1 100644 --- a/compiler/GHC/Tc/Errors/Ppr.hs +++ b/compiler/GHC/Tc/Errors/Ppr.hs @@ -3366,10 +3366,10 @@ pprTcSolverReportMsg ctxt , mismatchTyVarInfo = tv_info , mismatchAmbiguityInfo = ambig_infos , mismatchCoercibleInfo = coercible_info }) - = hang (pprMismatchMsg ctxt mismatch_msg) - 2 (vcat ( maybe empty (pprTyVarInfo ctxt) tv_info - : maybe empty pprCoercibleMsg coercible_info - : map pprAmbiguityInfo ambig_infos )) + = vcat ([ pprMismatchMsg ctxt mismatch_msg + , maybe empty (pprTyVarInfo ctxt) tv_info + , maybe empty pprCoercibleMsg coercible_info ] + ++ (map pprAmbiguityInfo ambig_infos)) pprTcSolverReportMsg _ (FixedRuntimeRepError frr_origs) = vcat (map make_msg frr_origs) where @@ -3418,7 +3418,7 @@ pprTcSolverReportMsg _ (FixedRuntimeRepError frr_origs) = CastTy inner_ty _ -- A confusing cast is one that is responsible -- for a representation-polymorphism error. - -> isConcrete (typeKind inner_ty) + -> isConcreteType (typeKind inner_ty) _ -> False type_printout :: Type -> SDoc diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs index b46b994e2f..244817c4a1 100644 --- a/compiler/GHC/Tc/Solver.hs +++ b/compiler/GHC/Tc/Solver.hs @@ -1447,58 +1447,6 @@ If the monomorphism restriction does not apply, then we quantify as follows: qtvs. We have to zonk the constraints first, so they "see" the freshly created skolems. -Note [Lift equality constraints when quantifying] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We can't quantify over a constraint (t1 ~# t2) because that isn't a -predicate type; see Note [Types for coercions, predicates, and evidence] -in GHC.Core.TyCo.Rep. - -So we have to 'lift' it to (t1 ~ t2). Similarly (~R#) must be lifted -to Coercible. - -This tiresome lifting is the reason that pick_me (in -pickQuantifiablePreds) returns a Maybe rather than a Bool. - -Note [Inheriting implicit parameters] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider this: - - f x = (x::Int) + ?y - -where f is *not* a top-level binding. -From the RHS of f we'll get the constraint (?y::Int). -There are two types we might infer for f: - - f :: Int -> Int - -(so we get ?y from the context of f's definition), or - - f :: (?y::Int) => Int -> Int - -At first you might think the first was better, because then -?y behaves like a free variable of the definition, rather than -having to be passed at each call site. But of course, the WHOLE -IDEA is that ?y should be passed at each call site (that's what -dynamic binding means) so we'd better infer the second. - -BOTTOM LINE: when *inferring types* you must quantify over implicit -parameters, *even if* they don't mention the bound type variables. -Reason: because implicit parameters, uniquely, have local instance -declarations. See pickQuantifiablePreds. - -Note [Quantifying over equality constraints] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Should we quantify over an equality constraint (s ~ t)? In general, we don't. -Doing so may simply postpone a type error from the function definition site to -its call site. (At worst, imagine (Int ~ Bool)). - -However, consider this - forall a. (F [a] ~ Int) => blah -Should we quantify over the (F [a] ~ Int). Perhaps yes, because at the call -site we will know 'a', and perhaps we have instance F [Bool] = Int. -So we *do* quantify over a type-family equality where the arguments mention -the quantified variables. - Note [Unconditionally resimplify constraints when quantifying] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ During quantification (in defaultTyVarsAndSimplify, specifically), we re-invoke @@ -1571,26 +1519,6 @@ a unification between beta1 and beta2, and all will be well. The key step is that this simplification happens *after* the call to approximateWC in simplifyInfer. -Note [Do not quantify over constraints that determine a variable] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider (typecheck/should_compile/tc231), where we're trying to infer -the type of a top-level declaration. We have - class Zork s a b | a -> b -and the candidate constraint at the end of simplifyInfer is - [W] Zork alpha (Z [Char]) beta -We definitely do want to quantify over alpha (which is mentioned in -the tau-type). But we do *not* want to quantify over beta: it is -determined by the functional dependency on Zork: note that the second -argument to Zork in the Wanted is a variable-free Z [Char]. - -The question here: do we want to quantify over the constraint? Definitely not. -Since we're not quantifying over beta, GHC has no choice but to zap beta -to Any, and then we infer a type involving (Zork a (Z [Char]) Any => ...). No no no. - -The no_fixed_dependencies check in pickQuantifiablePreds eliminates this -candidate from the pool. Because there are no Zork instances in scope, this -program is rejected. - -} decideQuantification @@ -1606,8 +1534,9 @@ decideQuantification -- See Note [Deciding quantification] decideQuantification skol_info infer_mode rhs_tclvl name_taus psigs candidates = do { -- Step 1: find the mono_tvs - ; (candidates, co_vars) <- decidePromotedTyVars infer_mode - name_taus psigs candidates + ; (candidates, co_vars, mono_tvs0) + <- decidePromotedTyVars infer_mode + name_taus psigs candidates -- Step 2: default any non-mono tyvars, and re-simplify -- This step may do some unification, but result candidates is zonked @@ -1622,10 +1551,7 @@ decideQuantification skol_info infer_mode rhs_tclvl name_taus psigs candidates -- into quantified skolems, so we have to zonk again ; candidates <- TcM.zonkTcTypes candidates ; psig_theta <- TcM.zonkTcTypes (concatMap sig_inst_theta psigs) - ; let min_theta = mkMinimalBySCs id $ -- See Note [Minimize by Superclasses] - pickQuantifiablePreds (mkVarSet qtvs) candidates - - min_psig_theta = mkMinimalBySCs id psig_theta + ; min_theta <- pickQuantifiablePreds (mkVarSet qtvs) mono_tvs0 candidates -- Add psig_theta back in here, even though it's already -- part of candidates, because we always want to quantify over @@ -1635,6 +1561,7 @@ decideQuantification skol_info infer_mode rhs_tclvl name_taus psigs candidates -- It's helpful to use the same "find difference" algorithm here as -- we use in GHC.Tc.Gen.Bind.chooseInferredQuantifiers (#20921) -- See Note [Constraints in partial type signatures] + ; let min_psig_theta = mkMinimalBySCs id psig_theta ; theta <- if null psig_theta then return min_theta -- Fast path for the non-partial-sig case else do { diff <- findInferredDiff min_psig_theta min_theta @@ -1686,7 +1613,7 @@ decidePromotedTyVars :: InferMode -> [(Name,TcType)] -> [TcIdSigInst] -> [PredType] - -> TcM ([PredType], CoVarSet) + -> TcM ([PredType], CoVarSet, TcTyVarSet) -- We are about to generalise over type variables at level N -- Each must be either -- (P) promoted @@ -1705,7 +1632,8 @@ decidePromotedTyVars :: InferMode -- Also return CoVars that appear free in the final quantified types -- we can't quantify over these, and we must make sure they are in scope decidePromotedTyVars infer_mode name_taus psigs candidates - = do { (no_quant, maybe_quant) <- pick infer_mode candidates + = do { tc_lvl <- TcM.getTcLevel + ; (no_quant, maybe_quant) <- pick infer_mode candidates -- If possible, we quantify over partial-sig qtvs, so they are -- not mono. Need to zonk them because they are meta-tyvar TyVarTvs @@ -1717,7 +1645,6 @@ decidePromotedTyVars infer_mode name_taus psigs candidates ; taus <- mapM (TcM.zonkTcType . snd) name_taus - ; tc_lvl <- TcM.getTcLevel ; let psig_tys = mkTyVarTys psig_qtvs ++ psig_theta -- (b) The co_var_tvs are tvs mentioned in the types of covars or @@ -1791,9 +1718,7 @@ decidePromotedTyVars infer_mode name_taus psigs candidates let dia = TcRnMonomorphicBindings (map fst name_taus) diagnosticTc (constrained_tvs `intersectsVarSet` tyCoVarsOfTypes taus) dia - -- Promote the mono_tvs - -- See Note [Promote monomorphic tyvars] - ; traceTc "decidePromotedTyVars: promotion:" (ppr mono_tvs) + -- Promote the mono_tvs: see Note [Promote monomorphic tyvars] ; _ <- promoteTyVarSet mono_tvs ; traceTc "decidePromotedTyVars" $ vcat @@ -1804,23 +1729,23 @@ decidePromotedTyVars infer_mode name_taus psigs candidates , text "mono_tvs =" <+> ppr mono_tvs , text "co_vars =" <+> ppr co_vars ] - ; return (maybe_quant, co_vars) } + ; return (maybe_quant, co_vars, mono_tvs0) } where pick :: InferMode -> [PredType] -> TcM ([PredType], [PredType]) -- Split the candidates into ones we definitely -- won't quantify, and ones that we might - pick NoRestrictions cand = return ([], cand) pick ApplyMR cand = return (cand, []) + pick NoRestrictions cand = return ([], cand) pick EagerDefaulting cand = do { os <- xoptM LangExt.OverloadedStrings ; return (partition (is_int_ct os) cand) } + -- is_int_ct returns True for a constraint we should /not/ quantify -- For EagerDefaulting, do not quantify over -- over any interactive class constraint is_int_ct ovl_strings pred - | Just (cls, _) <- getClassPredTys_maybe pred - = isInteractiveClass ovl_strings cls - | otherwise - = False + = case classifyPredType pred of + ClassPred cls _ -> isInteractiveClass ovl_strings cls + _ -> False ------------------- defaultTyVarsAndSimplify :: TcLevel @@ -1916,23 +1841,23 @@ decideQuantifiedTyVars skol_info name_taus psigs candidates ------------------ -- | When inferring types, should we quantify over a given predicate? --- Generally true of classes; generally false of equality constraints. --- Equality constraints that mention quantified type variables and --- implicit variables complicate the story. See Notes --- [Inheriting implicit parameters] and [Quantifying over equality constraints] +-- See Note [pickQuantifiablePreds] pickQuantifiablePreds :: TyVarSet -- Quantifying over these + -> TcTyVarSet -- These ones are free in the enviroment -> TcThetaType -- Proposed constraints to quantify - -> TcThetaType -- A subset that we can actually quantify + -> TcM TcThetaType -- A subset that we can actually quantify -- This function decides whether a particular constraint should be -- quantified over, given the type variables that are being quantified -pickQuantifiablePreds qtvs theta - = let flex_ctxt = True in -- Quantify over non-tyvar constraints, even without - -- -XFlexibleContexts: see #10608, #10351 - -- flex_ctxt <- xoptM Opt_FlexibleContexts - mapMaybe (pick_me flex_ctxt) theta +pickQuantifiablePreds qtvs mono_tvs0 theta + = do { tc_lvl <- TcM.getTcLevel + ; let is_nested = not (isTopTcLevel tc_lvl) + ; return (mkMinimalBySCs id $ -- See Note [Minimize by Superclasses] + mapMaybe (pick_me is_nested) theta) } where - pick_me flex_ctxt pred + pick_me is_nested pred + | let pred_tvs = tyCoVarsOfType pred + mentions_qtvs = pred_tvs `intersectsVarSet` qtvs = case classifyPredType pred of ClassPred cls tys @@ -1946,37 +1871,35 @@ pickQuantifiablePreds qtvs theta | isIPClass cls -> Just pred -- See Note [Inheriting implicit parameters] - | pick_cls_pred flex_ctxt cls tys + | not mentions_qtvs + -> Nothing -- Don't quantify over predicates that don't + -- mention any of the quantified type variables + + | is_nested -> Just pred - EqPred eq_rel ty1 ty2 - | quantify_equality eq_rel ty1 ty2 - , Just (cls, tys) <- boxEqPred eq_rel ty1 ty2 - -- boxEqPred: See Note [Lift equality constraints when quantifying] - , pick_cls_pred flex_ctxt cls tys - -> Just (mkClassPred cls tys) + -- From here on, we are thinking about top-level defns only - IrredPred ty - | tyCoVarsOfType ty `intersectsVarSet` qtvs + | pred_tvs `subVarSet` (qtvs `unionVarSet` mono_tvs0) + -- See Note [Do not quantify over constraints that determine a variable] -> Just pred - _ -> Nothing + | otherwise + -> Nothing + EqPred eq_rel ty1 ty2 + | mentions_qtvs + , quantify_equality eq_rel ty1 ty2 + , Just (cls, tys) <- boxEqPred eq_rel ty1 ty2 + -- boxEqPred: See Note [Lift equality constraints when quantifying] + -> Just (mkClassPred cls tys) + | otherwise + -> Nothing - pick_cls_pred flex_ctxt cls tys - = tyCoVarsOfTypes tys `intersectsVarSet` qtvs - && (checkValidClsArgs flex_ctxt cls tys) - -- Only quantify over predicates that checkValidType - -- will pass! See #10351. - && (no_fixed_dependencies cls tys) + IrredPred {} | mentions_qtvs -> Just pred + | otherwise -> Nothing - -- See Note [Do not quantify over constraints that determine a variable] - no_fixed_dependencies cls tys - = and [ qtvs `intersectsVarSet` tyCoVarsOfTypes fd_lhs_tys - | fd <- cls_fds - , let (fd_lhs_tys, _) = instFD fd cls_tvs tys ] - where - (cls_tvs, cls_fds) = classTvsFds cls + ForAllPred {} -> Nothing -- See Note [Quantifying over equality constraints] quantify_equality NomEq ty1 ty2 = quant_fun ty1 || quant_fun ty2 @@ -1988,7 +1911,6 @@ pickQuantifiablePreds qtvs theta -> tyCoVarsOfTypes tys `intersectsVarSet` qtvs _ -> False - ------------------ growThetaTyVars :: ThetaType -> TyCoVarSet -> TyCoVarSet -- See Note [growThetaTyVars vs closeWrtFunDeps] @@ -2025,6 +1947,202 @@ so we must promote it! The inferred type is just NB: promoteTyVarSet ignores coercion variables +Note [pickQuantifiablePreds] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +When pickQuantifiablePreds is called we have decided what type +variables to quantify over, `qtvs`. The only quesion is: which of the +unsolved candidate predicates should we quantify over? Call them +`picked_theta`. + +Note that will leave behind a residual implication + forall qtvs. picked_theta => unsolved_constraints +For the members of unsolved_constraints that we select for picked_theta +it is easy to solve, by identity. For the others we just hope that +we can solve them. + +So which of the candidates should we pick to quantify over? In some +situations we distinguish top-level from nested bindings. The point +about nested binding is that + (a) the types may mention type variables free in the environment + (b) all of the call sites are statically visible, reducing the + worries about "spooky action at a distance". + +First, never pick a constraint that doesn't mention any of the quantified +variables `qtvs`. Picking such a constraint essentially moves the solving of +the constraint from this function definition to call sites. But because the +constraint mentions no quantified variables, call sites have no advantage +over the definition site. Well, not quite: there could be new constraints +brought into scope by a pattern-match against a constrained (e.g. GADT) +constructor. Example + + data T a where { T1 :: T1 Bool; ... } + + f :: forall a. a -> T a -> blah + f x t = let g y = x&&y -- This needs a~Bool + in case t of + T1 -> g True + .... + +At g's call site we have `a~Bool`, so we /could/ infer + g :: forall . (a~Bool) => Bool -> Bool -- qtvs = {} + +This is all very contrived, and probably just postponse type errors to +the call site. If that's what you want, write a type signature. + +Actually, implicit parameters is an exception to the "no quantified vars" +rule (see Note [Inheriting implicit parameters]) so we can't actually +simply test this case first. + +Now we consider the different sorts of constraints: + +* For ClassPred constraints: + + * Never pick a CallStack constraint. + See Note [Overview of implicit CallStacks] + + * Always pick an implicit-parameter constraint. + Note [Inheriting implicit parameters] + + * For /top-level/ class constraints see + Note [Do not quantify over constraints that determine a variable] + +* For EqPred constraints see Note [Quantifying over equality constraints] + +* For IrredPred constraints, we allow anything that mentions the quantified + type variables. + +* A ForAllPred should not appear: the candidates come from approximateWC. + +Notice that we do /not/ consult -XFlexibleContexts here. For example, +we allow `pickQuantifiablePreds` to quantify over a constraint like +`Num [a]`; then if we don't have `-XFlexibleContexts` we'll get an +error from `checkValidType` but (critically) it includes the helpful +suggestion of adding `-XFlexibleContexts`. See #10608, #10351. + +Note [Lift equality constraints when quantifying] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We can't quantify over a constraint (t1 ~# t2) because that isn't a +predicate type; see Note [Types for coercions, predicates, and evidence] +in GHC.Core.TyCo.Rep. + +So we have to 'lift' it to (t1 ~ t2). Similarly (~R#) must be lifted +to Coercible. + +This tiresome lifting is the reason that pick_me (in +pickQuantifiablePreds) returns a Maybe rather than a Bool. + +Note [Inheriting implicit parameters] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider this: + + f x = (x::Int) + ?y + +where f is *not* a top-level binding. +From the RHS of f we'll get the constraint (?y::Int). +There are two types we might infer for f: + + f :: Int -> Int + +(so we get ?y from the context of f's definition), or + + f :: (?y::Int) => Int -> Int + +At first you might think the first was better, because then +?y behaves like a free variable of the definition, rather than +having to be passed at each call site. But of course, the WHOLE +IDEA is that ?y should be passed at each call site (that's what +dynamic binding means) so we'd better infer the second. + +BOTTOM LINE: when *inferring types* you must quantify over implicit +parameters, *even if* they don't mention the bound type variables. +Reason: because implicit parameters, uniquely, have local instance +declarations. See pickQuantifiablePreds. + +Note [Quantifying over equality constraints] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Should we quantify over an equality constraint (s ~ t) +in pickQuantifiablePreds? + +* It is always /sound/ to quantify over a constraint -- those + quantified constraints will need to be proved at each call site. + +* We definitely don't want to quantify over (Maybe a ~ Bool), to get + f :: forall a. (Maybe a ~ Bool) => blah + That simply postpones a type error from the function definition site to + its call site. Fortunately we have already filtered out insoluble + constraints: see `definite_error` in `simplifyInfer`. + +* What about (a ~ T alpha b), where we are about to quantify alpha, `a` and + `b` are in-scope skolems, and `T` is a data type. It's pretty unlikely + that this will be soluble at a call site, so we don't quantify over it. + +* What about `(F beta ~ Int)` where we are going to quantify `beta`? + Should we quantify over the (F beta ~ Int), to get + f :: forall b. (F b ~ Int) => blah + Aha! Perhaps yes, because at the call site we will instantiate `b`, and + perhaps we have `instance F Bool = Int`. So we *do* quantify over a + type-family equality where the arguments mention the quantified variables. + +This is all a bit ad-hoc. + +Note [Do not quantify over constraints that determine a variable] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider (typecheck/should_compile/tc231), where we're trying to infer +the type of a top-level declaration. We have + class Zork s a b | a -> b +and the candidate constraint at the end of simplifyInfer is + [W] Zork alpha[1] (Z [Char]) beta[1] +We definitely want to quantify over `alpha` (which is mentioned in the +tau-type). + +But we do *not* want to quantify over `beta`: it is determined by the +functional dependency on Zork: note that the second argument to Zork +in the Wanted is a variable-free `Z [Char]`. Quantifying over it +would be "Henry Ford polymorphism". (Presumably we don't have an +instance in scope that tells us what `beta` actually is.) Instead +we promote `beta[1]` to `beta[0]`, in `decidePromotedTyVars`. + +The question here: do we want to quantify over the constraint, to +give the type + forall a. Zork a (Z [Char]) beta[0] => blah +Definitely not. Since we're not quantifying over beta, it has been +promoted; and then will be zapped to Any in the final zonk. So we end +up with a (perhaps exported) type involving + forall a. Zork a (Z [Char]) Any => blah +No no no. We never want to show the programmer a type with `Any` in it. + +What we really want (to catch the Zork example) is this: +Hence, for a top-level binding, we eliminate the candidate from the +pool, by asking + + Do not quantify over the constraint if it mentions a variable that is + (a) not quantified (i.e. is determined by the type environment), but + (b) do not appear literally in the environment (mono_tvs0)? + +To understand (b) consider + + class C a b where { op :: a -> b -> () } + + mr = 3 -- mr :: alpha + f1 x = op x mr -- f1 :: forall b. b -> (), plus [W] C b alpha + intify = mr + (4 :: Int) + +In `f1` should we quantify over that `(C b alpha)`? Answer: since `alpha` +is free in the type envt, yes we should. After all, if we'd typechecked +`intify` first, we'd have set `alpha := Int`, and /then/ we'd certainly +quantify. The delicate Zork situation applies when beta is completely +unconstrained -- except by the fudep. + +However this subtle reasoning is needed only for /top-level/ declarations. +For /nested/ decls we can see all the calls, so we'll instantiate that +quantifed `Zork a (Z [Char]) beta` constraint at call sites, and either solve +it or not (probably not). We won't be left with a still-callable function +with Any in its type. So for nested definitions we don't make this tricky +test. + +Historical note: we had a different, and more complicated test +before, but it was utterly wrong: #23199. + Note [Quantification and partial signatures] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ When choosing type variables to quantify, the basic plan is to @@ -2257,6 +2375,9 @@ simplifyWantedsTcM wanted solveWanteds :: WantedConstraints -> TcS WantedConstraints solveWanteds wc@(WC { wc_errors = errs }) + | isEmptyWC wc -- Fast path + = return wc + | otherwise = do { cur_lvl <- TcS.getTcLevel ; traceTcS "solveWanteds {" $ vcat [ text "Level =" <+> ppr cur_lvl diff --git a/compiler/GHC/Tc/Solver/Equality.hs b/compiler/GHC/Tc/Solver/Equality.hs index ef2b5945c2..2a76792790 100644 --- a/compiler/GHC/Tc/Solver/Equality.hs +++ b/compiler/GHC/Tc/Solver/Equality.hs @@ -8,17 +8,16 @@ module GHC.Tc.Solver.Equality( import GHC.Prelude -import GHC.Tc.Types.Constraint -import GHC.Tc.Types.Origin -import GHC.Tc.Utils.Unify -import GHC.Tc.Utils.TcType -import GHC.Tc.Utils.TcMType( promoteMetaTyVarTo ) import GHC.Tc.Solver.Rewrite import GHC.Tc.Solver.Monad import GHC.Tc.Solver.Dict( matchLocalInst, chooseInstance ) import GHC.Tc.Solver.InertSet import GHC.Tc.Solver.Types( findFunEqsByTyCon ) import GHC.Tc.Types.Evidence +import GHC.Tc.Types.Constraint +import GHC.Tc.Types.Origin +import GHC.Tc.Utils.Unify +import GHC.Tc.Utils.TcType import GHC.Tc.Instance.Family ( tcTopNormaliseNewTypeTF_maybe ) import GHC.Tc.Instance.FunDeps( FunDepEqn(..) ) @@ -635,8 +634,8 @@ can_eq_newtype_nc ev swapped ty1 ((gres, co1), ty1') ty2 ps_ty2 ; let redn1 = mkReduction co1 ty1' ; new_ev <- rewriteEqEvidence emptyRewriterSet ev' swapped - redn1 - (mkReflRedn Representational ps_ty2) + redn1 (mkReflRedn Representational ps_ty2) + ; can_eq_nc False new_ev ReprEq ty1' ty1' ty2 ps_ty2 } --------- @@ -1375,8 +1374,8 @@ But if w2 is swapped around, to [W] w3 : F beta ~ F a -then we'll kick w1 out of the inert -set (it mentions the LHS of w3). We then rewrite w1 to +then we'll kick w1 out of the inert set (it mentions the LHS of w3). We then +rewrite w1 to [W] w4 : UnF (F a) ~ beta @@ -1498,13 +1497,13 @@ canEqCanLHSHetero ev eq_rel swapped lhs1 ki1 xi2 ki2 -- will have k2 ~ k1, so flip it to k1 ~ k2 NotSwapped -> id --- guaranteed that typeKind lhs == typeKind rhs canEqCanLHSHomo :: CtEvidence -> EqRel -> SwapFlag -> CanEqLHS -- lhs (or, if swapped, rhs) -> TcType -- pretty lhs -> TcType -> TcType -- rhs, pretty rhs -> TcS (StopOrContinue Ct) +-- Guaranteed that typeKind lhs == typeKind rhs canEqCanLHSHomo ev eq_rel swapped lhs1 ps_xi1 xi2 ps_xi2 | (xi2', mco) <- split_cast_ty xi2 , Just lhs2 <- canEqLHS_maybe xi2' @@ -1531,25 +1530,27 @@ canEqCanLHS2 :: CtEvidence -- lhs ~ (rhs |> mco) canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco | lhs1 `eqCanEqLHS` lhs2 -- It must be the case that mco is reflexive - = canEqReflexive ev eq_rel (canEqLHSType lhs1) + = canEqReflexive ev eq_rel lhs1_ty | TyVarLHS tv1 <- lhs1 , TyVarLHS tv2 <- lhs2 - , swapOverTyVars (isGiven ev) tv1 tv2 - = do { traceTcS "canEqLHS2 swapOver" (ppr tv1 $$ ppr tv2 $$ ppr swapped) - ; new_ev <- do_swap - ; canEqCanLHSFinish new_ev eq_rel IsSwapped (TyVarLHS tv2) - (ps_xi1 `mkCastTyMCo` sym_mco) } + = -- See Note [TyVar/TyVar orientation] in GHC.Tc.Utils.Unify + do { traceTcS "canEqLHS2 swapOver" (ppr tv1 $$ ppr tv2 $$ ppr swapped) + ; if swapOverTyVars (isGiven ev) tv1 tv2 + then finish_with_swapping + else finish_without_swapping } - | TyVarLHS tv1 <- lhs1 - , TyFamLHS fun_tc2 fun_args2 <- lhs2 - = canEqTyVarFunEq ev eq_rel swapped tv1 ps_xi1 fun_tc2 fun_args2 ps_xi2 mco + | TyVarLHS {} <- lhs1 + , TyFamLHS {} <- lhs2 + = if put_tyvar_on_lhs + then finish_without_swapping + else finish_with_swapping - | TyFamLHS fun_tc1 fun_args1 <- lhs1 - , TyVarLHS tv2 <- lhs2 - = do { new_ev <- do_swap - ; canEqTyVarFunEq new_ev eq_rel IsSwapped tv2 ps_xi2 - fun_tc1 fun_args1 ps_xi1 sym_mco } + | TyFamLHS {} <- lhs1 + , TyVarLHS {} <- lhs2 + = if put_tyvar_on_lhs + then finish_with_swapping + else finish_without_swapping | TyFamLHS fun_tc1 fun_args1 <- lhs1 , TyFamLHS fun_tc2 fun_args2 <- lhs2 @@ -1599,83 +1600,95 @@ canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco ; let tvs1 = tyCoVarsOfTypes fun_args1 tvs2 = tyCoVarsOfTypes fun_args2 + -- See Note [Orienting TyFamLHS/TyFamLHS] + swap_for_size = typesSize fun_args2 > typesSize fun_args1 + + -- See Note [Orienting TyFamLHS/TyFamLHS] swap_for_rewriting = anyVarSet (isTouchableMetaTyVar tclvl) tvs2 && - -- swap 'em: Note [Put touchable variables on the left] + -- See Note [Put touchable variables on the left] not (anyVarSet (isTouchableMetaTyVar tclvl) tvs1) - -- this check is just to avoid unfruitful swapping - - -- If we have F a ~ F (F a), we want to swap. - swap_for_occurs - | cterHasNoProblem $ checkTyFamEq fun_tc2 fun_args2 - (mkTyConApp fun_tc1 fun_args1) - , cterHasOccursCheck $ checkTyFamEq fun_tc1 fun_args1 - (mkTyConApp fun_tc2 fun_args2) - = True - - | otherwise - = False - - ; if swap_for_rewriting || swap_for_occurs - then do { new_ev <- do_swap - ; canEqCanLHSFinish new_ev eq_rel IsSwapped lhs2 (ps_xi1 `mkCastTyMCo` sym_mco) } - else finish_without_swapping } - - -- that's all the special cases. Now we just figure out which non-special case - -- to continue to. - | otherwise - = finish_without_swapping - - where - sym_mco = mkSymMCo mco - - do_swap = rewriteCastedEquality ev eq_rel swapped (canEqLHSType lhs1) (canEqLHSType lhs2) mco - finish_without_swapping = canEqCanLHSFinish ev eq_rel swapped lhs1 (ps_xi2 `mkCastTyMCo` mco) - - --- This function handles the case where one side is a tyvar and the other is --- a type family application. Which to put on the left? --- If the tyvar is a touchable meta-tyvar, put it on the left, as this may --- be our only shot to unify. --- Otherwise, put the function on the left, because it's generally better to --- rewrite away function calls. This makes types smaller. And it seems necessary: --- [W] F alpha ~ alpha --- [W] F alpha ~ beta --- [W] G alpha beta ~ Int ( where we have type instance G a a = a ) --- If we end up with a stuck alpha ~ F alpha, we won't be able to solve this. --- Test case: indexed-types/should_compile/CEqCanOccursCheck -canEqTyVarFunEq :: CtEvidence -- :: lhs ~ (rhs |> mco) - -- or (rhs |> mco) ~ lhs if swapped - -> EqRel -> SwapFlag - -> TyVar -> TcType -- lhs (or if swapped rhs), pretty lhs - -> TyCon -> [Xi] -> TcType -- rhs (or if swapped lhs) fun and args, pretty rhs - -> MCoercion -- :: kind(rhs) ~N kind(lhs) - -> TcS (StopOrContinue Ct) -canEqTyVarFunEq ev eq_rel swapped tv1 ps_xi1 fun_tc2 fun_args2 ps_xi2 mco - = do { is_touchable <- touchabilityTest (ctEvFlavour ev) tv1 rhs - ; if | case is_touchable of { Untouchable -> False; _ -> True } - , cterHasNoProblem $ - checkTyVarEq tv1 rhs `cterRemoveProblem` cteTypeFamily - -> canEqCanLHSFinish ev eq_rel swapped (TyVarLHS tv1) rhs + -- This second check is just to avoid unfruitful swapping - | otherwise - -> do { new_ev <- rewriteCastedEquality ev eq_rel swapped - (mkTyVarTy tv1) (mkTyConApp fun_tc2 fun_args2) - mco - ; canEqCanLHSFinish new_ev eq_rel IsSwapped - (TyFamLHS fun_tc2 fun_args2) - (ps_xi1 `mkCastTyMCo` sym_mco) } } + ; if swap_for_rewriting || swap_for_size + then finish_with_swapping + else finish_without_swapping } where sym_mco = mkSymMCo mco - rhs = ps_xi2 `mkCastTyMCo` mco + role = eqRelRole eq_rel + lhs1_ty = canEqLHSType lhs1 + lhs2_ty = canEqLHSType lhs2 + + finish_without_swapping + = canEqCanLHSFinish ev eq_rel swapped lhs1 (ps_xi2 `mkCastTyMCo` mco) + + -- Swapping. We have ev : lhs1 ~ lhs2 |> co + -- We swap to new_ev : lhs2 ~ lhs1 |> sym co + -- ev = grefl1 ; sym new_ev ; grefl2 + -- where grefl1 : lhs1 ~ lhs1 |> sym co + -- grefl2 : lhs2 ~ lhs2 |> co + finish_with_swapping + = do { let lhs1_redn = mkGReflRightMRedn role lhs1_ty sym_mco + lhs2_redn = mkGReflLeftMRedn role lhs2_ty mco + ; new_ev <-rewriteEqEvidence emptyRewriterSet ev swapped lhs1_redn lhs2_redn + ; canEqCanLHSFinish new_ev eq_rel IsSwapped lhs2 (ps_xi1 `mkCastTyMCo` sym_mco) } + + put_tyvar_on_lhs = isWanted ev && eq_rel == NomEq + -- See Note [Orienting TyVarLHS/TyFamLHS] + -- Same conditions as for canEqCanLHSFinish_try_unification + -- which we are setting ourselves up for here + +{- Note [Orienting TyVarLHS/TyFamLHS] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +What if one side is a TyVarLHS and the other is a TyFamLHS, (a ~ F tys)? +Which to put on the left? Answer: + +* If there is no chance of unifying, put the type family on the left, + (F tys ~ a), because it's generally better to rewrite away function + calls. See `put_tyvar_on_lhs` in canEqCanLHS2; and + Note [Orienting TyVarLHS/TyFamLHS] + +* But if there /is/ a chance of unifying, put the tyvar on the left, + (a ~ F tys), as this may be our only shot to unify. Again see + `put_tyvar_on_lhs`. + +* But if we /fail/ to unify then flip back to (F tys ~ a) because it's + generally better to rewrite away function calls. See the call to + `swapAndFinish` in `canEqCanLHSFinish_try_unification` + + It's important to flip back. Consider + [W] F alpha ~ alpha + [W] F alpha ~ beta + [W] G alpha beta ~ Int ( where we have type instance G a a = a ) + If we end up with a stuck alpha ~ F alpha, we won't be able to solve this. + Test case: indexed-types/should_compile/CEqCanOccursCheck + +Note [Orienting TyFamLHS/TyFamLHS] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +If we have a TyFamLHS on both sides, we choose how to orient it. + +* swap_for_size. If we have + S a ~ F (G (H (Maybe a))) + then we swap so that we tend to rewrite the bigger type (F (G (H (Maybe a)))) + into the smaller one (S a). This same test tends to avoid occurs-check + errors. E.g. + S g ~ F (G (S g)) + Here (S g) occurs on the RHS, so this is not canonical. But if we swap it + around, it /is/ canonical + F (G (S g)) ~ S g + +* swap_for_rewriting: put touchable meta-tyvars on the left: + see Note [Put touchable variables on the left] +-} -- The RHS here is either not CanEqLHS, or it's one that we -- want to rewrite the LHS to (as per e.g. swapOverTyVars) -canEqCanLHSFinish :: CtEvidence - -> EqRel -> SwapFlag - -> CanEqLHS -- lhs (or, if swapped, rhs) - -> TcType -- rhs (or, if swapped, lhs) - -> TcS (StopOrContinue Ct) -canEqCanLHSFinish ev eq_rel swapped lhs rhs +canEqCanLHSFinish, canEqCanLHSFinish_try_unification, + canEqCanLHSFinish_no_unification + :: CtEvidence + -> EqRel -> SwapFlag + -> CanEqLHS -- lhs (or, if swapped, rhs) + -> TcType -- rhs (or, if swapped, lhs) + -> TcS (StopOrContinue Ct) -- RHS is fully rewritten, but with type synonyms -- preserved as much as possible -- Guaranteed preconditions that @@ -1683,71 +1696,25 @@ canEqCanLHSFinish ev eq_rel swapped lhs rhs -- (TyEq:N) checked in can_eq_nc' -- (TyEq:TV) handled in canEqCanLHS2 - = do { -- rewriteEqEvidence performs the swap if necessary - new_ev <- rewriteEqEvidence emptyRewriterSet ev swapped - (mkReflRedn role lhs_ty) - (mkReflRedn role rhs) +--------------------------- +canEqCanLHSFinish ev eq_rel swapped lhs rhs + = do { traceTcS "canEqCanLHSFinish" $ + vcat [ text "ev:" <+> ppr ev + , text "swapped:" <+> ppr swapped + , text "lhs:" <+> ppr lhs + , text "rhs:" <+> ppr rhs ] - -- Assertion: (TyEq:K) is already satisfied + -- Assertion: (TyEq:K) is already satisfied ; massert (canEqLHSKind lhs `eqType` typeKind rhs) - -- Assertion: (TyEq:N) is already satisfied (if applicable) + -- Assertion: (TyEq:N) is already satisfied (if applicable) ; assertPprM ty_eq_N_OK $ vcat [ text "CanEqCanLHSFinish: (TyEq:N) not satisfied" , text "rhs:" <+> ppr rhs ] - -- Do checkTypeEq to guarantee (TyEq:OC), (TyEq:F) - -- Must do the occurs check even on tyvar/tyvar equalities, - -- in case have x ~ (y :: ..x...); this is #12593. - ; let result0 = checkTypeEq lhs rhs `cterRemoveProblem` cteTypeFamily - -- cterRemoveProblem cteTypeFamily: type families are OK here - -- NB: no occCheckExpand here; see Note [Rewriting synonyms] - -- in GHC.Tc.Solver.Rewrite - - -- (a ~R# b a) is soluble if b later turns out to be Identity - result = case eq_rel of - NomEq -> result0 - ReprEq -> cterSetOccursCheckSoluble result0 - - non_canonical_result what - = do { traceTcS ("canEqCanLHSFinish: " ++ what) (ppr lhs $$ ppr rhs) - ; solveIrredEquality (NonCanonicalReason result) new_ev } - - ; if cterHasNoProblem result - then do { traceTcS "CEqCan" (ppr lhs $$ ppr rhs) - ; ics <- getInertCans - ; interactEq ics (EqCt { eq_ev = new_ev, eq_eq_rel = eq_rel - , eq_lhs = lhs, eq_rhs = rhs }) } - - else do { m_stuff <- breakTyEqCycle_maybe ev result lhs rhs - -- See Note [Type equality cycles]; - -- returning Nothing is the vastly common case - ; case m_stuff of - { Nothing -> non_canonical_result "Can't make canonical" - - - ; Just rhs_redn@(Reduction _ new_rhs) -> - do { traceTcS "canEqCanLHSFinish breaking a cycle" $ - vcat [ text "lhs:" <+> ppr lhs, text "rhs:" <+> ppr rhs - , text "new_rhs:" <+> ppr new_rhs ] - - -- This check is Detail (1) in the Note - ; if cterHasOccursCheck (checkTypeEq lhs new_rhs) - then non_canonical_result "Note [Type equality cycles] Detail (1)" - - else do { -- See Detail (6) of Note [Type equality cycles] - new_new_ev <- rewriteEqEvidence emptyRewriterSet - new_ev NotSwapped - (mkReflRedn Nominal lhs_ty) - rhs_redn - ; ics <- getInertCans - ; interactEq ics (EqCt { eq_ev = new_new_ev, eq_eq_rel = eq_rel - , eq_lhs = lhs, eq_rhs = new_rhs }) }}}}} - where - role = eqRelRole eq_rel - - lhs_ty = canEqLHSType lhs + ; canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs } + where -- This is about (TyEq:N): check that we don't have a saturated application -- of a newtype TyCon at the top level of the RHS, if the constructor -- of the newtype is in scope. @@ -1765,13 +1732,177 @@ canEqCanLHSFinish ev eq_rel swapped lhs rhs | otherwise = return True +----------------------- +canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs + -- Try unification; for Wanted, Nominal equalities with a meta-tyvar on the LHS + | isWanted ev -- See Note [Do not unify Givens] + , NomEq <- eq_rel -- See Note [Do not unify representational equalities] + , TyVarLHS tv <- lhs + = do { given_eq_lvl <- getInnermostGivenEqLevel + ; if not (touchabilityAndShapeTest given_eq_lvl tv rhs) + then if | Just can_rhs <- canTyFamEqLHS_maybe rhs + -> swapAndFinish ev eq_rel swapped (mkTyVarTy tv) can_rhs + -- See Note [Orienting TyVarLHS/TyFamLHS] + + | otherwise + -> canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs + else + + -- We have a touchable unification variable on the left + do { check_result <- checkTouchableTyVarEq ev tv rhs + ; case check_result of { + PuFail reason + | Just can_rhs <- canTyFamEqLHS_maybe rhs + -> swapAndFinish ev eq_rel swapped (mkTyVarTy tv) can_rhs + -- Swap back: see Note [Orienting TyVarLHS/TyFamLHS] + + | reason `cterHasOnlyProblems` do_not_prevent_rewriting + -> canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs + + | otherwise + -> tryIrredInstead reason ev eq_rel swapped lhs rhs ; + + PuOK rhs_redn _ -> + + -- Success: we can solve by unification + do { -- In the common case where rhs_redn is Refl, we don't need to rewrite + -- the evidence even if swapped=IsSwapped. Suppose the original was + -- [W] co : Int ~ alpha + -- We unify alpha := Int, and set co := <Int>. No need to + -- swap to co = sym co' + -- co' = <Int> + new_ev <- if isReflCo (reductionCoercion rhs_redn) + then return ev + else rewriteEqEvidence emptyRewriterSet ev swapped + (mkReflRedn Nominal (mkTyVarTy tv)) rhs_redn + + ; let tv_ty = mkTyVarTy tv + final_rhs = reductionReducedType rhs_redn + tv_lvl = tcTyVarLevel tv + + ; traceTcS "Sneaky unification:" $ + vcat [text "Unifies:" <+> ppr tv <+> text ":=" <+> ppr final_rhs, + text "Coercion:" <+> pprEq tv_ty final_rhs, + text "Left Kind is:" <+> ppr (typeKind tv_ty), + text "Right Kind is:" <+> ppr (typeKind final_rhs) ] + + -- Update the unification variable itself + ; unifyTyVar tv final_rhs + + -- Provide Refl evidence for the constraint + -- Ignore 'swapped' because it's Refl! + ; setEvBindIfWanted new_ev IsCoherent $ + evCoercion (mkNomReflCo final_rhs) + + -- Set the unification flag if we have done outer unifications + -- that might affect an earlier implication constraint + ; ambient_lvl <- getTcLevel + ; when (ambient_lvl `strictlyDeeperThan` tv_lvl) $ + setUnificationFlag tv_lvl + + -- Kick out any constraints that can now be rewritten + ; n_kicked <- kickOutAfterUnification tv + + ; return (Stop new_ev (text "Solved by unification" <+> pprKicked n_kicked)) }}}} + + -- Otherwise unification is off the table + | otherwise + = canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs + + where + -- Some problems prevent /unification/ but not /rewriting/ + -- Skolem-escape: if we have [W] alpha[2] ~ Maybe b[3] + -- we can't unify (skolem-escape); but it /is/ canonical, + -- and hence we /can/ use it for rewriting + -- Concrete-ness: alpha[conc] ~ b[sk] + -- We can use it to rewrite; we still have to solve the original + -- Coercion holes: see wrinkle (2) of + -- Note [Equalities with incompatible kinds] + do_not_prevent_rewriting :: CheckTyEqResult + do_not_prevent_rewriting = cteProblem cteSkolemEscape S.<> + cteProblem cteConcrete S.<> + cteProblem cteCoercionHole + +--------------------------- +-- Unification is off the table +canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs + = do { -- Do checkTypeEq to guarantee (TyEq:OC), (TyEq:F) + -- Must do the occurs check even on tyvar/tyvar equalities, + -- in case have x ~ (y :: ..x...); this is #12593. + ; check_result <- checkTypeEq ev eq_rel lhs rhs + + ; let lhs_ty = canEqLHSType lhs + ; case check_result of + PuFail reason + + -- If we had F a ~ G (F a), which gives an occurs check, + -- then swap it to G (F a) ~ F a, which does not + -- However `swap_for_size` above will orient it with (G (F a)) on + -- the left anwyway, so the next four lines of code are redundant + -- I'm leaving them here in case they become relevant again +-- | TyFamLHS {} <- lhs +-- , Just can_rhs <- canTyFamEqLHS_maybe rhs +-- , reason `cterHasOnlyProblem` cteSolubleOccurs +-- -> swapAndFinish ev eq_rel swapped lhs_ty can_rhs +-- | otherwise + + -> tryIrredInstead reason ev eq_rel swapped lhs rhs + + PuOK rhs_redn _ + -> do { new_ev <- rewriteEqEvidence emptyRewriterSet ev swapped + (mkReflRedn (eqRelRole eq_rel) lhs_ty) + rhs_redn + + -- Important: even if the coercion is Refl, + -- * new_ev has reductionReducedType on the RHS + -- * eq_rhs is set to reductionReducedType + -- See Note [Forgetful synonyms in checkTyConApp] in GHC.Tc.Utils.Unify + ; interactEq (EqCt { eq_ev = new_ev, eq_eq_rel = eq_rel + , eq_lhs = lhs + , eq_rhs = reductionReducedType rhs_redn }) } } + +---------------------- +swapAndFinish :: CtEvidence -> EqRel -> SwapFlag + -> TcType -> CanEqLHS -- ty ~ F tys + -> TcS (StopOrContinue Ct) +-- We have an equality alpha ~ F tys, that we can't unify e.g because 'tys' +-- mentions alpha, it would not be a canonical constraint as-is. +-- We want to flip it to (F tys ~ a), whereupon it is canonical +swapAndFinish ev eq_rel swapped lhs_ty can_rhs + = do { new_ev <- rewriteEqEvidence emptyRewriterSet ev (flipSwap swapped) + (mkReflRedn role (canEqLHSType can_rhs)) + (mkReflRedn role lhs_ty) + ; interactEq (EqCt { eq_ev = new_ev, eq_eq_rel = eq_rel + , eq_lhs = can_rhs, eq_rhs = lhs_ty }) } + where + role = eqRelRole eq_rel + +---------------------- +tryIrredInstead :: CheckTyEqResult -> CtEvidence -> EqRel -> SwapFlag + -> CanEqLHS -> TcType -> TcS (StopOrContinue Ct) +-- We have a non-canonical equality +-- We still swap it if 'swapped' says so, so that it is oriented +-- in the direction that the error message reporting machinery +-- expects it; e.g. (m ~ t m) rather than (t m ~ m) +-- This is not very important, and only affects error reporting. +tryIrredInstead reason ev eq_rel swapped lhs rhs + = do { traceTcS "cantMakeCanonical" (ppr reason $$ ppr lhs $$ ppr rhs) + ; new_ev <- rewriteEqEvidence emptyRewriterSet ev swapped + (mkReflRedn role (canEqLHSType lhs)) + (mkReflRedn role rhs) + ; solveIrredEquality (NonCanonicalReason reason) new_ev } + where + role = eqRelRole eq_rel + +----------------------- -- | Solve a reflexive equality constraint canEqReflexive :: CtEvidence -- ty ~ ty -> EqRel -> TcType -- ty -> TcS (StopOrContinue Ct) -- always Stop canEqReflexive ev eq_rel ty - = do { setEvBindIfWanted ev IsCoherent (evCoercion $ mkReflCo (eqRelRole eq_rel) ty) + = do { setEvBindIfWanted ev IsCoherent $ + evCoercion (mkReflCo (eqRelRole eq_rel) ty) ; stopWith ev "Solved by reflexivity" } {- Note [Equalities with incompatible kinds] @@ -1806,8 +1937,15 @@ Wrinkles: and unifying alpha effectively promotes this wanted to a given. Doing so means we lose track of the rewriter set associated with the wanted. + Another way to say it: we must not have a co_hole in a Given, and + unification effectively makes a Given. (This is not very well motivated; + may need to dig deeper if anything goes wrong.) + On the other hand, w is perfectly suitable for rewriting, because of the - way we carefully track rewriter sets. + way we carefully track rewriter sets. So we include cteCoercionHole in + `do_not_prevent_rewriting` in `canEqCanLHSFinish_try_unification`. (Side + note: I think this is an open choice. Maybe we'd get better error + messages if we did not use these equalities for rewriting.) We thus allow w to be a CEqCan, but we prevent unification. See Note [Unification preconditions] in GHC.Tc.Utils.Unify. @@ -1823,18 +1961,19 @@ Wrinkles: [W] (a :: k1) ~ ((rhs |> sym co) :: k1) to the irreducibles. Some time later, we solve co, and fill in co's coercion hole. This kicks out the irreducible as described in (2). - But now, during canonicalization, we see the cast - and remove it, in canEqCast. By the time we get into canEqCanLHS, the equality - is heterogeneous again, and the process repeats. - - To avoid this, we don't strip casts off a type if the other type - in the equality is a CanEqLHS (the scenario above can happen with a - type family, too. testcase: typecheck/should_compile/T13822). - And this is an improvement regardless: - because tyvars can, generally, unify with casted types, there's no - reason to go through the work of stripping off the cast when the - cast appears opposite a tyvar. This is implemented in the cast case - of can_eq_nc'. + + But now, during canonicalization, we see the cast and remove it, in + canEqCast. By the time we get into canEqCanLHS, the equality is + heterogeneous again, and the process repeats. + + To avoid this, we don't strip casts off a type if the other type in the + equality is a CanEqLHS (the scenario above can happen with a type + family, too. testcase: typecheck/should_compile/T13822). + + And this is an improvement regardless: because tyvars can, generally, + unify with casted types, there's no reason to go through the work of + stripping off the cast when the cast appears opposite a tyvar. This is + implemented in the cast case of can_eq_nc'. Historical note: @@ -1911,10 +2050,10 @@ use them for rewriting. (NB: A rigid type constructor is at the top of all RHSs, preventing reorienting in canEqTyVarFunEq in the tyvar cases.) -The key idea is to replace the outermost type family applications in the RHS of the -starred constraints with a fresh variable, which we'll call a cycle-breaker -variable, or cbv. Then, relate the cbv back with the original type family application -via new equality constraints. Our situations thus become: +The key idea is to replace the outermost type family applications in the RHS of +the starred constraints with a fresh variable, which we'll call a cycle-breaker +variable, or cbv. Then, relate the cbv back with the original type family +application via new equality constraints. Our situations thus become: instance C (Maybe b) [G] a ~ Maybe cbv @@ -1936,32 +2075,34 @@ or [W] Code a ~ '[ '[ alpha ] ] This transformation (creating the new types and emitting new equality -constraints) is done in breakTyEqCycle_maybe. +constraints) is done by the `FamAppBreaker` field of `TEFA_Break`, which +in turn lives in the `tef_fam_app` field of `TyEqFlags`. And that in +turn controls the behaviour of the workhorse: GHC.Tc.Utils.Unify.checkTyEqRhs. The details depend on whether we're working with a Given or a Wanted. Given ----- +We emit a new Given, [G] F a ~ cbv, equating the type family application +to our new cbv. This is actually done by `break_given` in +`GHC.Tc.Solver.Monad.checkTypeEq`. -We emit a new Given, [G] F a ~ cbv, equating the type family application to -our new cbv. Note its orientation: The type family ends up on the left; see -commentary on canEqTyVarFunEq, which decides how to orient such cases. No -special treatment for CycleBreakerTvs is necessary. This scenario is now -easily soluble, by using the first Given to rewrite the Wanted, which can now -be solved. +Note its orientation: The type family ends up on the left; see +Note [Orienting TyFamLHS/TyFamLHS]d. No special treatment for +CycleBreakerTvs is necessary. This scenario is now easily soluble, by using +the first Given to rewrite the Wanted, which can now be solved. (The first Given actually also rewrites the second one, giving [G] F (Maybe cbv) ~ cbv, but this causes no trouble.) -Of course, we don't want our fresh variables leaking into e.g. error messages. -So we fill in the metavariables with their original type family applications -after we're done running the solver (in nestImplicTcS and runTcSWithEvBinds). -This is done by restoreTyVarCycles, which uses the inert_cycle_breakers field in -InertSet, which contains the pairings invented in breakTyEqCycle_maybe. - -That is: +Of course, we don't want our fresh variables leaking into e.g. error +messages. So we fill in the metavariables with their original type family +applications after we're done running the solver (in nestImplicTcS and +runTcSWithEvBinds). This is done by `restoreTyVarCycles`, which uses the +`inert_cycle_breakers` field in InertSet, which contains the pairings +invented in `break_given`. -We transform +That is, we transform [G] g : lhs ~ ...(F lhs)... to [G] (Refl lhs) : F lhs ~ cbv -- CEqCan @@ -1972,10 +2113,10 @@ Note that * `cbv` is a is a meta-tyvar, but it is completely untouchable. * We track the cycle-breaker variables in inert_cycle_breakers in InertSet * We eventually fill in the cycle-breakers, with `cbv := F lhs`. - No one else fills in cycle-breakers! + No one else fills in CycleBreakerTvs! * The evidence for the new `F lhs ~ cbv` constraint is Refl, because we know this fill-in is ultimately going to happen. -* In inert_cycle_breakers, we remember the (cbv, F lhs) pair; that is, we +* In `inert_cycle_breakers`, we remember the (cbv, F lhs) pair; that is, we remember the /original/ type. The [G] F lhs ~ cbv constraint may be rewritten by other givens (eg if we have another [G] lhs ~ (b,c)), but at the end we still fill in with cbv := F lhs @@ -1984,9 +2125,12 @@ Note that Wanted ------ -The fresh cycle-breaker variables here must actually be normal, touchable -metavariables. That is, they are TauTvs. Nothing at all unusual. Repeating -the example from above, we have +First, we do not cycle-break unless the LHS is a unifiable type variable +See Note [Don't cycle-break Wanteds when not unifying] in GHC.Tc.Solver.Monad. + +OK, so suppose the LHS is a unifiable type variable. The fresh cycle-breaker +variables here must actually be normal, touchable metavariables. That is, they +are TauTvs. Nothing at all unusual. Repeating the example from above, we have *[W] alpha ~ (Arg alpha -> Res alpha) @@ -1996,22 +2140,20 @@ and we turn this into [W] Arg alpha ~ cbv1 [W] Res alpha ~ cbv2 -where cbv1 and cbv2 are fresh TauTvs. Why TauTvs? See [Why TauTvs] below. +where cbv1 and cbv2 are fresh TauTvs. This is actually done by `break_wanted` +in `GHC.Tc.Solver.Monad.checkTouchableTyVarEq`. + +Why TauTvs? See [Why TauTvs] below. Critically, we emit the two new constraints (the last two above) -directly instead of calling unifyWanted. (Otherwise, we'd end up unifying cbv1 -and cbv2 immediately, achieving nothing.) -Next, we unify alpha := cbv1 -> cbv2, having eliminated the occurs check. This -unification -- which must be the next step after breaking the cycles -- -happens in the course of normal behavior of top-level -interactions, later in the solver pipeline. We know this unification will -indeed happen because breakTyEqCycle_maybe, which decides whether to apply -this logic, checks to ensure unification will succeed in its final_check. -(In particular, the LHS must be a touchable tyvar, never a type family. We don't -yet have an example of where this logic is needed with a type family, and it's -unclear how to handle this case, so we're skipping for now.) Now, we're -here (including further context from our original example, from the top of the -Note): +directly instead of calling unifyWanted. (Otherwise, we'd end up +unifying cbv1 and cbv2 immediately, achieving nothing.) Next, we +unify alpha := cbv1 -> cbv2, having eliminated the occurs check. This +unification happens immediately following a successful call to +checkTouchableTyVarEq, in canEqCanLHSFinish_try_unification. + +Now, we're here (including further context from our original example, +from the top of the Note): instance C (a -> b) [W] Arg (cbv1 -> cbv2) ~ cbv1 @@ -2080,62 +2222,54 @@ Note that we need to unify the cbvs here; if we did not, there would be no way to solve those constraints. That's why the cycle-breakers are ordinary TauTvs. -In all cases ------------- - -We detect this scenario by the following characteristics: - - a constraint with a soluble occurs-check failure - (as indicated by the cteSolubleOccurs bit set in a CheckTyEqResult - from checkTypeEq) - - and a nominal equality - - and either - - a Given flavour (but see also Detail (7) below) - - a Wanted flavour, with a touchable metavariable on the left - -We don't use this trick for representational equalities, as there is no -concrete use case where it is helpful (unlike for nominal equalities). -Furthermore, because function applications can be CanEqLHSs, but newtype -applications cannot, the disparities between the cases are enough that it -would be effortful to expand the idea to representational equalities. A quick -attempt, with +How all this is implemented +--------------------------- +We implement all this via the `TEFA_Break` constructor of `TyEqFamApp`, +itself stored in the `tef_fam_app` field of `TyEqFlags`, which controls +the behaviour of `GHC.Tc.Utils.Unify.checkTyEqRhs`. The `TEFA_Break` +stuff happens when `checkTyEqRhs` encounters a family application. - data family N a b +We try the cycle-breaking trick: +* For Wanteds, when there is a touchable unification variable on the left +* For Givens, regardless of the LHS + +EXCEPT that, in both cases, as `GHC.Tc.Solver.Monad.mkTEFA_Break` shows, we +don't use this trick: + +* When the constraint we are looking at was itself created by cycle-breaking; + see Detail (7) below. +* For representational equalities, as there is no concrete use case where it is + helpful (unlike for nominal equalities). + + Furthermore, because function applications can be CanEqLHSs, but newtype + applications cannot, the disparities between the cases are enough that it + would be effortful to expand the idea to representational equalities. A quick + attempt, with + data family N a b f :: (Coercible a (N a b), Coercible (N a b) b) => a -> b f = coerce + failed with "Could not match 'b' with 'b'." Further work is held off + until when we have a concrete incentive to explore this dark corner. + +More details: -failed with "Could not match 'b' with 'b'." Further work is held off -until when we have a concrete incentive to explore this dark corner. - -Details: - - (1) We don't look under foralls, at all, when substituting away type family - applications, because doing so can never be fruitful. Recall that we - are in a case like [G] lhs ~ forall b. ... lhs .... Until we have a type - family that can pull the body out from a forall (e.g. type instance F (forall b. ty) = ty), - this will always be - insoluble. Note also that the forall cannot be in an argument to a - type family, or that outer type family application would already have - been substituted away. - - However, we still must check to make sure that breakTyEqCycle_maybe actually - succeeds in getting rid of all occurrences of the offending lhs. If - one is hidden under a forall, this won't be true. A similar problem can - happen if the variable appears only in a kind - (e.g. k ~ ... (a :: k) ...). So we perform an additional check after - performing the substitution. It is tiresome to re-run all of checkTypeEq - here, but reimplementing just the occurs-check is even more tiresome. - - Skipping this check causes typecheck/should_fail/GivenForallLoop and - polykinds/T18451 to loop. - - (2) Our goal here is to avoid loops in rewriting. We can thus skip looking - in coercions, as we don't rewrite in coercions in the algorithm in - GHC.Solver.Rewrite. (This is another reason - we need to re-check that we've gotten rid of all occurrences of the - offending variable.) - - (3) As we're substituting as described in this Note, we can build ill-kinded + (1) We don't look under foralls, at all, in `checkTyEqRhs`. There might be + a cyclic occurrence underneath, in a case like + [G] lhs ~ forall b. ... lhs .... + but it doesn't matter because we will classify the constraint as Irred, + so it will not be used for rewriting. + + Earlier versions required an extra, post-breaking, check. Skipping this + check causes typecheck/should_fail/GivenForallLoop and polykinds/T18451 to + loop. But now it is all simpler, with no need for a second check. + + (2) Historical Note: our goal here is to avoid loops in rewriting. We can thus + skip looking in coercions, as we don't rewrite in coercions in the + algorithm in GHC.Solver.Rewrite. This doesn't seem relevant any more. + We cycle break to make the constraint canonical. + + (3) As we cycle-break as described in this Note, we can build ill-kinded types. For example, if we have Proxy (F a) b, where (b :: F a), then replacing this with Proxy cbv b is ill-kinded. However, we will later set cbv := F a, and so the zonked type will be well-kinded again. @@ -2151,37 +2285,36 @@ Details: that we never assume anything about its structure, like that it has a result type or a RuntimeRep argument). - (4) The evidence for the produced Givens is all just reflexive, because - we will eventually set the cycle-breaker variable to be the type family, - and then, after the zonk, all will be well. See also the notes at the - end of the Given section of this Note. - - (5) The approach here is inefficient because it replaces every (outermost) - type family application with a type variable, regardless of whether that - particular appplication is implicated in the occurs check. An alternative - would be to replce only type-family applications that mention the offending LHS. - For instance, we could choose to - affect only type family applications that mention the offending LHS: - e.g. in a ~ (F b, G a), we need to replace only G a, not F b. Furthermore, - we could try to detect cases like a ~ (F a, F a) and use the same - tyvar to replace F a. (Cf. - Note [Flattening type-family applications when matching instances] - in GHC.Core.Unify, which - goes to this extra effort.) There may be other opportunities for - improvement. However, this is really a very small corner case. - The investment to craft a clever, - performant solution seems unworthwhile. - - (6) We often get the predicate associated with a constraint from its - evidence with ctPred. We thus must not only make sure the generated - CEqCan's fields have the updated RHS type (that is, the one produced - by replacing type family applications with fresh variables), - but we must also update the evidence itself. This is done by the call to rewriteEqEvidence - in canEqCanLHSFinish. + (4) The evidence for the produced Givens is all just reflexive, because we + will eventually set the cycle-breaker variable to be the type family, and + then, after the zonk, all will be well. See also the notes at the end of + the Given section of this Note. + + (5) The implementation in `checkTyEqRhs` is efficient because it only replaces + a type family application with a type variable, if that particular + appplication is implicated in the occurs check. For example: + [W] alpha ~ Maybe (F alpha, G beta) + We'll end up calling GHC.Tc.Utils.Unify.checkFamApp + * On `F alpha`, which fail and calls the cycle-breaker in TEFA_Break + * On `G beta`, which succeeds no problem. + + However, we make no attempt to detect cases like a ~ (F a, F a) and use the + same tyvar to replace F a. The constraint solver will common them up later! + (Cf. Note [Flattening type-family applications when matching instances] in + GHC.Core.Unify, which goes to this extra effort.) However, this is really + a very small corner case. The investment to craft a clever, performant + solution seems unworthwhile. + + (6) We often get the predicate associated with a constraint from its evidence + with ctPred. We thus must not only make sure the generated CEqCan's fields + have the updated RHS type (that is, the one produced by replacing type + family applications with fresh variables), but we must also update the + evidence itself. This is done by the call to rewriteEqEvidence in + canEqCanLHSFinish. (7) We don't wish to apply this magic on the equalities created - by this very same process. - Consider this, from typecheck/should_compile/ContextStack2: + by this very same process. Consider this, from + typecheck/should_compile/ContextStack2: type instance TF (a, b) = (TF a, TF b) t :: (a ~ TF (a, Int)) => ... @@ -2207,25 +2340,18 @@ Details: [G] (TF cbv1, TF cbv2) ~ cbv1 - which looks remarkably like the Given we started with. If left - unchecked, this will end up breaking cycles again, looping ad - infinitum (and resulting in a context-stack reduction error, - not an outright loop). The solution is easy: don't break cycles - on an equality generated by breaking cycles. Instead, we mark this - final Given as a CIrredCan with a NonCanonicalReason with the soluble - occurs-check bit set (only). + which looks remarkably like the Given we started with. If left unchecked, + this will end up breaking cycles again, looping ad infinitum (and + resulting in a context-stack reduction error, not an outright loop). The + solution is easy: don't break cycles on an equality generated by breaking + cycles. Instead, we mark this final Given as a CIrredCan with a + NonCanonicalReason with the soluble occurs-check bit set (only). We track these equalities by giving them a special CtOrigin, - CycleBreakerOrigin. This works for both Givens and Wanteds, as - we need the logic in the W case for e.g. typecheck/should_fail/T17139. - Because this logic needs to work for Wanteds, too, we cannot - simply look for a CycleBreakerTv on the left: Wanteds don't use them. - - (8) We really want to do this all only when there is a soluble occurs-check - failure, not when other problems arise (such as an impredicative - equality like alpha ~ forall a. a -> a). That is why breakTyEqCycle_maybe - uses cterHasOnlyProblem when looking at the result of checkTypeEq, which - checks for many of the invariants on a CEqCan. + CycleBreakerOrigin. This works for both Givens and Wanteds, as we need the + logic in the W case for e.g. typecheck/should_fail/T17139. Because this + logic needs to work for Wanteds, too, we cannot simply look for a + CycleBreakerTv on the left: Wanteds don't use them. ********************************************************************** @@ -2235,22 +2361,6 @@ Details: ********************************************************************** -} -rewriteCastedEquality :: CtEvidence -- :: lhs ~ (rhs |> mco), or (rhs |> mco) ~ lhs - -> EqRel -> SwapFlag - -> TcType -- lhs - -> TcType -- rhs - -> MCoercion -- mco - -> TcS CtEvidence -- :: (lhs |> sym mco) ~ rhs - -- result is independent of SwapFlag -rewriteCastedEquality ev eq_rel swapped lhs rhs mco - = rewriteEqEvidence emptyRewriterSet ev swapped lhs_redn rhs_redn - where - lhs_redn = mkGReflRightMRedn role lhs sym_mco - rhs_redn = mkGReflLeftMRedn role rhs mco - - sym_mco = mkSymMCo mco - role = eqRelRole eq_rel - rewriteEqEvidence :: RewriterSet -- New rewriters -- See GHC.Tc.Types.Constraint -- Note [Wanteds rewrite Wanteds] @@ -2355,25 +2465,24 @@ But it's not so simple: call to strictly_more_visible. -} -interactEq :: InertCans -> EqCt -> TcS (StopOrContinue Ct) -interactEq inerts - work_item@(EqCt { eq_lhs = lhs, eq_ev = ev, eq_eq_rel = eq_rel }) +interactEq :: EqCt -> TcS (StopOrContinue Ct) +interactEq work_item@(EqCt { eq_lhs = lhs, eq_ev = ev, eq_eq_rel = eq_rel }) - | Just (ev_i, swapped) <- inertsCanDischarge inerts work_item - = do { setEvBindIfWanted ev IsCoherent $ - evCoercion (maybeSymCo swapped $ - downgradeRole (eqRelRole eq_rel) - (ctEvRole ev_i) - (ctEvCoercion ev_i)) - ; stopWith ev "Solved from inert" } - - | otherwise - = case lhs of - TyVarLHS tv -> tryToSolveByUnification tv work_item + = do { inerts <- getInertCans + ; if | Just (ev_i, swapped) <- inertsCanDischarge inerts work_item + -> do { setEvBindIfWanted ev IsCoherent $ + evCoercion (maybeSymCo swapped $ + downgradeRole (eqRelRole eq_rel) + (ctEvRole ev_i) + (ctEvCoercion ev_i)) + ; stopWith ev "Solved from inert" } - TyFamLHS tc args -> do { improveLocalFunEqs inerts tc args work_item - ; improveTopFunEqs tc args work_item - ; finishEqCt work_item } + | otherwise + -> case lhs of + TyVarLHS {} -> finishEqCt work_item + TyFamLHS tc args -> do { improveLocalFunEqs inerts tc args work_item + ; improveTopFunEqs tc args work_item + ; finishEqCt work_item } } inertsCanDischarge :: InertCans -> EqCt @@ -2422,81 +2531,32 @@ inertsCanDischarge inerts (EqCt { eq_lhs = lhs_w, eq_rhs = rhs_w inertsCanDischarge _ _ = Nothing ----------------------- --- We have a meta-tyvar on the left, and metaTyVarUpdateOK has said "yes" --- So try to solve by unifying. --- Three reasons why not: --- Skolem escape --- Given equalities (GADTs) --- Unifying a TyVarTv with a non-tyvar type -tryToSolveByUnification :: TcTyVar -- LHS tyvar - -> EqCt - -> TcS (StopOrContinue Ct) -tryToSolveByUnification tv - work_item@(EqCt { eq_rhs = rhs, eq_ev = ev, eq_eq_rel = eq_rel }) - - | ReprEq <- eq_rel -- See Note [Do not unify representational equalities] - = do { traceTcS "Not unifying representational equality" (ppr work_item) - ; dont_unify } - | otherwise - = do { is_touchable <- touchabilityTest (ctEvFlavour ev) tv rhs - ; traceTcS "tryToSolveByUnification" (vcat [ ppr tv <+> char '~' <+> ppr rhs - , ppr is_touchable ]) +{- Note [Do not unify Givens] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider this GADT match + data T a where + T1 :: T Int + ... - ; case is_touchable of - Untouchable -> dont_unify - -- For the latter two cases see Note [Solve by unification] + f x = case x of + T1 -> True + ... - TouchableSameLevel -> solveByUnification ev tv rhs +So we get f :: T alpha[1] -> beta[1] + x :: T alpha[1] +and from the T1 branch we get the implication + forall[2] (alpha[1] ~ Int) => beta[1] ~ Bool - TouchableOuterLevel free_metas tv_lvl - -> do { wrapTcS $ mapM_ (promoteMetaTyVarTo tv_lvl) free_metas - ; setUnificationFlag tv_lvl - ; solveByUnification ev tv rhs } } - where - dont_unify = finishEqCt work_item - -solveByUnification :: CtEvidence -> TcTyVar -> Xi -> TcS (StopOrContinue Ct) --- Solve with the identity coercion --- Precondition: kind(xi) equals kind(tv) --- Precondition: CtEvidence is Wanted --- Precondition: CtEvidence is nominal --- Returns: work_item where --- work_item = the new Given constraint --- --- NB: No need for an occurs check here, because solveByUnification always --- arises from a CEqCan, a *canonical* constraint. Its invariant (TyEq:OC) --- says that in (a ~ xi), the type variable a does not appear in xi. --- See GHC.Tc.Types.Constraint.Ct invariants. --- --- Post: tv is unified (by side effect) with xi; --- we often write tv := xi -solveByUnification ev tv xi - = do { let tv_ty = mkTyVarTy tv - ; traceTcS "Sneaky unification:" $ - vcat [text "Unifies:" <+> ppr tv <+> text ":=" <+> ppr xi, - text "Coercion:" <+> pprEq tv_ty xi, - text "Left Kind is:" <+> ppr (typeKind tv_ty), - text "Right Kind is:" <+> ppr (typeKind xi) ] - ; unifyTyVar tv xi - ; setEvBindIfWanted ev IsCoherent (evCoercion (mkNomReflCo xi)) - ; n_kicked <- kickOutAfterUnification tv - ; return (Stop ev (text "Solved by unification" <+> pprKicked n_kicked)) } +Now, clearly we don't want to unify alpha:=Int! Yet at the moment we +process [G] alpha[1] ~ Int, we don't have any given-equalities in the +inert set, and hence there are no given equalities to make alpha untouchable. -{- Note [Avoid double unifications] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The spontaneous solver has to return a given which mentions the unified unification -variable *on the left* of the equality. Here is what happens if not: - Original wanted: (a ~ alpha), (alpha ~ Int) -We spontaneously solve the first wanted, without changing the order! - given : a ~ alpha [having unified alpha := a] -Now the second wanted comes along, but it cannot rewrite the given, so we simply continue. -At the end we spontaneously solve that guy, *reunifying* [alpha := Int] - -We avoid this problem by orienting the resulting given so that the unification -variable is on the left (note that alternatively we could attempt to -enforce this at canonicalization). +NB: if it were alpha[2] ~ Int, this argument wouldn't hold. But that +never happens: invariant (GivenInv) in Note [TcLevel invariants] +in GHC.Tc.Utils.TcType. + +Simple solution: never unify in Givens! Note [Do not unify representational equalities] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/compiler/GHC/Tc/Solver/InertSet.hs b/compiler/GHC/Tc/Solver/InertSet.hs index ed1386380a..ab5ee70ac1 100644 --- a/compiler/GHC/Tc/Solver/InertSet.hs +++ b/compiler/GHC/Tc/Solver/InertSet.hs @@ -36,7 +36,7 @@ module GHC.Tc.Solver.InertSet ( -- * Cycle breaker vars CycleBreakerVarStack, pushCycleBreakerVarStack, - insertCycleBreakerBinding, + addCycleBreakerBindings, forAllCycleBreakerBindings_ ) where @@ -237,13 +237,15 @@ instance Outputable WorkList where * * ********************************************************************* -} -type CycleBreakerVarStack = NonEmpty [(TcTyVar, TcType)] +type CycleBreakerVarStack = NonEmpty (Bag (TcTyVar, TcType)) -- ^ a stack of (CycleBreakerTv, original family applications) lists -- first element in the stack corresponds to current implication; -- later elements correspond to outer implications -- used to undo the cycle-breaking needed to handle -- Note [Type equality cycles] in GHC.Tc.Solver.Canonical -- Why store the outer implications? For the use in mightEqualLater (only) + -- + -- Why NonEmpty? So there is always a top element to add to data InertSet = IS { inert_cans :: InertCans @@ -291,7 +293,7 @@ emptyInertCans emptyInert :: InertSet emptyInert = IS { inert_cans = emptyInertCans - , inert_cycle_breakers = [] :| [] + , inert_cycle_breakers = emptyBag :| [] , inert_famapp_cache = emptyFunEqs , inert_solved_dicts = emptyDictMap } @@ -722,7 +724,7 @@ applying S(f,_) to t. ----------------------------------------------------------------------------- Our main invariant: - the CEqCans in inert_eqs should be a terminating generalised substitution + the EqCts in inert_eqs should be a terminating generalised substitution ----------------------------------------------------------------------------- Note that termination is not the same as idempotence. To apply S to a @@ -814,7 +816,7 @@ Main Theorem [Stability under extension] (T3) lhs not in t -- No occurs check in the work item -- If lhs is a type family application, we require only that -- lhs is not *rewritable* in t. See Note [Rewritable] and - -- Note [CEqCan occurs check] in GHC.Tc.Types.Constraint. + -- Note [EqCt occurs check] in GHC.Tc.Types.Constraint. AND, for every (lhs1 -fs-> s) in S: (K0) not (fw >= fs) @@ -849,7 +851,7 @@ The idea is that * T3 is guaranteed by an occurs-check on the work item. This is done during canonicalisation, in checkTypeEq; invariant - (TyEq:OC) of CEqCan. See also Note [CEqCan occurs check] in GHC.Tc.Types.Constraint. + (TyEq:OC) of CEqCan. See also Note [EqCt occurs check] in GHC.Tc.Types.Constraint. * (K1-3) are the "kick-out" criteria. (As stated, they are really the "keep" criteria.) If the current inert S contains a triple that does @@ -1633,13 +1635,13 @@ mightEqualLater inert_set given_pred given_loc wanted_pred wanted_loc | otherwise = False - -- like startSolvingByUnification, but allows cbv variables to unify + -- Like checkTopShape, but allows cbv variables to unify can_unify :: TcTyVar -> MetaInfo -> Type -> Bool can_unify _lhs_tv TyVarTv rhs_ty -- see Example 3 from the Note | Just rhs_tv <- getTyVar_maybe rhs_ty = case tcTyVarDetails rhs_tv of MetaTv { mtv_info = TyVarTv } -> True - MetaTv {} -> False -- could unify with anything + MetaTv {} -> False -- Could unify with anything SkolemTv {} -> True RuntimeUnk -> True | otherwise -- not a var on the RHS @@ -1811,7 +1813,7 @@ lookupCycleBreakerVar cbv (IS { inert_cycle_breakers = cbvs_stack }) -- to avoid #20231. This function (and its one usage site) is the only reason -- that we store a stack instead of just the top environment. | Just tyfam_app <- assert (isCycleBreakerTyVar cbv) $ - firstJusts (NE.map (lookup cbv) cbvs_stack) + firstJusts (NE.map (lookupBag cbv) cbvs_stack) = tyfam_app | otherwise = pprPanic "lookupCycleBreakerVar found an unbound cycle breaker" (ppr cbv $$ ppr cbvs_stack) @@ -1819,15 +1821,16 @@ lookupCycleBreakerVar cbv (IS { inert_cycle_breakers = cbvs_stack }) -- | Push a fresh environment onto the cycle-breaker var stack. Useful -- when entering a nested implication. pushCycleBreakerVarStack :: CycleBreakerVarStack -> CycleBreakerVarStack -pushCycleBreakerVarStack = ([] <|) +pushCycleBreakerVarStack = (emptyBag <|) -- | Add a new cycle-breaker binding to the top environment on the stack. -insertCycleBreakerBinding :: TcTyVar -- ^ cbv, must be a CycleBreakerTv - -> TcType -- ^ cbv's expansion - -> CycleBreakerVarStack -> CycleBreakerVarStack -insertCycleBreakerBinding cbv expansion (top_env :| rest_envs) - = assert (isCycleBreakerTyVar cbv) $ - ((cbv, expansion) : top_env) :| rest_envs +addCycleBreakerBindings :: Bag (TcTyVar, Type) -- ^ (cbv,expansion) pairs + -> InertSet -> InertSet +addCycleBreakerBindings prs ics + = assertPpr (all (isCycleBreakerTyVar . fst) prs) (ppr prs) $ + ics { inert_cycle_breakers = add_to (inert_cycle_breakers ics) } + where + add_to (top_env :| rest_envs) = (prs `unionBags` top_env) :| rest_envs -- | Perform a monadic operation on all pairs in the top environment -- in the stack. diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs index a22c135d18..f3d0097f93 100644 --- a/compiler/GHC/Tc/Solver/Monad.hs +++ b/compiler/GHC/Tc/Solver/Monad.hs @@ -48,7 +48,7 @@ module GHC.Tc.Solver.Monad ( newWanted, newWantedNC, newWantedEvVarNC, newBoundEvVarId, - unifyTyVar, reportUnifications, touchabilityTest, TouchabilityTestResult(..), + unifyTyVar, reportUnifications, touchabilityAndShapeTest, setEvBind, setWantedEq, setWantedEvTerm, setEvBindIfWanted, newEvVar, newGivenEvVar, newGivenEvVars, @@ -115,13 +115,10 @@ module GHC.Tc.Solver.Monad ( getDefaultInfo, getDynFlags, getGlobalRdrEnvTcS, matchFam, matchFamTcM, checkWellStagedDFun, - pprEq, -- Smaller utils, re-exported from TcM - -- TODO (DV): these are only really used in the - -- instance matcher in GHC.Tc.Solver. I am wondering - -- if the whole instance matcher simply belongs - -- here + pprEq, - breakTyEqCycle_maybe, rewriterView + -- Enforcing invariants for type equalities + checkTypeEq, checkTouchableTyVarEq ) where import GHC.Prelude @@ -169,7 +166,6 @@ import GHC.Types.Name.Reader import GHC.Types.Var import GHC.Types.Var.Set import GHC.Types.Unique.Supply -import GHC.Types.Unique.Set (nonDetEltsUniqSet) import GHC.Unit.Module ( HasModule, getModule, extractModule ) import qualified GHC.Rename.Env as TcM @@ -188,15 +184,15 @@ import GHC.Utils.Misc( equalLength ) import GHC.Exts (oneShot) import Control.Monad import Data.IORef -import Data.List ( mapAccumL, partition, zip4 ) +import Data.List ( mapAccumL, zip4 ) import Data.Foldable import qualified Data.Semigroup as S #if defined(DEBUG) +import GHC.Types.Unique.Set (nonDetEltsUniqSet) import GHC.Data.Graph.Directed #endif - {- ********************************************************************* * * StopOrContinue @@ -1312,85 +1308,6 @@ reportUnifications (TcS thing_inside) ; TcM.updTcRef (tcs_unified env) (+ n_unifs) ; return (n_unifs, res) } -data TouchabilityTestResult - -- See Note [Solve by unification] in GHC.Tc.Solver.Interact - -- which points out that having TouchableSameLevel is just an optimisation; - -- we could manage with TouchableOuterLevel alone (suitably renamed) - = TouchableSameLevel - | TouchableOuterLevel [TcTyVar] -- Promote these - TcLevel -- ..to this level - | Untouchable - -instance Outputable TouchabilityTestResult where - ppr TouchableSameLevel = text "TouchableSameLevel" - ppr (TouchableOuterLevel tvs lvl) = text "TouchableOuterLevel" <> parens (ppr lvl <+> ppr tvs) - ppr Untouchable = text "Untouchable" - -touchabilityTest :: CtFlavour -> TcTyVar -> TcType -> TcS TouchabilityTestResult --- This is the key test for untouchability: --- See Note [Unification preconditions] in GHC.Tc.Utils.Unify --- and Note [Solve by unification] in GHC.Tc.Solver.Interact -touchabilityTest flav tv1 rhs - | flav /= Given -- See Note [Do not unify Givens] - , MetaTv { mtv_tclvl = tv_lvl, mtv_info = info } <- tcTyVarDetails tv1 - = do { can_continue_solving <- wrapTcS $ startSolvingByUnification info rhs - ; if not can_continue_solving - then return Untouchable - else - do { ambient_lvl <- getTcLevel - ; given_eq_lvl <- getInnermostGivenEqLevel - - ; if | tv_lvl `sameDepthAs` ambient_lvl - -> return TouchableSameLevel - - | tv_lvl `deeperThanOrSame` given_eq_lvl -- No intervening given equalities - , all (does_not_escape tv_lvl) free_skols -- No skolem escapes - -> return (TouchableOuterLevel free_metas tv_lvl) - - | otherwise - -> return Untouchable } } - | otherwise - = return Untouchable - where - (free_metas, free_skols) = partition isPromotableMetaTyVar $ - nonDetEltsUniqSet $ - tyCoVarsOfType rhs - - does_not_escape tv_lvl fv - | isTyVar fv = tv_lvl `deeperThanOrSame` tcTyVarLevel fv - | otherwise = True - -- Coercion variables are not an escape risk - -- If an implication binds a coercion variable, it'll have equalities, - -- so the "intervening given equalities" test above will catch it - -- Coercion holes get filled with coercions, so again no problem. - -{- Note [Do not unify Givens] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider this GADT match - data T a where - T1 :: T Int - ... - - f x = case x of - T1 -> True - ... - -So we get f :: T alpha[1] -> beta[1] - x :: T alpha[1] -and from the T1 branch we get the implication - forall[2] (alpha[1] ~ Int) => beta[1] ~ Bool - -Now, clearly we don't want to unify alpha:=Int! Yet at the moment we -process [G] alpha[1] ~ Int, we don't have any given-equalities in the -inert set, and hence there are no given equalities to make alpha untouchable. - -NB: if it were alpha[2] ~ Int, this argument wouldn't hold. But that -never happens: invariant (GivenInv) in Note [TcLevel invariants] -in GHC.Tc.Utils.TcType. - -Simple solution: never unify in Givens! --} - getDefaultInfo :: TcS ([Type], (Bool, Bool)) getDefaultInfo = wrapTcS TcM.tcGetDefaultTys @@ -2142,110 +2059,174 @@ unifyWanteds rewriters ctlocs roles rhss lhss = unify_wanteds rewriters $ zip4 c ************************************************************************ -} --- | Conditionally replace all type family applications in the RHS with fresh --- variables, emitting givens that relate the type family application to the --- variable. See Note [Type equality cycles] in GHC.Tc.Solver.Canonical. --- This only works under conditions as described in the Note; otherwise, returns --- Nothing. -breakTyEqCycle_maybe :: CtEvidence - -> CheckTyEqResult -- result of checkTypeEq - -> CanEqLHS - -> TcType -- RHS - -> TcS (Maybe ReductionN) - -- new RHS that doesn't have any type families -breakTyEqCycle_maybe (ctLocOrigin . ctEvLoc -> CycleBreakerOrigin _) _ _ _ - -- see Detail (7) of Note - = return Nothing - -breakTyEqCycle_maybe ev cte_result lhs rhs - | NomEq <- eq_rel +checkTouchableTyVarEq + :: CtEvidence + -> TcTyVar -- A touchable meta-tyvar + -> TcType -- The RHS + -> TcS (PuResult () Reduction) +-- Used for Nominal, Wanted equalities, with a touchable meta-tyvar on LHS +-- If checkTouchableTyVarEq tv ty = PuOK redn cts +-- then we can unify +-- tv := ty |> redn +-- with extra wanteds 'cts' +-- If it returns (PuFail reason) we can't unify, and the reason explains why. +checkTouchableTyVarEq ev lhs_tv rhs + | simpleUnifyCheck True lhs_tv rhs + -- True <=> type families are ok on the RHS + = do { traceTcS "checkTouchableTyVarEq: simple-check wins" (ppr lhs_tv $$ ppr rhs) + ; return (pure (mkReflRedn Nominal rhs)) } - , cte_result `cterHasOnlyProblem` cteSolubleOccurs - -- only do this if the only problem is a soluble occurs-check - -- See Detail (8) of the Note. + | otherwise + = do { traceTcS "checkTouchableTyVarEq {" (ppr lhs_tv $$ ppr rhs) + ; check_result <- wrapTcS (check_rhs rhs) + ; traceTcS "checkTouchableTyVarEq }" (ppr lhs_tv $$ ppr check_result) + ; case check_result of + PuFail reason -> return (PuFail reason) + PuOK redn cts -> do { emitWork (bagToList cts) + ; return (pure redn) } } - = do { should_break <- final_check - ; if should_break then do { redn <- go rhs - ; return (Just redn) } - else return Nothing } where - flavour = ctEvFlavour ev - eq_rel = ctEvEqRel ev - - final_check = case flavour of - Given -> return True - Wanted -- Wanteds work only with a touchable tyvar on the left - -- See "Wanted" section of the Note. - | TyVarLHS lhs_tv <- lhs -> - do { result <- touchabilityTest Wanted lhs_tv rhs - ; return $ case result of - Untouchable -> False - _ -> True } - | otherwise -> return False - - -- This could be considerably more efficient. See Detail (5) of Note. - go :: TcType -> TcS ReductionN - go ty | Just ty' <- rewriterView ty = go ty' - go (Rep.TyConApp tc tys) - | isTypeFamilyTyCon tc -- worried about whether this type family is not actually - -- causing trouble? See Detail (5) of Note. - = do { let (fun_args, extra_args) = splitAt (tyConArity tc) tys - fun_app = mkTyConApp tc fun_args - fun_app_kind = typeKind fun_app - ; fun_redn <- emit_work fun_app_kind fun_app - ; arg_redns <- unzipRedns <$> mapM go extra_args - ; return $ mkAppRedns fun_redn arg_redns } - -- Worried that this substitution will change kinds? - -- See Detail (3) of Note + (lhs_tv_info, lhs_tv_lvl) = case tcTyVarDetails lhs_tv of + MetaTv { mtv_info = info, mtv_tclvl = lvl } -> (info,lvl) + _ -> pprPanic "checkTouchableTyVarEq" (ppr lhs_tv) + -- lhs_tv should be a meta-tyvar + + is_concrete_lhs_tv = isConcreteInfo lhs_tv_info + + check_rhs rhs + -- Crucial special case for alpha ~ F tys + -- We don't want to flatten that (F tys)! + | Just (TyFamLHS tc tys) <- canTyFamEqLHS_maybe rhs + = if is_concrete_lhs_tv + then failCheckWith (cteProblem cteConcrete) + else recurseIntoTyConApp arg_flags tc tys + | otherwise + = checkTyEqRhs flags rhs + + flags = TEF { tef_foralls = False -- isRuntimeUnkSkol lhs_tv + , tef_fam_app = mkTEFA_Break ev NomEq break_wanted + , tef_unifying = Unifying lhs_tv_info lhs_tv_lvl LC_Promote + , tef_lhs = TyVarLHS lhs_tv + , tef_occurs = cteInsolubleOccurs } + + arg_flags = famAppArgFlags flags + + break_wanted fam_app + -- Occurs check or skolem escape; so flatten + = do { let fam_app_kind = typeKind fam_app + ; reason <- checkPromoteFreeVars cteInsolubleOccurs + lhs_tv lhs_tv_lvl (tyCoVarsOfType fam_app_kind) + ; if not (cterHasNoProblem reason) -- Failed to promote free vars + then failCheckWith reason + else + do { let tv_info | isConcreteInfo lhs_tv_info = lhs_tv_info + | otherwise = TauTv + -- Make a concrete tyvar if lhs_tv is concrete + -- e.g. alpha[2,conc] ~ Maybe (F beta[4]) + -- We want to flatten to + -- alpha[2,conc] ~ Maybe gamma[2,conc] + -- gamma[2,conc] ~ F beta[4] + ; new_tv_ty <- TcM.newMetaTyVarTyWithInfo lhs_tv_lvl tv_info fam_app_kind + ; let pty = mkPrimEqPredRole Nominal fam_app new_tv_ty + ; hole <- TcM.newCoercionHole pty + ; let new_ev = CtWanted { ctev_pred = pty + , ctev_dest = HoleDest hole + , ctev_loc = cb_loc + , ctev_rewriters = ctEvRewriters ev } + ; return (PuOK (mkReduction (HoleCo hole) new_tv_ty) + (singleCt (mkNonCanonical new_ev))) } } + + -- See Detail (7) of the Note + cb_loc = updateCtLocOrigin (ctEvLoc ev) CycleBreakerOrigin + +------------------------ +checkTypeEq :: CtEvidence -> EqRel -> CanEqLHS -> TcType + -> TcS (PuResult () Reduction) +-- Used for general CanEqLHSs, ones that do +-- not have a touchable type variable on the LHS (i.e. not unifying) +checkTypeEq ev eq_rel lhs rhs + | isGiven ev + = do { traceTcS "checkTypeEq {" (vcat [ text "lhs:" <+> ppr lhs + , text "rhs:" <+> ppr rhs ]) + ; check_result <- wrapTcS (check_given_rhs rhs) + ; traceTcS "checkTypeEq }" (ppr check_result) + ; case check_result of + PuFail reason -> return (PuFail reason) + PuOK redn prs -> do { new_givens <- mapBagM mk_new_given prs + ; emitWorkNC (bagToList new_givens) + ; updInertTcS (addCycleBreakerBindings prs) + ; return (pure redn) } } + + | otherwise -- Wanted + = do { check_result <- wrapTcS (checkTyEqRhs wanted_flags rhs) + ; case check_result of + PuFail reason -> return (PuFail reason) + PuOK redn cts -> do { emitWork (bagToList cts) + ; return (pure redn) } } + where + check_given_rhs rhs + -- See Note [Special case for top-level of Given equality] + | Just (TyFamLHS tc tys) <- canTyFamEqLHS_maybe rhs + = recurseIntoTyConApp arg_flags tc tys + | otherwise + = checkTyEqRhs given_flags rhs + + arg_flags = famAppArgFlags given_flags + + given_flags = TEF { tef_lhs = lhs + , tef_foralls = False + , tef_unifying = NotUnifying + , tef_fam_app = mkTEFA_Break ev eq_rel break_given + , tef_occurs = occ_prob } + -- TEFA_Break used for: [G] a ~ Maybe (F a) + -- or [W] F a ~ Maybe (F a) + + wanted_flags = TEF { tef_lhs = lhs + , tef_foralls = False + , tef_unifying = NotUnifying + , tef_fam_app = TEFA_Recurse + , tef_occurs = occ_prob } + -- TEFA_Recurse: see Note [Don't cycle-break Wanteds when not unifying] + + -- occ_prob: see Note [Occurs check and representational equality] + occ_prob = case eq_rel of + NomEq -> cteInsolubleOccurs + ReprEq -> cteSolubleOccurs + + break_given :: TcType -> TcM (PuResult (TcTyVar,TcType) Reduction) + break_given fam_app + = do { new_tv <- TcM.newCycleBreakerTyVar (typeKind fam_app) + ; return (PuOK (mkReflRedn Nominal (mkTyVarTy new_tv)) + (unitBag (new_tv, fam_app))) } + -- Why reflexive? See Detail (4) of the Note + + --------------------------- + mk_new_given :: (TcTyVar, TcType) -> TcS CtEvidence + mk_new_given (new_tv, fam_app) + = newGivenEvVar cb_loc (given_pred, given_term) + where + new_ty = mkTyVarTy new_tv + given_pred = mkPrimEqPred fam_app new_ty + given_term = evCoercion $ mkNomReflCo new_ty -- See Detail (4) of Note - | otherwise - = do { arg_redns <- unzipRedns <$> mapM go tys - ; return $ mkTyConAppRedn Nominal tc arg_redns } - - go (Rep.AppTy ty1 ty2) - = mkAppRedn <$> go ty1 <*> go ty2 - go (Rep.FunTy vis w arg res) - = mkFunRedn Nominal vis <$> go w <*> go arg <*> go res - go (Rep.CastTy ty cast_co) - = mkCastRedn1 Nominal ty cast_co <$> go ty - go ty@(Rep.TyVarTy {}) = skip ty - go ty@(Rep.LitTy {}) = skip ty - go ty@(Rep.ForAllTy {}) = skip ty -- See Detail (1) of Note - go ty@(Rep.CoercionTy {}) = skip ty -- See Detail (2) of Note - - skip ty = return $ mkReflRedn Nominal ty - - emit_work :: TcKind -- of the function application - -> TcType -- original function application - -> TcS ReductionN -- rewritten type (the fresh tyvar) - emit_work fun_app_kind fun_app = case flavour of - Given -> - do { new_tv <- wrapTcS (TcM.newCycleBreakerTyVar fun_app_kind) - ; let new_ty = mkTyVarTy new_tv - given_pred = mkHeteroPrimEqPred fun_app_kind fun_app_kind - fun_app new_ty - given_term = evCoercion $ mkNomReflCo new_ty -- See Detail (4) of Note - ; new_given <- newGivenEvVar new_loc (given_pred, given_term) - ; traceTcS "breakTyEqCycle replacing type family in Given" (ppr new_given) - ; emitWorkNC [new_given] - ; updInertTcS $ \is -> - is { inert_cycle_breakers = insertCycleBreakerBinding new_tv fun_app - (inert_cycle_breakers is) } - ; return $ mkReflRedn Nominal new_ty } - -- Why reflexive? See Detail (4) of the Note - - Wanted -> - do { new_tv <- wrapTcS (TcM.newFlexiTyVar fun_app_kind) - ; let new_ty = mkTyVarTy new_tv - ; co <- emitNewWantedEq new_loc (ctEvRewriters ev) Nominal new_ty fun_app - ; return $ mkReduction (mkSymCo co) new_ty } - - -- See Detail (7) of the Note - new_loc = updateCtLocOrigin (ctEvLoc ev) CycleBreakerOrigin - --- does not fit scenario from Note -breakTyEqCycle_maybe _ _ _ _ = return Nothing + -- See Detail (7) of the Note + cb_loc = updateCtLocOrigin (ctEvLoc ev) CycleBreakerOrigin + +mkTEFA_Break :: CtEvidence -> EqRel -> FamAppBreaker a -> TyEqFamApp a +mkTEFA_Break ev eq_rel breaker + | NomEq <- eq_rel + , not cycle_breaker_origin + = TEFA_Break breaker + | otherwise + = TEFA_Recurse + where + -- cycle_breaker_origin: see Detail (7) of Note [Type equality cycles] + -- in GHC.Tc.Solver.Equality + cycle_breaker_origin = case ctLocOrigin (ctEvLoc ev) of + CycleBreakerOrigin {} -> True + _ -> False +------------------------- -- | Fill in CycleBreakerTvs with the variables they stand for. -- See Note [Type equality cycles] in GHC.Tc.Solver.Canonical. restoreTyVarCycles :: InertSet -> TcM () @@ -2254,12 +2235,74 @@ restoreTyVarCycles is {-# SPECIALISE forAllCycleBreakerBindings_ :: CycleBreakerVarStack -> (TcTyVar -> TcType -> TcM ()) -> TcM () #-} --- Unwrap a type synonym only when either: --- The type synonym is forgetful, or --- the type synonym mentions a type family in its expansion --- See Note [Rewriting synonyms] in GHC.Tc.Solver.Rewrite. -rewriterView :: TcType -> Maybe TcType -rewriterView ty@(Rep.TyConApp tc _) - | isForgetfulSynTyCon tc || (isTypeSynonymTyCon tc && not (isFamFreeTyCon tc)) - = coreView ty -rewriterView _other = Nothing + +{- Note [Occurs check and representational equality] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +(a ~R# b a) is soluble if b later turns out to be Identity +So we treat this as a "soluble occurs check". + +Note [Special case for top-level of Given equality] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We take care when examining + [G] F ty ~ G (...(F ty)...) +where both sides are TyFamLHSs. We don't want to flatten that RHS to + [G] F ty ~ cbv + [G] G (...(F ty)...) ~ cbv +Instead we'd like to say "occurs-check" and swap LHS and RHS, which yields a +canonical constraint + [G] G (...(F ty)...) ~ F ty +That tents to rewrite a big type to smaller one. This happens in T15703, +where we had: + [G] Pure g ~ From1 (To1 (Pure g)) +Making a loop breaker and rewriting left to right just makes much bigger +types than swapping it over. + +(We might hope to have swapped it over before getting to checkTypeEq, +but better safe than sorry.) + +NB: We never see a TyVarLHS here, such as + [G] a ~ F tys here +because we'd have swapped it to + [G] F tys ~ a +in canEqCanLHS2, before getting to checkTypeEq. + +Note [Don't cycle-break Wanteds when not unifying] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consdier + [W] a[2] ~ Maybe (F a[2]) + +Should we cycle-break this Wanted, thus? + + [W] a[2] ~ Maybe delta[2] + [W] delta[2] ~ F a[2] + +For a start, this is dodgy because we might just unify delta, thus undoing +what we have done, and getting an infinite loop in the solver. Even if we +somehow prevented ourselves from doing so, is there any merit in the split? +Maybe: perhaps we can use that equality on `a` to unlock other constraints? +Consider + type instance F (Maybe _) = Bool + + [G] g1: a ~ Maybe Bool + [W] w1: a ~ Maybe (F a) + +If we loop-break w1 to get + [W] w1': a ~ Maybe gamma + [W] w3: gamma ~ F a +Now rewrite w3 with w1' + [W] w3': gamma ~ F (Maybe gamma) +Now use the type instance to get + gamma := Bool +Now we are left with + [W] w1': a ~ Maybe Bool +which we can solve from the Given. + +BUT in this situation we could have rewritten the +/original/ Wanted from the Given, like this: + [W] w1': Maybe Bool ~ Maybe (F (Maybe Bool)) +and that is readily soluble. + +In short: loop-breaking Wanteds, when we aren't unifying, +seems of no merit. Hence TEFA_Recurse, rather than TEFA_Break, +in `wanted_flags` in `checkTypeEq`. +-}
\ No newline at end of file diff --git a/compiler/GHC/Tc/Types/Constraint.hs b/compiler/GHC/Tc/Types/Constraint.hs index a2e84ab7dc..4814c63280 100644 --- a/compiler/GHC/Tc/Types/Constraint.hs +++ b/compiler/GHC/Tc/Types/Constraint.hs @@ -34,14 +34,16 @@ module GHC.Tc.Types.Constraint ( CtIrredReason(..), isInsolubleReason, CheckTyEqResult, CheckTyEqProblem, cteProblem, cterClearOccursCheck, - cteOK, cteImpredicative, cteTypeFamily, + cteOK, cteImpredicative, cteTypeFamily, cteCoercionHole, cteInsolubleOccurs, cteSolubleOccurs, cterSetOccursCheckSoluble, + cteConcrete, cteSkolemEscape, + impredicativeProblem, insolubleOccursProblem, solubleOccursProblem, - cterHasNoProblem, cterHasProblem, cterHasOnlyProblem, + cterHasNoProblem, cterHasProblem, cterHasOnlyProblem, cterHasOnlyProblems, cterRemoveProblem, cterHasOccursCheck, cterFromKind, - CanEqLHS(..), canEqLHS_maybe, canEqLHSKind, canEqLHSType, - eqCanEqLHS, + CanEqLHS(..), canEqLHS_maybe, canTyFamEqLHS_maybe, + canEqLHSKind, canEqLHSType, eqCanEqLHS, Hole(..), HoleSort(..), isOutOfScopeHole, DelayedError(..), NotConcreteError(..), @@ -148,38 +150,6 @@ import Data.List ( intersperse ) * These are the constraints the low-level simplifier works with * * * ************************************************************************ - -Note [CEqCan occurs check] -~~~~~~~~~~~~~~~~~~~~~~~~~~ -A CEqCan relates a CanEqLHS (a type variable or type family applications) on -its left to an arbitrary type on its right. It is used for rewriting. -Because it is used for rewriting, it would be disastrous if the RHS -were to mention the LHS: this would cause a loop in rewriting. - -We thus perform an occurs-check. There is, of course, some subtlety: - -* For type variables, the occurs-check looks deeply. This is because - a CEqCan over a meta-variable is also used to inform unification, - in GHC.Tc.Solver.Interact.solveByUnification. If the LHS appears - anywhere, at all, in the RHS, unification will create an infinite - structure, which is bad. - -* For type family applications, the occurs-check is shallow; it looks - only in places where we might rewrite. (Specifically, it does not - look in kinds or coercions.) An occurrence of the LHS in, say, an - RHS coercion is OK, as we do not rewrite in coercions. No loop to - be found. - - You might also worry about the possibility that a type family - application LHS doesn't exactly appear in the RHS, but something - that reduces to the LHS does. Yet that can't happen: the RHS is - already inert, with all type family redexes reduced. So a simple - syntactic check is just fine. - -The occurs check is performed in GHC.Tc.Utils.Unify.checkTypeEq -and forms condition T3 in Note [Extending the inert equalities] -in GHC.Tc.Solver.InertSet. - -} -- | A 'Xi'-type is one that has been fully rewritten with respect @@ -265,22 +235,54 @@ data Ct {- Note [Invariants of EqCt] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -An EqCt carries a canonical equality constraint, that satisfies these invariants: - * See Note [inert_eqs: the inert equalities] in GHC.Tc.Solver.InertSet - * Many are checked in checkTypeEq in GHC.Tc.Utils.Unify +An EqCt is a canonical equality constraint, one that can live in the inert set, +and that can be used to rewrite other constrtaints. It satisfies these invariants: * (TyEq:OC) lhs does not occur in rhs (occurs check) - Note [CEqCan occurs check] + Note [EqCt occurs check] * (TyEq:F) rhs has no foralls (this avoids substituting a forall for the tyvar in other types) * (TyEq:K) typeKind lhs `tcEqKind` typeKind rhs; Note [Ct kind invariant] * (TyEq:N) If the equality is representational, rhs is not headed by a saturated - application of a newtype TyCon. - See Note [No top-level newtypes on RHS of representational equalities] - in GHC.Tc.Solver.Canonical. (Applies only when constructor of newtype is - in scope.) - * (TyEq:TV) If rhs (perhaps under a cast) is also CanEqLHS, then it is oriented - to give best chance of unification happening; eg if rhs is touchable then lhs is too - Note [TyVar/TyVar orientation] in GHC.Tc.Utils.Unify + application of a newtype TyCon. See GHC.Tc.Solver.Equality + Note [No top-level newtypes on RHS of representational equalities]. + (Applies only when constructor of newtype is in scope.) + * (TyEq:U) An EqCt is not immediately unifiable. If we can unify a:=ty, we + will not form an EqCt (a ~ ty). + +These invariants ensure that the EqCts in inert_eqs constitute a terminating +generalised substitution. See Note [inert_eqs: the inert equalities] +in GHC.Tc.Solver.InertSet for what these words mean! + +Note [EqCt occurs check] +~~~~~~~~~~~~~~~~~~~~~~~~~~ +A CEqCan relates a CanEqLHS (a type variable or type family applications) on +its left to an arbitrary type on its right. It is used for rewriting. +Because it is used for rewriting, it would be disastrous if the RHS +were to mention the LHS: this would cause a loop in rewriting. + +We thus perform an occurs-check. There is, of course, some subtlety: + +* For type variables, the occurs-check looks deeply. This is because + a CEqCan over a meta-variable is also used to inform unification, + in GHC.Tc.Solver.Interact.solveByUnification. If the LHS appears + anywhere, at all, in the RHS, unification will create an infinite + structure, which is bad. + +* For type family applications, the occurs-check is shallow; it looks + only in places where we might rewrite. (Specifically, it does not + look in kinds or coercions.) An occurrence of the LHS in, say, an + RHS coercion is OK, as we do not rewrite in coercions. No loop to + be found. + + You might also worry about the possibility that a type family + application LHS doesn't exactly appear in the RHS, but something + that reduces to the LHS does. Yet that can't happen: the RHS is + already inert, with all type family redexes reduced. So a simple + syntactic check is just fine. + +The occurs check is performed in GHC.Tc.Utils.Unify.checkTyEqRhs +and forms condition T3 in Note [Extending the inert equalities] +in GHC.Tc.Solver.InertSet. -} data EqCt -- An equality constraint; see Note [Invariants of EqCt] @@ -293,11 +295,11 @@ data EqCt -- An equality constraint; see Note [Invariants of EqCt] ------------ -- | A 'CanEqLHS' is a type that can appear on the left of a canonical --- equality: a type variable or exactly-saturated type family application. +-- equality: a type variable or /exactly-saturated/ type family application. data CanEqLHS = TyVarLHS TcTyVar - | TyFamLHS TyCon -- ^ of the family - [Xi] -- ^ exactly saturating the family + | TyFamLHS TyCon -- ^ TyCon of the family + [Xi] -- ^ Arguments, /exactly saturating/ the family instance Outputable CanEqLHS where ppr (TyVarLHS tv) = ppr tv @@ -478,7 +480,7 @@ isInsolubleReason AbstractTyConReason = True -- ------------------------------------------------------------------------------ --- | A set of problems in checking the validity of a type equality. +-- | A /set/ of problems in checking the validity of a type equality. -- See 'checkTypeEq'. newtype CheckTyEqResult = CTER Word8 @@ -491,20 +493,35 @@ cterHasNoProblem :: CheckTyEqResult -> Bool cterHasNoProblem (CTER 0) = True cterHasNoProblem _ = False --- | An individual problem that might be logged in a 'CheckTyEqResult' +-- | An /individual/ problem that might be logged in a 'CheckTyEqResult' newtype CheckTyEqProblem = CTEP Word8 -cteImpredicative, cteTypeFamily, cteInsolubleOccurs, cteSolubleOccurs :: CheckTyEqProblem -cteImpredicative = CTEP (bit 0) -- forall or (=>) encountered -cteTypeFamily = CTEP (bit 1) -- type family encountered -cteInsolubleOccurs = CTEP (bit 2) -- occurs-check -cteSolubleOccurs = CTEP (bit 3) -- occurs-check under a type function or in a coercion - -- must be one bit to the left of cteInsolubleOccurs --- See also Note [Insoluble occurs check] in GHC.Tc.Errors +cteImpredicative, cteTypeFamily, cteInsolubleOccurs, + cteSolubleOccurs, cteCoercionHole, cteConcrete, + cteSkolemEscape :: CheckTyEqProblem +cteImpredicative = CTEP (bit 0) -- Forall or (=>) encountered +cteTypeFamily = CTEP (bit 1) -- Type family encountered + +cteInsolubleOccurs = CTEP (bit 2) -- Occurs-check +cteSolubleOccurs = CTEP (bit 3) -- Occurs-check under a type function, or in a coercion, + -- or in a representational equality; see + -- See Note [Occurs check and representational equality] + -- cteSolubleOccurs must be one bit to the left of cteInsolubleOccurs + -- See also Note [Insoluble occurs check] in GHC.Tc.Errors + +cteCoercionHole = CTEP (bit 4) -- Coercion hole encountered +cteConcrete = CTEP (bit 5) -- Type variable that can't be made concrete + -- e.g. alpha[conc] ~ Maybe beta[tv] +cteSkolemEscape = CTEP (bit 6) -- Skolem escape e.g. alpha[2] ~ b[sk,4] cteProblem :: CheckTyEqProblem -> CheckTyEqResult cteProblem (CTEP mask) = CTER mask +impredicativeProblem, insolubleOccursProblem, solubleOccursProblem :: CheckTyEqResult +impredicativeProblem = cteProblem cteImpredicative +insolubleOccursProblem = cteProblem cteInsolubleOccurs +solubleOccursProblem = cteProblem cteSolubleOccurs + occurs_mask :: Word8 occurs_mask = insoluble_mask .|. soluble_mask where @@ -519,6 +536,9 @@ CTER bits `cterHasProblem` CTEP mask = (bits .&. mask) /= 0 cterHasOnlyProblem :: CheckTyEqResult -> CheckTyEqProblem -> Bool CTER bits `cterHasOnlyProblem` CTEP mask = bits == mask +cterHasOnlyProblems :: CheckTyEqResult -> CheckTyEqResult -> Bool +CTER bits `cterHasOnlyProblems` CTER mask = (bits .&. complement mask) == 0 + cterRemoveProblem :: CheckTyEqResult -> CheckTyEqProblem -> CheckTyEqResult cterRemoveProblem (CTER bits) (CTEP mask) = CTER (bits .&. complement mask) @@ -555,18 +575,31 @@ instance Semigroup CheckTyEqResult where instance Monoid CheckTyEqResult where mempty = cteOK +instance Eq CheckTyEqProblem where + (CTEP b1) == (CTEP b2) = b1==b2 + +instance Outputable CheckTyEqProblem where + ppr prob@(CTEP bits) = case lookup prob allBits of + Just s -> text s + Nothing -> text "unknown:" <+> ppr bits + instance Outputable CheckTyEqResult where - ppr cter | cterHasNoProblem cter = text "cteOK" + ppr cter | cterHasNoProblem cter + = text "cteOK" | otherwise - = parens $ fcat $ intersperse vbar $ set_bits - where - all_bits = [ (cteImpredicative, "cteImpredicative") - , (cteTypeFamily, "cteTypeFamily") - , (cteInsolubleOccurs, "cteInsolubleOccurs") - , (cteSolubleOccurs, "cteSolubleOccurs") ] - set_bits = [ text str - | (bitmask, str) <- all_bits - , cter `cterHasProblem` bitmask ] + = braces $ fcat $ intersperse vbar $ + [ text str + | (bitmask, str) <- allBits + , cter `cterHasProblem` bitmask ] + +allBits :: [(CheckTyEqProblem, String)] +allBits = [ (cteImpredicative, "cteImpredicative") + , (cteTypeFamily, "cteTypeFamily") + , (cteInsolubleOccurs, "cteInsolubleOccurs") + , (cteSolubleOccurs, "cteSolubleOccurs") + , (cteConcrete, "cteConcrete") + , (cteSkolemEscape, "cteSkolemEscape") + , (cteCoercionHole, "cteCoercionHole") ] {- Note [CIrredCan constraints] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -735,6 +768,11 @@ canEqLHS_maybe xi | Just tv <- getTyVar_maybe xi = Just $ TyVarLHS tv + | otherwise + = canTyFamEqLHS_maybe xi + +canTyFamEqLHS_maybe :: Xi -> Maybe CanEqLHS +canTyFamEqLHS_maybe xi | Just (tc, args) <- tcSplitTyConApp_maybe xi , isTypeFamilyTyCon tc , args `lengthIs` tyConArity tc @@ -1193,11 +1231,11 @@ nonDefaultableTyVarsOfWC (WC { wc_simple = simples, wc_impl = implics, wc_errors EqPred NomEq lhs rhs | Just tv <- getTyVar_maybe lhs , isConcreteTyVar tv - , not (isConcrete rhs) + , not (isConcreteType rhs) -> unitVarSet tv | Just tv <- getTyVar_maybe rhs , isConcreteTyVar tv - , not (isConcrete lhs) + , not (isConcreteType lhs) -> unitVarSet tv _ -> emptyVarSet diff --git a/compiler/GHC/Tc/Utils/Concrete.hs b/compiler/GHC/Tc/Utils/Concrete.hs index d69a3c473a..fe0f261005 100644 --- a/compiler/GHC/Tc/Utils/Concrete.hs +++ b/compiler/GHC/Tc/Utils/Concrete.hs @@ -22,7 +22,7 @@ import GHC.Core.Coercion ( coToMCo, mkCastTyMCo , mkGReflRightMCo, mkNomReflCo ) import GHC.Core.TyCo.Rep ( Type(..), MCoercion(..) ) import GHC.Core.TyCon ( isConcreteTyCon ) -import GHC.Core.Type ( isConcrete, typeKind, tyVarKind, coreView +import GHC.Core.Type ( isConcreteType, typeKind, tyVarKind, coreView , mkTyVarTy, mkTyConApp, mkFunTy, mkAppTy ) import GHC.Tc.Types ( TcM, ThStage(..), PendingStuff(..) ) @@ -87,7 +87,7 @@ as a central point of reference for this topic. Note [The Concrete mechanism] Instead of simply checking that a type `ty` is concrete (i.e. computing - 'isConcrete`), we emit an equality constraint: + 'isConcreteType`), we emit an equality constraint: co :: ty ~# concrete_ty @@ -183,7 +183,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 -GHC.Core.Type.isConcrete checks whether a type meets this definition. +GHC.Core.Type.isConcreteType checks whether a type meets this definition. Definition: a /concrete type constructor/ is defined by - a promoted data constructor @@ -627,8 +627,6 @@ makeTypeConcrete :: ConcreteTvOrigin -> TcType -> TcM (TcType, [NotConcreteReaso -- 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" $ @@ -640,7 +638,7 @@ makeTypeConcrete conc_orig ty = go ty | Just ty <- coreView ty = go ty - | isConcrete ty + | isConcreteType ty = pure ty go ty@(TyVarTy tv) -- not a ConcreteTv (already handled above) = do { mb_filled <- lift $ isFilledMetaTyVar_maybe tv diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs index 46643a4c8d..b4971210fd 100644 --- a/compiler/GHC/Tc/Utils/TcMType.hs +++ b/compiler/GHC/Tc/Utils/TcMType.hs @@ -23,8 +23,10 @@ module GHC.Tc.Utils.TcMType ( newFlexiTyVarTys, -- Int -> Kind -> TcM [TcType] newOpenFlexiTyVar, newOpenFlexiTyVarTy, newOpenTypeKind, newOpenBoxedTypeKind, - newMetaKindVar, newMetaKindVars, newMetaTyVarTyAtLevel, - newAnonMetaTyVar, newConcreteTyVar, cloneMetaTyVar, + newMetaKindVar, newMetaKindVars, + newMetaTyVarTyAtLevel, newMetaTyVarTyWithInfo, + newAnonMetaTyVar, newConcreteTyVar, + cloneMetaTyVar, cloneMetaTyVarWithInfo, newCycleBreakerTyVar, newMultiplicityVar, @@ -823,7 +825,7 @@ cloneTyVarTyVar name kind newConcreteTyVar :: HasDebugCallStack => ConcreteTvOrigin -> FastString -> TcKind -> TcM TcTyVar newConcreteTyVar reason fs kind - = assertPpr (isConcrete kind) assert_msg $ + = assertPpr (isConcreteType kind) assert_msg $ newNamedAnonMetaTyVar fs (ConcreteTv reason) kind where assert_msg = text "newConcreteTyVar: non-concrete kind" <+> ppr kind @@ -884,6 +886,18 @@ cloneMetaTyVar tv ; traceTc "cloneMetaTyVar" (ppr tyvar) ; return tyvar } +cloneMetaTyVarWithInfo :: MetaInfo -> TcLevel -> TcTyVar -> TcM TcTyVar +cloneMetaTyVarWithInfo info tc_lvl tv + = assert (isTcTyVar tv) $ + do { ref <- newMutVar Flexi + ; name' <- cloneMetaTyVarName (tyVarName tv) + ; let details = MetaTv { mtv_info = info + , mtv_ref = ref + , mtv_tclvl = tc_lvl } + tyvar = mkTcTyVar name' (tyVarKind tv) details + ; traceTc "cloneMetaTyVarWithInfo" (ppr tyvar) + ; return tyvar } + -- Works for both type and kind variables readMetaTyVar :: TyVar -> TcM MetaDetails readMetaTyVar tyvar = assertPpr (isMetaTyVar tyvar) (ppr tyvar) $ @@ -955,7 +969,7 @@ writeMetaTyVarRef tyvar ref ty ; let zonked_ty_kind = typeKind zonked_ty zonked_ty_lvl = tcTypeLevel zonked_ty level_check_ok = not (zonked_ty_lvl `strictlyDeeperThan` tv_lvl) - level_check_msg = ppr zonked_ty_lvl $$ ppr tv_lvl $$ ppr tyvar $$ ppr ty + level_check_msg = ppr zonked_ty_lvl $$ ppr tv_lvl $$ ppr tyvar $$ ppr ty $$ ppr zonked_ty kind_check_ok = zonked_ty_kind `eqType` zonked_tv_kind -- Note [Extra-constraint holes in partial type signatures] in GHC.Tc.Gen.HsType @@ -1100,6 +1114,15 @@ newMetaTyVarTyAtLevel tc_lvl kind ; name <- newMetaTyVarName (fsLit "p") ; return (mkTyVarTy (mkTcTyVar name kind details)) } +newMetaTyVarTyWithInfo :: TcLevel -> MetaInfo -> TcKind -> TcM TcType +newMetaTyVarTyWithInfo tc_lvl info kind + = do { ref <- newMutVar Flexi + ; let details = MetaTv { mtv_info = info + , mtv_ref = ref + , mtv_tclvl = tc_lvl } + ; name <- newMetaTyVarName (fsLit "p") + ; return (mkTyVarTy (mkTcTyVar name kind details)) } + {- ********************************************************************* * * Finding variables to quantify over diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs index 67b19c032a..db546edfd4 100644 --- a/compiler/GHC/Tc/Utils/TcType.hs +++ b/compiler/GHC/Tc/Utils/TcType.hs @@ -38,7 +38,7 @@ module GHC.Tc.Utils.TcType ( -- TcLevel TcLevel(..), topTcLevel, pushTcLevel, isTopTcLevel, strictlyDeeperThan, deeperThanOrSame, sameDepthAs, - tcTypeLevel, tcTyVarLevel, maxTcLevel, + tcTypeLevel, tcTyVarLevel, maxTcLevel, minTcLevel, -------------------------------- -- MetaDetails @@ -47,7 +47,7 @@ module GHC.Tc.Utils.TcType ( isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isMetaTyVarTy, isTyVarTy, tcIsTcTyVar, isTyVarTyVar, isOverlappableTyVar, isTyConableTyVar, ConcreteTvOrigin(..), isConcreteTyVar_maybe, isConcreteTyVar, - isConcreteTyVarTy, isConcreteTyVarTy_maybe, + isConcreteTyVarTy, isConcreteTyVarTy_maybe, isConcreteInfo, isAmbiguousTyVar, isCycleBreakerTyVar, metaTyVarRef, metaTyVarInfo, isFlexi, isIndirect, isRuntimeUnkSkol, metaTyVarTcLevel, setMetaTyVarTcLevel, metaTyVarTcLevel_maybe, @@ -653,7 +653,7 @@ data MetaDetails | Indirect TcType -- | What restrictions are on this metavariable around unification? --- These are checked in GHC.Tc.Utils.Unify.startSolvingByUnification. +-- These are checked in GHC.Tc.Utils.Unify.checkTopShape data MetaInfo = TauTv -- ^ This MetaTv is an ordinary unification variable -- A TauTv is always filled in with a tau-type, which @@ -715,6 +715,9 @@ Note [TcLevel invariants] and each Implication has a level number (of type TcLevel) +* INVARIANT (KindInv) Given a type variable (tv::ki) at at level L, + the free vars of `ki` all have level <= L + * INVARIANTS. In a tree of Implications, (ImplicInv) The level number (ic_tclvl) of an Implication is @@ -797,6 +800,9 @@ touchable; but then 'b' has escaped its scope into the outer implication. maxTcLevel :: TcLevel -> TcLevel -> TcLevel maxTcLevel (TcLevel a) (TcLevel b) = TcLevel (a `max` b) +minTcLevel :: TcLevel -> TcLevel -> TcLevel +minTcLevel (TcLevel a) (TcLevel b) = TcLevel (a `min` b) + topTcLevel :: TcLevel -- See Note [TcLevel assignment] topTcLevel = TcLevel 0 -- 0 = outermost level @@ -1200,6 +1206,10 @@ isConcreteTyVar_maybe tv | otherwise = Nothing +isConcreteInfo :: MetaInfo -> Bool +isConcreteInfo (ConcreteTv {}) = True +isConcreteInfo _ = False + -- | Is this type variable a concrete type variable, i.e. -- it is a metavariable with 'ConcreteTv' 'MetaInfo'? isConcreteTyVar :: TcTyVar -> Bool diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs index eea0ed95ef..fc5728cc81 100644 --- a/compiler/GHC/Tc/Utils/Unify.hs +++ b/compiler/GHC/Tc/Utils/Unify.hs @@ -1,6 +1,8 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TupleSections #-} {-# LANGUAGE RecursiveDo #-} +{-# LANGUAGE MultiWayIf #-} +{-# LANGUAGE RecordWildCards #-} {- (c) The University of Glasgow 2006 @@ -20,7 +22,7 @@ module GHC.Tc.Utils.Unify ( -- Various unifications unifyType, unifyKind, unifyExpectedType, uType, promoteTcType, - swapOverTyVars, startSolvingByUnification, + swapOverTyVars, touchabilityAndShapeTest, -------------------------------- -- Holes @@ -32,51 +34,58 @@ module GHC.Tc.Utils.Unify ( matchExpectedFunKind, matchActualFunTySigma, matchActualFunTysRho, - checkTyVarEq, checkTyFamEq, checkTypeEq - + checkTyEqRhs, recurseIntoTyConApp, + PuResult(..), failCheckWith, okCheckRefl, mapCheck, + TyEqFlags(..), TyEqFamApp(..), AreUnifying(..), LevelCheck(..), FamAppBreaker, + famAppArgFlags, simpleUnifyCheck, checkPromoteFreeVars, ) where import GHC.Prelude import GHC.Hs -import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep, makeTypeConcrete, hasFixedRuntimeRep_syntactic ) +import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep, hasFixedRuntimeRep_syntactic ) import GHC.Tc.Utils.Env import GHC.Tc.Utils.Instantiate import GHC.Tc.Utils.Monad import GHC.Tc.Utils.TcMType import GHC.Tc.Utils.TcType +import GHC.Tc.Types.Evidence +import GHC.Tc.Types.Constraint +import GHC.Tc.Types.Origin +import GHC.Types.Name( Name, isSystemName ) + import GHC.Core.Type import GHC.Core.TyCo.Rep -import GHC.Core.TyCo.Ppr( debugPprType ) +import GHC.Core.TyCo.FVs( isInjectiveInType ) +import GHC.Core.TyCo.Ppr( debugPprType {- pprTyVar -} ) import GHC.Core.TyCon import GHC.Core.Coercion import GHC.Core.Multiplicity +import GHC.Core.Reduction import qualified GHC.LanguageExtensions as LangExt -import GHC.Tc.Types.Evidence -import GHC.Tc.Types.Constraint -import GHC.Tc.Types.Origin -import GHC.Types.Name( Name, isSystemName ) - import GHC.Builtin.Types import GHC.Types.Var as Var import GHC.Types.Var.Set import GHC.Types.Var.Env -import GHC.Utils.Error -import GHC.Driver.Session import GHC.Types.Basic -import GHC.Data.Bag -import GHC.Data.FastString( fsLit ) +import GHC.Types.Unique.Set (nonDetEltsUniqSet) + +import GHC.Utils.Error import GHC.Utils.Misc import GHC.Utils.Outputable as Outputable import GHC.Utils.Panic import GHC.Utils.Panic.Plain -import GHC.Exts ( inline ) +import GHC.Driver.Session +import GHC.Data.Bag +import GHC.Data.FastString( fsLit ) + import Control.Monad +import Data.Monoid as DM ( Any(..) ) import qualified Data.Semigroup as S ( (<>) ) {- ********************************************************************* @@ -1053,11 +1062,9 @@ definitely_poly ty | (tvs, theta, tau) <- tcSplitSigmaTy ty , (tv:_) <- tvs -- At least one tyvar , null theta -- No constraints; see (DP1) - , checkTyVarEq tv tau `cterHasProblem` cteInsolubleOccurs + , tv `isInjectiveInType` tau -- The tyvar actually occurs (DP2), - -- and occurs in an injective position (DP3). - -- Fortunately checkTyVarEq, used for the occur check, - -- is just what we need. + -- and occurs in an injective position (DP3). = True | otherwise = False @@ -2065,37 +2072,31 @@ uUnfilledVar2 :: CtOrigin -> TcM Coercion uUnfilledVar2 origin t_or_k swapped tv1 ty2 = do { cur_lvl <- getTcLevel - ; go cur_lvl } - where - go cur_lvl - | isTouchableMetaTyVar cur_lvl tv1 -- See Note [Unification preconditions], (UNTOUCHABLE) wrinkles - , cterHasNoProblem (checkTyVarEq tv1 ty2) - -- See Note [Prevent unification with type families] - = 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 (typeKind ty2) (tyVarKind tv1) - ; traceTc "uUnfilledVar2 ok" $ - vcat [ ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1) - , ppr ty2 <+> dcolon <+> ppr (typeKind ty2) - , ppr (isReflCo co_k), ppr co_k ] - - ; if isReflCo co_k - -- Only proceed if the kinds match - -- NB: tv1 should still be unfilled, despite the kind unification - -- because tv1 is not free in ty2 (or, hence, in its kind) - then do { writeMetaTyVar tv1 ty2 - ; return (mkNomReflCo 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 - - | otherwise - = not_ok_so_defer - + -- Here we don't know about given equalities here; so we treat + -- /any/ level outside this one as untouchable. Hence cur_lvl. + ; if not (touchabilityAndShapeTest cur_lvl tv1 ty2 + && simpleUnifyCheck False tv1 ty2) + then not_ok_so_defer + else + do { co_k <- uType KindLevel kind_origin (typeKind ty2) (tyVarKind tv1) + ; traceTc "uUnfilledVar2 ok" $ + vcat [ ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1) + , ppr ty2 <+> dcolon <+> ppr (typeKind ty2) + , ppr (isReflCo co_k), ppr co_k ] + + ; if isReflCo co_k + -- Only proceed if the kinds match + -- NB: tv1 should still be unfilled, despite the kind unification + -- because tv1 is not free in ty2' (or, hence, in its kind) + then do { writeMetaTyVar tv1 ty2 + ; return (mkNomReflCo 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 + }} + where ty1 = mkTyVarTy tv1 kind_origin = KindEqOrigin ty1 ty2 origin (Just t_or_k) @@ -2108,43 +2109,6 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2 -- 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. -startSolvingByUnification :: MetaInfo -> TcType -- zonked - -> TcM Bool -startSolvingByUnification _ xi - | hasCoercionHoleTy xi -- (COERCION-HOLE) check - = return False -startSolvingByUnification info xi - = case info of - 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 getTyVar_maybe xi of - Nothing -> return False - Just tv -> - case tcTyVarDetails tv of -- (TYVAR-TV) wrinkle - SkolemTv {} -> return True - RuntimeUnk -> return True - MetaTv { mtv_info = info } -> - case info of - TyVarTv -> return True - _ -> return False - _ -> return True - swapOverTyVars :: Bool -> TcTyVar -> TcTyVar -> Bool swapOverTyVars is_given tv1 tv2 -- See Note [Unification variables on the left] @@ -2265,7 +2229,7 @@ There are five reasons not to unify: We thus simply do not unify in this case. This is expanded as Wrinkle (2) in Note [Equalities with incompatible kinds] - in GHC.Tc.Solver.Canonical. + in GHC.Tc.Solver.Equality Needless to say, all there are wrinkles: @@ -2296,8 +2260,9 @@ Needless to say, all there are wrinkles: isTouchableMetaTyVar. * In the constraint solver, we track where Given equalities occur - and use that to guard unification in GHC.Tc.Solver.Canonical.touchabilityTest - More details in Note [Tracking Given equalities] in GHC.Tc.Solver.InertSet + and use that to guard unification in + GHC.Tc.Solver.Canonical.touchabilityAndShapeTest. More details in + Note [Tracking Given equalities] in GHC.Tc.Solver.InertSet Historical note: in the olden days (pre 2021) the constraint solver also used to unify only if l=n. Equalities were "floated" out of the @@ -2312,8 +2277,8 @@ Note [TyVar/TyVar orientation] See also Note [Fundeps with instances, and equality orientation] where the kind equality orientation is important -Given (a ~ b), should we orient the CEqCan as (a~b) or (b~a)? -This is a surprisingly tricky question! This is invariant (TyEq:TV). +Given (a ~ b), should we orient the equality as (a~b) or (b~a)? +This is a surprisingly tricky question! The question is answered by swapOverTyVars, which is used - in the eager unifier, in GHC.Tc.Utils.Unify.uUnfilledVar1 @@ -2330,11 +2295,9 @@ So we look for a positive reason to swap, using a three-step test: * Priority. If the levels are the same, look at what kind of type variable it is, using 'lhsPriority'. - Generally speaking we always try to put a MetaTv on the left - in preference to SkolemTv or RuntimeUnkTv: - a) Because the MetaTv may be touchable and can be unified - b) Even if it's not touchable, GHC.Tc.Solver.floatConstraints - looks for meta tyvars on the left + Generally speaking we always try to put a MetaTv on the left in + preference to SkolemTv or RuntimeUnkTv, because the MetaTv may be + touchable and can be unified. Tie-breaking rules for MetaTvs: - CycleBreakerTv: This is essentially a stand-in for another type; @@ -2555,6 +2518,116 @@ matchExpectedFunKind hs_ty n k = go n k {- ********************************************************************* * * + Checking alpha ~ ty + for the on-the-fly unifier +* * +********************************************************************* -} + +{- Commented out because I think we can just use the simple, + efficient simpleUnifyCheck instead; we can always defer. + +uTypeCheckTouchableTyVarEq :: TcTyVar -> TcType -> TcM (PuResult () TcType) +-- The check may expand type synonyms to avoid an occurs check, +-- so we must use the return type +-- +-- Precondition: rhs is fully zonked +uTypeCheckTouchableTyVarEq lhs_tv rhs + | simpleUnifyCheck False lhs_tv rhs -- Do a fast-path check + -- False <=> See Note [Prevent unification with type families] + = return (pure rhs) + + | otherwise + = do { traceTc "uTypeCheckTouchableTyVarEq {" (pprTyVar lhs_tv $$ ppr rhs) + ; check_result <- checkTyEqRhs flags rhs :: TcM (PuResult () Reduction) + ; traceTc "uTypeCheckTouchableTyVarEq }" (ppr check_result) + ; case check_result of + PuFail reason -> return (PuFail reason) + PuOK redn _ -> assertPpr (isReflCo (reductionCoercion redn)) + (ppr lhs_tv $$ ppr rhs $$ ppr redn) $ + return (pure (reductionReducedType redn)) } + where + flags | MetaTv { mtv_info = tv_info, mtv_tclvl = tv_lvl } <- tcTyVarDetails lhs_tv + = TEF { tef_foralls = isRuntimeUnkSkol lhs_tv + , tef_fam_app = TEFA_Fail + , tef_unifying = Unifying tv_info tv_lvl LC_None + , tef_lhs = TyVarLHS lhs_tv + , tef_occurs = cteInsolubleOccurs } + | otherwise + = pprPanic "uTypeCheckTouchableTyVarEq" (ppr lhs_tv) + -- TEFA_Fail: See Note [Prevent unification with type families] +-} + +simpleUnifyCheck :: Bool -> TcTyVar -> TcType -> Bool +-- A fast check: True <=> unification is OK +-- If it says 'False' then unification might still be OK, but +-- it'll take more work to do -- use the full checkTypeEq +-- +-- * Always rejects foralls unless lhs_tv is RuntimeUnk +-- (used by GHCi debugger) +-- * Rejects a non-concrete type if lhs_tv is concrete +-- * Rejects type families unless fam_ok=True +-- * Does a level-check for type variables +-- +-- This function is pretty heavily used, so it's optimised not to allocate +simpleUnifyCheck fam_ok lhs_tv rhs + = go rhs + where + !(occ_in_ty, occ_in_co) = mkOccFolders lhs_tv + + lhs_tv_lvl = tcTyVarLevel lhs_tv + lhs_tv_is_concrete = isConcreteTyVar lhs_tv + forall_ok = case tcTyVarDetails lhs_tv of + MetaTv { mtv_info = RuntimeUnkTv } -> True + _ -> False + + go (TyVarTy tv) + | lhs_tv == tv = False + | tcTyVarLevel tv > lhs_tv_lvl = False + | lhs_tv_is_concrete, not (isConcreteTyVar tv) = False + | occ_in_ty $! (tyVarKind tv) = False + | otherwise = True + + go (FunTy {ft_af = af, ft_mult = w, ft_arg = a, ft_res = r}) + | isInvisibleFunArg af, not forall_ok = False + | otherwise = go w && go a && go r + + go (TyConApp tc tys) + | lhs_tv_is_concrete, not (isConcreteTyCon tc) = False + | not (isTauTyCon tc) = False + | not fam_ok, not (isFamFreeTyCon tc) = False + | otherwise = all go tys + + go (AppTy t1 t2) = go t1 && go t2 + go (ForAllTy (Bndr tv _) ty) + | forall_ok = go (tyVarKind tv) && (tv == lhs_tv || go ty) + | otherwise = False + + go (CastTy ty co) = not (occ_in_co co) && go ty + go (CoercionTy co) = not (occ_in_co co) + go (LitTy {}) = True + + +mkOccFolders :: TcTyVar -> (TcType -> Bool, TcCoercion -> Bool) +-- These functions return True +-- * if lhs_tv occurs (incl deeply, in the kind of variable) +-- * if there is a coercion hole +-- No expansion of type synonyms +mkOccFolders lhs_tv = (getAny . check_ty, getAny . check_co) + where + !(check_ty, _, check_co, _) = foldTyCo occ_folder emptyVarSet + occ_folder = TyCoFolder { tcf_view = noView -- Don't expand synonyms + , tcf_tyvar = do_tcv, tcf_covar = do_tcv + , tcf_hole = do_hole + , tcf_tycobinder = do_bndr } + + do_tcv is v = Any (not (v `elemVarSet` is) && v == lhs_tv) + `mappend` check_ty (varType v) + + do_bndr is tcv _faf = extendVarSet is tcv + do_hole _is _hole = DM.Any True -- Reject coercion holes + +{- ********************************************************************* +* * Equality invariant checking * * ********************************************************************* -} @@ -2562,8 +2635,7 @@ matchExpectedFunKind hs_ty n k = go n k {- Note [Checking for foralls] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Unless we have -XImpredicativeTypes (which is a totally unsupported -feature), we do not want to unify +We never want to unify alpha ~ (forall a. a->a) -> Int So we look for foralls hidden inside the type, and it's convenient to do that at the same time as the occurs check (which looks for @@ -2590,134 +2662,570 @@ kind had instead been then this kind equality would rightly complain about unifying kappa with (forall k. k->*) +Note [Forgetful synonyms in checkTyConApp] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider + type S a b = b -- Forgets 'a' + + [W] alpha[2] ~ Maybe (S beta[4] gamma[2]) + +We don't want to promote beta to level 2; rather, we should +expand the synonym. (Currently, in checkTypeEqRhs promotion +is irrevocable, by side effect.) + +To avoid this risk we eagerly expand forgetful synonyms. +This also means we won't get an occurs check in + a ~ Maybe (S a b) + +The annoyance is that we might expand the synonym unnecessarily, +something we generally try to avoid. But for now, this seems +simple. + +In a forgetful case like a ~ Maybe (S a b), `checkTyEqRhs` returns +a Reduction that looks + Reduction { reductionCoercion = Refl + , reductionReducedType = Maybe b } +We must jolly well use that reductionReduced type, even though the +reductionCoercion is Refl. See `canEqCanLHSFinish_no_unification`. -} ----------------- -{-# NOINLINE checkTyVarEq #-} -- checkTyVarEq becomes big after the `inline` fires -checkTyVarEq :: TcTyVar -> TcType -> CheckTyEqResult -checkTyVarEq tv ty - = inline checkTypeEq (TyVarLHS tv) ty - -- inline checkTypeEq so that the `case`s over the CanEqLHS get blasted away - -{-# NOINLINE checkTyFamEq #-} -- checkTyFamEq becomes big after the `inline` fires -checkTyFamEq :: TyCon -- type function - -> [TcType] -- args, exactly saturated - -> TcType -- RHS - -> CheckTyEqResult -- always drops cteTypeFamily -checkTyFamEq fun_tc fun_args ty - = inline checkTypeEq (TyFamLHS fun_tc fun_args) ty - `cterRemoveProblem` cteTypeFamily - -- inline checkTypeEq so that the `case`s over the CanEqLHS get blasted away - -checkTypeEq :: CanEqLHS -> TcType -> CheckTyEqResult --- If cteHasNoProblem (checkTypeEq dflags lhs rhs), then lhs ~ rhs --- is a canonical CEqCan. --- --- In particular, this looks for: --- (a) a forall type (forall a. blah) --- (b) a predicate type (c => ty) --- (c) a type family; see Note [Prevent unification with type families] --- (d) an occurrence of the LHS (occurs check) --- --- Note that an occurs-check does not mean "definite error". For example --- type family F a --- type instance F Int = Int --- consider --- b0 ~ F b0 --- This is perfectly reasonable, if we later get b0 ~ Int. But we --- certainly can't unify b0 := F b0 +data PuResult a b = PuFail CheckTyEqResult + | PuOK b (Bag a) + +instance Functor (PuResult a) where + fmap _ (PuFail prob) = PuFail prob + fmap f (PuOK x cts) = PuOK (f x) cts + +instance Applicative (PuResult a) where + pure x = PuOK x emptyBag + PuFail p1 <*> PuFail p2 = PuFail (p1 S.<> p2) + PuFail p1 <*> PuOK {} = PuFail p1 + PuOK {} <*> PuFail p2 = PuFail p2 + PuOK f c1 <*> PuOK x c2 = PuOK (f x) (c1 `unionBags` c2) + +instance (Outputable a, Outputable b) => Outputable (PuResult a b) where + ppr (PuFail prob) = text "PuFail" <+> (ppr prob) + ppr (PuOK x cts) = text "PuOK" <> braces + (vcat [ text "redn:" <+> ppr x + , text "cts:" <+> ppr cts ]) + +pprPur :: PuResult a b -> SDoc +-- For debugging +pprPur (PuFail prob) = text "PuFail:" <> ppr prob +pprPur (PuOK {}) = text "PuOK" + +okCheckRefl :: TcType -> TcM (PuResult a Reduction) +okCheckRefl ty = return (PuOK (mkReflRedn Nominal ty) emptyBag) + +failCheckWith :: CheckTyEqResult -> TcM (PuResult a b) +failCheckWith p = return (PuFail p) + +mapCheck :: (x -> TcM (PuResult a Reduction)) + -> [x] + -> TcM (PuResult a Reductions) +mapCheck f xs + = do { (ress :: [PuResult a Reduction]) <- mapM f xs + ; return (unzipRedns <$> sequenceA ress) } + -- sequenceA :: [PuResult a Reduction] -> PuResult a [Reduction] + -- unzipRedns :: [Reduction] -> Reductions + +----------------------------- +-- | Options describing how to deal with a type equality +-- in the pure unifier. See 'checkTyEqRhs' +data TyEqFlags a + = TEF { tef_foralls :: Bool -- Allow foralls + , tef_lhs :: CanEqLHS -- LHS of the constraint + , tef_unifying :: AreUnifying -- Always NotUnifying if tef_lhs is TyFamLHS + , tef_fam_app :: TyEqFamApp a + , tef_occurs :: CheckTyEqProblem } -- Soluble or insoluble occurs check + +-- | What to do when encountering a type-family application while processing +-- a type equality in the pure unifier. -- --- For (a), (b), and (c) we check only the top level of the type, NOT --- inside the kinds of variables it mentions, and for (d) see --- Note [CEqCan occurs check] in GHC.Tc.Types.Constraint. --- --- checkTypeEq is called from --- * checkTyFamEq, checkTyVarEq (which inline it to specialise away the --- case-analysis on 'lhs') --- * checkEqCanLHSFinish, which does not know the form of 'lhs' -checkTypeEq lhs ty - = go ty +-- See Note [Family applications in canonical constraints] +data TyEqFamApp a + = TEFA_Fail -- Always fail + | TEFA_Recurse -- Just recurse + | TEFA_Break (FamAppBreaker a) -- Recurse, but replace with cycle breaker if fails, + -- using the FamAppBreaker + +data AreUnifying + = Unifying + MetaInfo -- MetaInfo of the LHS tyvar (which is a meta-tyvar) + TcLevel -- Level of the LHS tyvar + LevelCheck + + | NotUnifying -- Not attempting to unify + +data LevelCheck + = LC_None -- Level check not needed: we should never encounter + -- a tyvar at deeper level than the LHS + + | LC_Check -- Do a level check between the LHS tyvar and the occurrence tyvar + -- Fail if the level check fails + + | LC_Promote -- Do a level check between the LHS tyvar and the occurrence tyvar + -- If the level check fails, and the occurrence is a unification + -- variable, promote it + +instance Outputable (TyEqFlags a) where + ppr (TEF { .. }) = text "TEF" <> braces ( + vcat [ text "tef_foralls =" <+> ppr tef_foralls + , text "tef_lhs =" <+> ppr tef_lhs + , text "tef_unifying =" <+> ppr tef_unifying + , text "tef_fam_app =" <+> ppr tef_fam_app + , text "tef_occurs =" <+> ppr tef_occurs ]) + +instance Outputable (TyEqFamApp a) where + ppr TEFA_Fail = text "TEFA_Fail" + ppr TEFA_Recurse = text "TEFA_Fail" + ppr (TEFA_Break {}) = text "TEFA_Break" + +instance Outputable AreUnifying where + ppr NotUnifying = text "NotUnifying" + ppr (Unifying mi lvl lc) = text "Unifying" <+> + braces (ppr mi <> comma <+> ppr lvl <> comma <+> ppr lc) + +instance Outputable LevelCheck where + ppr LC_None = text "LC_None" + ppr LC_Check = text "LC_Check" + ppr LC_Promote = text "LC_Promote" + +famAppArgFlags :: TyEqFlags a -> TyEqFlags a +-- Adjust the flags when going undter a type family +-- Only the outer family application gets the loop-breaker treatment +-- Ditto tyvar promotion. E.g. +-- [W] alpha[2] ~ Maybe (F beta[3]) +-- Do not promote beta[3]; instead promote (F beta[3]) +famAppArgFlags flags@(TEF { tef_unifying = unifying }) + = flags { tef_fam_app = TEFA_Recurse + , tef_unifying = zap_promotion unifying + , tef_occurs = cteSolubleOccurs } + -- tef_occurs: under a type family, an occurs check is not definitely-insoluble where - 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 - -- or a TyCon that would usually be disallowed by bad_tc - -- See Note [RuntimeUnkTv] in GHC.Runtime.Heap.Inspect - ghci_tv - | TyVarLHS tv <- lhs - , MetaTv { mtv_info = RuntimeUnkTv } <- tcTyVarDetails tv - = True + zap_promotion (Unifying info lvl LC_Promote) = Unifying info lvl LC_Check + zap_promotion unifying = unifying + +type FamAppBreaker a = TcType -> TcM (PuResult a Reduction) + -- Given a family-application ty, return a Reduction :: ty ~ cvb + -- where 'cbv' is a fresh loop-breaker tyvar (for Given), or + -- just a fresh TauTv (for Wanted) + +checkTyEqRhs :: forall a. TyEqFlags a -> TcType -> TcM (PuResult a Reduction) +checkTyEqRhs flags ty + = case ty of + LitTy {} -> okCheckRefl ty + TyConApp tc tys -> checkTyConApp flags ty tc tys + TyVarTy tv -> checkTyVar flags tv + -- Don't worry about foralls inside the kind; see Note [Checking for foralls] + -- Nor can we expand synonyms; see Note [Occurrence checking: look inside kinds] + -- in GHC.Core.FVs + + FunTy {ft_af = af, ft_mult = w, ft_arg = a, ft_res = r} + | isInvisibleFunArg af -- e.g. Num a => blah + , not (tef_foralls flags) + -> failCheckWith impredicativeProblem -- Not allowed (TyEq:F) + | otherwise + -> do { w_res <- checkTyEqRhs flags w + ; a_res <- checkTyEqRhs flags a + ; r_res <- checkTyEqRhs flags r + ; return (mkFunRedn Nominal af <$> w_res <*> a_res <*> r_res) } + + AppTy fun arg -> do { fun_res <- checkTyEqRhs flags fun + ; arg_res <- checkTyEqRhs flags arg + ; return (mkAppRedn <$> fun_res <*> arg_res) } + + CastTy ty co -> do { ty_res <- checkTyEqRhs flags ty + ; co_res <- checkCo flags co + ; return (mkCastRedn1 Nominal ty <$> co_res <*> ty_res) } + + CoercionTy co -> do { co_res <- checkCo flags co + ; return (mkReflCoRedn Nominal <$> co_res) } + + ForAllTy {} + | tef_foralls flags -> okCheckRefl ty + | otherwise -> failCheckWith impredicativeProblem -- Not allowed (TyEq:F) + + +------------------- +checkCo :: TyEqFlags a -> Coercion -> TcM (PuResult a Coercion) +-- See Note [checkCo] +checkCo (TEF { tef_lhs = TyFamLHS {} }) co + = return (PuOK co emptyBag) + +checkCo (TEF { tef_lhs = TyVarLHS lhs_tv + , tef_unifying = unifying + , tef_occurs = occ_prob }) co + -- Check for coercion holes, if unifying + -- See (COERCION-HOLE) in Note [Unification preconditions] + | Unifying {} <- unifying + , hasCoercionHoleCo co + = failCheckWith (cteProblem cteCoercionHole) + + -- Occurs check (can promote) + | Unifying _ lhs_tv_lvl LC_Promote <- unifying + = do { reason <- checkPromoteFreeVars occ_prob lhs_tv lhs_tv_lvl (tyCoVarsOfCo co) + ; if cterHasNoProblem reason + then return (pure co) + else failCheckWith reason } + + -- Occurs check (no promotion) + | lhs_tv `elemVarSet` tyCoVarsOfCo co + = failCheckWith (cteProblem occ_prob) + + | otherwise + = return (PuOK co emptyBag) + +{- Note [checkCo] +~~~~~~~~~~~~~~~~~ +We don't often care about the contents of coercions, so checking +coercions before making an equality constraint may be surprising. +But there are several cases we need to be wary of: + +(1) When we're unifying a variable, we must make sure that the variable + appears nowhere on the RHS -- even in a coercion. Otherwise, we'll + create a loop. + +(2) We must still make sure that no variable in a coercion is at too + high a level. But, when unifying, we can promote any variables we encounter. + +(3) We do not unify variables with a type with a free coercion hole. + See (COERCION-HOLE) in Note [Unification preconditions]. + + +Note [Promotion and level-checking] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +"Promotion" happens when we have this: + + [W] w1: alpha[2] ~ Maybe beta[4] + +Here we must NOT unify alpha := Maybe beta, because beta may turn out +to stand for a type involving some inner skolem. Yikes! +Skolem-escape. So instead we /promote/ beta, like this: + + beta[4] := beta'[2] + [W] w1: alpha[2] ~ Maybe beta'[2] + +Now we can unify alpha := Maybe beta', which might unlock other +constraints. But if some other constraint wants to unify beta with a +nested skolem, it'll get stuck with a skolem-escape error. + +Now consider `w2` where a type family is involved (#22194): + + [W] w2: alpha[2] ~ Maybe (F gamma beta[4]) + +In `w2`, it may or may not be the case that `beta` is level 2; suppose +we later discover gamma := Int, and type instance F Int _ = Int. +So, instead, we promote the entire funcion call: + + [W] w2': alpha[2] ~ Maybe gamma[2] + [W] w3: gamma[2] ~ F gamma beta[4] + +Now we can unify alpha := Maybe gamma, which is a Good Thng. + +Wrinkle (W1) + +There is an important wrinkle: /all this only applies when unifying/. +For example, suppose we have + [G] a[2] ~ Maybe b[4] +where 'a' is a skolem. This Given might arise from a GADT match, and +we can absolutely use it to rewrite locally. In fact we must do so: +that is how we exploit local knowledge about the outer skolem a[2]. +This applies equally for a Wanted [W] a[2] ~ Maybe b[4]. Using it for +local rewriting is fine. (It's not clear to me that it is /useful/, +but it's fine anyway.) + +So we only do the level-check in checkTyVar when /unifying/ not for +skolems (or untouchable unification variables). + +Note [Family applications in canonical constraints] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +A constraint with a type family application in the RHS needs special care. + +* First, occurs checks. If we have + [G] a ~ Maybe (F (Maybe a)) + [W] alpha ~ Maybe (F (Maybe alpha)) + it looks as if we have an occurs check. But go read + Note [Type equality cycles] in GHC.Tc.Solver.Equality + + The same considerations apply when the LHS is a type family: + [G] G a ~ Maybe (F (Maybe (G a))) + [W] G alpha ~ Maybe (F (Maybe (G alpha))) + +* Second, promotion. If we have (#22194) + [W] alpha[2] ~ Maybe (F beta[4]) + it is wrong to promote beta. Instead we want to split to + [W] alpha[2] ~ Maybe gamma[2] + [W] gamma[2] ~ F beta[4] + See Note [Promotion and level-checking] above. + +* Third, concrete type variables. If we have + [W] alpha[conc] ~ Maybe (F tys) + we want to add an extra variable thus: + [W] alpha[conc] ~ Maybe gamma[conc] + [W] gamma[conc] ~ F tys + Now we can unify alpha, and that might unlock something else. + +In all these cases we want to create a fresh type variable, and +emit a new equality connecting it to the type family application. + +The `tef_fam_app` field of `TypeEqFlags` says what to do at a type +family application in the RHS of the constraint. `TEFA_Fail` and +`TEFA_Recurse` are straightforward. `TEFA_Break` is the clever +one. As you can see in `checkFamApp`, it + * Checks the arguments, but using `famAppArgFlags` to record that + we are now "under" a type-family application. It `tef_fam_app` to + `TEFA_Recurse`. + * If any of the arguments fail (level-check error, occurs check) + use the `FamAppBreaker` to create the extra binding. + +Note that this always cycle-breaks the /outermost/ family application. +If we have [W] alpha ~ Maybe (F (G alpha)) +* We'll use checkFamApp on `(F (G alpha))` +* It will recurse into `(G alpha)` with TEFA_Recurse, but not cycle-break it +* The occurs check will fire when we hit `alpha` +* `checkFamApp` on `(F (G alpha))` will see the failure and invoke + the `FamAppBreaker`. +-} + +------------------- +checkTyConApp :: TyEqFlags a + -> TcType -> TyCon -> [TcType] + -> TcM (PuResult a Reduction) +checkTyConApp flags@(TEF { tef_unifying = unifying, tef_foralls = foralls_ok }) + tc_app tc tys + | isTypeFamilyTyCon tc + , let arity = tyConArity tc + = if tys `lengthIs` arity + then checkFamApp flags tc_app tc tys -- Common case + else do { let (fun_args, extra_args) = splitAt (tyConArity tc) tys + fun_app = mkTyConApp tc fun_args + ; fun_res <- checkFamApp flags fun_app tc fun_args + ; extra_res <- mapCheck (checkTyEqRhs flags) extra_args + ; traceTc "Over-sat" (ppr tc <+> ppr tys $$ ppr arity $$ pprPur fun_res $$ pprPur extra_res) + ; return (mkAppRedns <$> fun_res <*> extra_res) } + + | Just ty' <- rewriterView tc_app + -- e.g. S a where type S a = F [a] + -- or type S a = Int + -- See Note [Forgetful synonyms in checkTyConApp] + = checkTyEqRhs flags ty' + + | not (isTauTyCon tc || foralls_ok) + = failCheckWith impredicativeProblem + + | Unifying info _ _ <- unifying + , isConcreteInfo info + , not (isConcreteTyCon tc) + = failCheckWith (cteProblem cteConcrete) + + | otherwise -- Recurse on arguments + = recurseIntoTyConApp flags tc tys + +recurseIntoTyConApp :: TyEqFlags a -> TyCon -> [TcType] -> TcM (PuResult a Reduction) +recurseIntoTyConApp flags tc tys + = do { tys_res <- mapCheck (checkTyEqRhs flags) tys + ; return (mkTyConAppRedn Nominal tc <$> tys_res) } + +------------------- +checkFamApp :: TyEqFlags a + -> TcType -> TyCon -> [TcType] -- Saturated family application + -> TcM (PuResult a Reduction) +-- See Note [Family applications in canonical constraints] +checkFamApp flags@(TEF { tef_unifying = unifying, tef_occurs = occ_prob + , tef_fam_app = fam_app_flag, tef_lhs = lhs }) + fam_app tc tys + = case fam_app_flag of + TEFA_Fail -> failCheckWith (cteProblem cteTypeFamily) + + _ | TyFamLHS lhs_tc lhs_tys <- lhs + , tcEqTyConApps lhs_tc lhs_tys tc tys -- F ty ~ ...(F ty)... + -> case fam_app_flag of + TEFA_Recurse -> failCheckWith (cteProblem occ_prob) + TEFA_Break breaker -> breaker fam_app + + _ | Unifying lhs_info _ _ <- unifying + , isConcreteInfo lhs_info + -> case fam_app_flag of + TEFA_Recurse -> failCheckWith (cteProblem cteConcrete) + TEFA_Break breaker -> breaker fam_app + + TEFA_Recurse + -> do { tys_res <- mapCheck (checkTyEqRhs arg_flags) tys + ; traceTc "under" (ppr tc $$ pprPur tys_res $$ ppr flags) + ; return (mkTyConAppRedn Nominal tc <$> tys_res) } + + TEFA_Break breaker -- Recurse; and break if there is a problem + -> do { tys_res <- mapCheck (checkTyEqRhs arg_flags) tys + ; case tys_res of + PuOK redns cts -> return (PuOK (mkTyConAppRedn Nominal tc redns) cts) + PuFail {} -> breaker fam_app } + where + arg_flags = famAppArgFlags flags + +------------------- +checkTyVar :: forall a. TyEqFlags a -> TcTyVar -> TcM (PuResult a Reduction) +checkTyVar (TEF { tef_lhs = lhs, tef_unifying = unifying, tef_occurs = occ_prob }) occ_tv + = case lhs of + TyFamLHS {} -> success -- Nothing to do if the LHS is a type-family + TyVarLHS lhs_tv -> check_tv unifying lhs_tv + where + lvl_occ = tcTyVarLevel occ_tv + success = okCheckRefl (mkTyVarTy occ_tv) + + --------------------- + check_tv NotUnifying lhs_tv + = simple_occurs_check lhs_tv + -- We need an occurs-check here, but no level check + -- See Note [Promotion and level-checking] wrinkle (W1) + + check_tv (Unifying info lvl prom) lhs_tv + = do { mb_done <- isFilledMetaTyVar_maybe occ_tv + ; case mb_done of + Just {} -> success + -- Already promoted; job done + -- Example alpha[2] ~ Maybe (beta[4], beta[4]) + -- We promote the first occurrence, and then encounter it + -- a second time; we don't want to re-promote it! + -- Remember, the entire process started with a fully zonked type + + Nothing -> check_unif info lvl prom lhs_tv } + + --------------------- + -- We are in the Unifying branch of AreUnifing + check_unif :: MetaInfo -> TcLevel -> LevelCheck + -> TcTyVar -> TcM (PuResult a Reduction) + check_unif lhs_tv_info lhs_tv_lvl prom lhs_tv + | isConcreteInfo lhs_tv_info + , not (isConcreteTyVar occ_tv) + = if can_make_concrete occ_tv + then promote lhs_tv lhs_tv_info lhs_tv_lvl + else failCheckWith (cteProblem cteConcrete) + + | lvl_occ `strictlyDeeperThan` lhs_tv_lvl + = case prom of + LC_None -> pprPanic "check_unif" (ppr lhs_tv $$ ppr occ_tv) + LC_Check -> failCheckWith (cteProblem cteSkolemEscape) + LC_Promote + | isSkolemTyVar occ_tv -> failCheckWith (cteProblem cteSkolemEscape) + | otherwise -> promote lhs_tv lhs_tv_info lhs_tv_lvl | otherwise - = False + = simple_occurs_check lhs_tv + + --------------------- + simple_occurs_check lhs_tv + | lhs_tv == occ_tv || check_kind (tyVarKind occ_tv) + = failCheckWith (cteProblem occ_prob) + | otherwise + = success + where + (check_kind, _) = mkOccFolders lhs_tv + + --------------------- + can_make_concrete occ_tv = case tcTyVarDetails occ_tv of + MetaTv { mtv_info = info } -> case info of + ConcreteTv {} -> True + TauTv {} -> True + _ -> False + _ -> False -- Don't attempt to make other type variables concrete + -- (e.g. SkolemTv, TyVarTv, CycleBreakerTv, RuntimeUnkTv). + + --------------------- + -- occ_tv is definitely a MetaTyVar + promote lhs_tv lhs_tv_info lhs_tv_lvl + | MetaTv { mtv_info = info_occ, mtv_tclvl = lvl_occ } <- tcTyVarDetails occ_tv + = do { let new_info | isConcreteInfo lhs_tv_info = lhs_tv_info + | otherwise = info_occ + new_lvl = lhs_tv_lvl `minTcLevel` lvl_occ + -- c[conc,3] ~ p[tau,2]: want to clone p:=p'[conc,2] + -- c[tau,2] ~ p[tau,3]: want to clone p:=p'[tau,2] + + -- Check the kind of occ_tv + ; reason <- checkPromoteFreeVars occ_prob lhs_tv lhs_tv_lvl (tyCoVarsOfType (tyVarKind occ_tv)) + + ; if cterHasNoProblem reason -- Successfully promoted + then do { new_tv_ty <- promote_meta_tyvar new_info new_lvl occ_tv + ; okCheckRefl new_tv_ty } + else failCheckWith reason } + + | otherwise = pprPanic "promote" (ppr occ_tv) + +------------------------- +checkPromoteFreeVars :: CheckTyEqProblem -- What occurs check problem to report + -> TcTyVar -> TcLevel + -> TyCoVarSet -> TcM CheckTyEqResult +-- Check this set of TyCoVars for +-- (a) occurs check +-- (b) promote if necessary, or report skolem escape +checkPromoteFreeVars occ_prob lhs_tv lhs_tv_lvl vs + = do { oks <- mapM do_one (nonDetEltsUniqSet vs) + ; return (mconcat oks) } + where + do_one :: TyCoVar -> TcM CheckTyEqResult + do_one v | isCoVar v = return cteOK + | lhs_tv == v = return (cteProblem occ_prob) + | no_promotion = return cteOK + | not (isMetaTyVar v) = return (cteProblem cteSkolemEscape) + | otherwise = promote_one v + where + no_promotion = not (tcTyVarLevel v `strictlyDeeperThan` lhs_tv_lvl) + + -- isCoVar case: coercion variables are not an escape risk + -- If an implication binds a coercion variable, it'll have equalities, + -- so the "intervening given equalities" test above will catch it + -- Coercion holes get filled with coercions, so again no problem. + + promote_one tv = do { _ <- promote_meta_tyvar TauTv lhs_tv_lvl tv + ; return cteOK } + +promote_meta_tyvar :: MetaInfo -> TcLevel -> TcTyVar -> TcM TcType +promote_meta_tyvar info dest_lvl occ_tv + = do { -- Check whether occ_tv is already unified. The rhs-type + -- started zonked, but we may have promoted one of its type + -- variables, and we then encounter it for the second time. + -- But if so, it'll definitely be another already-checked TyVar + mb_filled <- isFilledMetaTyVar_maybe occ_tv + ; case mb_filled of { + Just ty -> return ty ; + Nothing -> + + -- OK, not done already, so clone/promote it + do { new_tv <- cloneMetaTyVarWithInfo info dest_lvl occ_tv + ; writeMetaTyVar occ_tv (mkTyVarTy new_tv) + ; traceTc "promoteTyVar" (ppr occ_tv <+> text "-->" <+> ppr new_tv) + ; return (mkTyVarTy new_tv) } } } + + + +------------------------- +touchabilityAndShapeTest :: TcLevel -> TcTyVar -> TcType -> Bool +-- This is the key test for untouchability: +-- See Note [Unification preconditions] in GHC.Tc.Utils.Unify +-- and Note [Solve by unification] in GHC.Tc.Solver.Interact +-- True <=> touchability and shape are OK +touchabilityAndShapeTest given_eq_lvl tv rhs + | MetaTv { mtv_info = info, mtv_tclvl = tv_lvl } <- tcTyVarDetails tv + , checkTopShape info rhs + = tv_lvl `deeperThanOrSame` given_eq_lvl + | otherwise + = False + +------------------------- +-- | checkTopShape checks (TYVAR-TV) +-- Note [Unification preconditions]; returns True if these conditions +-- are satisfied. But see the Note for other preconditions, too. +checkTopShape :: MetaInfo -> TcType -> Bool +checkTopShape info xi + = case info of + TyVarTv -> + case getTyVar_maybe xi of -- Looks through type synonyms + Nothing -> False + Just tv -> case tcTyVarDetails tv of -- (TYVAR-TV) wrinkle + SkolemTv {} -> True + RuntimeUnk -> True + MetaTv { mtv_info = TyVarTv } -> True + _ -> False + CycleBreakerTv -> False -- We never unify these + _ -> True - go :: TcType -> CheckTyEqResult - go (TyVarTy tv') = go_tv tv' - go (TyConApp tc tys) = go_tc tc tys - go (LitTy {}) = cteOK - go (FunTy {ft_af = af, ft_mult = w, ft_arg = a, ft_res = r}) - = go w S.<> go a S.<> go r S.<> - if not ghci_tv && isInvisibleFunArg af - then impredicative - else cteOK - go (AppTy fun arg) = go fun S.<> go arg - go (CastTy ty co) = go ty S.<> go_co co - go (CoercionTy co) = go_co co - go (ForAllTy (Bndr tv' _) ty) = (case lhs of - TyVarLHS tv | tv == tv' -> go_occ (tyVarKind tv') S.<> cterClearOccursCheck (go ty) - | otherwise -> go_occ (tyVarKind tv') S.<> go ty - _ -> go ty) - S.<> - if ghci_tv then cteOK else impredicative - - go_tv :: TcTyVar -> CheckTyEqResult - -- this slightly peculiar way of defining this means - -- we don't have to evaluate this `case` at every variable - -- occurrence - go_tv = case lhs of - TyVarLHS tv -> \ tv' -> go_occ (tyVarKind tv') S.<> - if tv == tv' then insoluble_occurs else cteOK - TyFamLHS {} -> \ _tv' -> cteOK - -- See Note [Occurrence checking: look inside kinds] in GHC.Core.Type - - -- For kinds, we only do an occurs check; we do not worry - -- about type families or foralls - -- See Note [Checking for foralls] - go_occ k = cterFromKind $ go k - - go_tc :: TyCon -> [TcType] -> CheckTyEqResult - -- this slightly peculiar way of defining this means - -- we don't have to evaluate this `case` at every tyconapp - go_tc = case lhs of - TyVarLHS {} -> \ tc tys -> check_tc tc S.<> go_tc_args tc tys - TyFamLHS fam_tc fam_args -> \ tc tys -> - if tcEqTyConApps fam_tc fam_args tc tys - then insoluble_occurs - else check_tc tc S.<> go_tc_args tc tys - - -- just look at arguments, not the tycon itself - go_tc_args :: TyCon -> [TcType] -> CheckTyEqResult - go_tc_args tc tys | isGenerativeTyCon tc Nominal = foldMap go tys - | otherwise - = let (tf_args, non_tf_args) = splitAt (tyConArity tc) tys in - cterSetOccursCheckSoluble (foldMap go tf_args) S.<> foldMap go non_tf_args - - -- no bother about impredicativity in coercions, as they're - -- inferred - go_co co | TyVarLHS tv <- lhs - , tv `elemVarSet` tyCoVarsOfCo co - = soluble_occurs - - -- Don't check coercions for type families; see commentary at top of function - | otherwise - = cteOK - - check_tc :: TyCon -> CheckTyEqResult - check_tc - | ghci_tv = \ _tc -> cteOK - | otherwise = \ tc -> (if isTauTyCon tc then cteOK else impredicative) S.<> - (if isFamFreeTyCon tc then cteOK else type_family) |