diff options
| author | Simon Peyton Jones <simon.peytonjones@gmail.com> | 2023-03-10 09:55:00 +0000 |
|---|---|---|
| committer | Krzysztof Gogolewski <krzysztof.gogolewski@tweag.io> | 2023-04-14 20:01:02 +0200 |
| commit | 2371d6b2d178895cc97f7bfebf489af4a095241b (patch) | |
| tree | 877f7d8f6f4e6b0c788f4084533d331692db25ca | |
| parent | d48fbfea5f7b760ec3d13dd2947257986c095b75 (diff) | |
| download | haskell-2371d6b2d178895cc97f7bfebf489af4a095241b.tar.gz | |
Major refactor in the handling of equality constraints
This MR substantially refactors the way in which the constraint
solver deals with equality constraints. The big thing is:
* Intead of a pipeline in which we /first/ canonicalise and /then/
interact (the latter including performing unification) the two steps
are more closely integreated into one. That avoids the current
rather indirect communication between the two steps.
The proximate cause for this refactoring is fixing #22194, which involve
solving [W] alpha[2] ~ Maybe (F beta[4])
by doing this:
alpha[2] := Maybe delta[2]
[W] delta[2] ~ F beta[4]
That is, we don't promote beta[4]! This is very like introducing a cycle
breaker, and was very awkward to do before, but now it is all nice.
See GHC.Tc.Utils.Unify Note [Promotion and level-checking] and
Note [Family applications in canonical constraints].
The big change is this:
* Several canonicalisation checks (occurs-check, cycle-breaking,
checking for concreteness) are combined into one new function:
GHC.Tc.Utils.Unify.checkTyEqRhs
This function is controlled by `TyEqFlags`, which says what to do
for foralls, type families etc.
* `canEqCanLHSFinish` now sees if unification is possible, and if so,
actually does it: see `canEqCanLHSFinish_try_unification`.
There are loads of smaller changes:
* The on-the-fly unifier `GHC.Tc.Utils.Unify.unifyType` has a
cheap-and-cheerful version of `checkTyEqRhs`, called
`simpleUnifyCheck`. If `simpleUnifyCheck` succeeds, it can unify,
otherwise it defers by emitting a constraint. This is simpler than
before.
* I simplified the swapping code in `GHC.Tc.Solver.Equality.canEqCanLHS`.
Especially the nasty stuff involving `swap_for_occurs` and
`canEqTyVarFunEq`. Much nicer now. See
Note [Orienting TyVarLHS/TyFamLHS]
Note [Orienting TyFamLHS/TyFamLHS]
* Added `cteSkolemOccurs`, `cteConcrete`, and `cteCoercionHole` to the
problems that can be discovered by `checkTyEqRhs`.
* I fixed #23199 `pickQuantifiablePreds`, which actually allows GHC to
to accept both cases in #22194 rather than rejecting both.
Yet smaller:
* Added a `synIsConcrete` flag to `SynonymTyCon` (alongside `synIsFamFree`)
to reduce the need for synonym expansion when checking concreteness.
Use it in `isConcreteType`.
* Renamed `isConcrete` to `isConcreteType`
* Defined `GHC.Core.TyCo.FVs.isInjectiveInType` as a more efficient
way to find if a particular type variable is used injectively than
finding all the injective variables. It is called in
`GHC.Tc.Utils.Unify.definitely_poly`, which in turn is used quite a
lot.
* Moved `rewriterView` to `GHC.Core.Type`, so we can use it from the
constraint solver.
Fixes #22194, #23199
Compile times decrease by an average of 0.1%; but there is a 7.4%
drop in compiler allocation on T15703.
Metric Decrease:
T15703
40 files changed, 2181 insertions, 1240 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) diff --git a/testsuite/tests/ado/T16135.stderr b/testsuite/tests/ado/T16135.stderr new file mode 100644 index 0000000000..e6a77cdfe6 --- /dev/null +++ b/testsuite/tests/ado/T16135.stderr @@ -0,0 +1,14 @@ +T16135.hs:11:18: error: [GHC-83865] + • Couldn't match type ‘a0’ with ‘a’ + Expected: f a0 + Actual: f a + ‘a’ is a rigid type variable bound by + a pattern with constructor: + MkT :: forall {k} (f :: k -> *) (a :: k). f a -> T f, + in a pattern binding in + a 'do' block + at T16135.hs:10:5-10 + • In the first argument of ‘MkT’, namely ‘fa’ + In the second argument of ‘($)’, namely ‘MkT fa’ + In a stmt of a 'do' block: return $ MkT fa + • Relevant bindings include fa :: f a (bound at T16135.hs:10:9) diff --git a/testsuite/tests/ado/all.T b/testsuite/tests/ado/all.T index c46ea88404..0568cd00e9 100644 --- a/testsuite/tests/ado/all.T +++ b/testsuite/tests/ado/all.T @@ -20,5 +20,5 @@ test('T15344', normal, compile_and_run, ['']) test('T16628', normal, compile_fail, ['']) test('T17835', normal, compile, ['']) test('T20540', normal, compile, ['']) -test('T16135', [when(compiler_debugged(),expect_broken(16135)), js_broken(22576)], compile, ['']) +test('T16135', [when(compiler_debugged(),expect_broken(16135)), js_broken(22576)], compile_fail, ['']) test('T22483', normal, compile, ['-Wall']) diff --git a/testsuite/tests/indexed-types/should_compile/T3208b.stderr b/testsuite/tests/indexed-types/should_compile/T3208b.stderr index 45a3b9b74c..9cb2670505 100644 --- a/testsuite/tests/indexed-types/should_compile/T3208b.stderr +++ b/testsuite/tests/indexed-types/should_compile/T3208b.stderr @@ -1,6 +1,6 @@ T3208b.hs:15:10: error: [GHC-05617] - • Could not deduce ‘OTerm o0 ~ STerm a’ arising from a use of ‘fce’ + • Could not deduce ‘STerm o0 ~ OTerm a’ arising from a use of ‘fce’ from the context: (OTerm a ~ STerm a, OBJECT a, SUBST a) bound by the type signature for: fce' :: forall a c. @@ -15,7 +15,7 @@ T3208b.hs:15:10: error: [GHC-05617] fce' :: a -> c (bound at T3208b.hs:15:1) T3208b.hs:15:15: error: [GHC-05617] - • Could not deduce ‘STerm o0 ~ STerm a’ + • Could not deduce ‘OTerm o0 ~ OTerm a’ arising from a use of ‘apply’ from the context: (OTerm a ~ STerm a, OBJECT a, SUBST a) bound by the type signature for: @@ -23,7 +23,7 @@ T3208b.hs:15:15: error: [GHC-05617] (OTerm a ~ STerm a, OBJECT a, SUBST a) => a -> c at T3208b.hs:14:1-56 - NB: ‘STerm’ is a non-injective type family + NB: ‘OTerm’ is a non-injective type family The type variable ‘o0’ is ambiguous • In the first argument of ‘fce’, namely ‘(apply f)’ In the expression: fce (apply f) diff --git a/testsuite/tests/indexed-types/should_fail/T8227.stderr b/testsuite/tests/indexed-types/should_fail/T8227.stderr index 64792ae0e9..3d20ee24ca 100644 --- a/testsuite/tests/indexed-types/should_fail/T8227.stderr +++ b/testsuite/tests/indexed-types/should_fail/T8227.stderr @@ -1,9 +1,10 @@ T8227.hs:24:27: error: [GHC-83865] • Couldn't match type: Scalar (V a) - with: t0 -> t0 + with: p0 -> p0 Expected: Scalar (V a) - Actual: Scalar (V (t0 -> t0)) -> Scalar (V (t0 -> t0)) + Actual: Scalar (V (Scalar (V p0) -> p0)) + -> Scalar (V (Scalar (V p0) -> p0)) • In the expression: arcLengthToParam eps eps In an equation for ‘absoluteToParam’: absoluteToParam eps seg = arcLengthToParam eps eps @@ -14,9 +15,9 @@ T8227.hs:24:27: error: [GHC-83865] (bound at T8227.hs:24:1) T8227.hs:24:48: error: [GHC-27958] - • Couldn't match type ‘t0’ with ‘Scalar (V t0)’ - arising from a type equality Scalar (V a) ~ t0 -> t0 - The type variable ‘t0’ is ambiguous + • Couldn't match type ‘p0’ with ‘Scalar (V p0)’ + arising from a type equality Scalar (V a) ~ Scalar (V p0) -> p0 + The type variable ‘p0’ is ambiguous • In the second argument of ‘arcLengthToParam’, namely ‘eps’ In the expression: arcLengthToParam eps eps In an equation for ‘absoluteToParam’: diff --git a/testsuite/tests/partial-sigs/should_fail/T14040a.stderr b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr index 5614422045..fc3c1e0c8b 100644 --- a/testsuite/tests/partial-sigs/should_fail/T14040a.stderr +++ b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr @@ -1,7 +1,7 @@ T14040a.hs:26:46: error: [GHC-46956] - • Couldn't match kind ‘k1’ with ‘WeirdList z’ - Expected kind ‘WeirdList k1’, + • Couldn't match kind ‘k0’ with ‘WeirdList z’ + Expected kind ‘WeirdList k0’, but ‘xs’ has kind ‘WeirdList (WeirdList z)’ because kind variable ‘z’ would escape its scope This (rigid, skolem) kind variable is bound by @@ -25,8 +25,8 @@ T14040a.hs:26:46: error: [GHC-46956] -> p _ wl T14040a.hs:27:27: error: [GHC-46956] - • Couldn't match kind ‘k0’ with ‘z’ - Expected kind ‘WeirdList k0’, + • Couldn't match kind ‘k1’ with ‘z’ + Expected kind ‘WeirdList k1’, but ‘WeirdCons x xs’ has kind ‘WeirdList z’ because kind variable ‘z’ would escape its scope This (rigid, skolem) kind variable is bound by diff --git a/testsuite/tests/polykinds/T14939.hs b/testsuite/tests/polykinds/T14939.hs index f1387a00ab..39b9784d1f 100644 --- a/testsuite/tests/polykinds/T14939.hs +++ b/testsuite/tests/polykinds/T14939.hs @@ -16,4 +16,4 @@ data AlgCat (cls::Type -> Constraint) :: Cat (Alg cls Type) where AlgCat :: (cls a, cls b) => (a -> b) -> AlgCat cls a b leftAdj :: AlgCat cls (Frí cls a) b -> (a -> b) -leftAdj (AlgCat f) a = undefined
\ No newline at end of file +leftAdj (AlgCat f) a = undefined diff --git a/testsuite/tests/polykinds/T18451a.hs b/testsuite/tests/polykinds/T18451a.hs index 5611a7afcb..b7c5f983ea 100644 --- a/testsuite/tests/polykinds/T18451a.hs +++ b/testsuite/tests/polykinds/T18451a.hs @@ -10,3 +10,9 @@ type Const a b = a foo :: forall a b (c :: Const Type b). Proxy '[a, c] foo = error "ruk" + +-- We infer a :: k0, k0 ~ Const Type b +-- We unify k0 := Const Type b (in the eager unifier) +-- And that leaves us with +-- forall (a :: Const Type b) (b :: Type) (c :: Const Type b). ...a +-- Bad! But delicate because we could expand the synonym diff --git a/testsuite/tests/polykinds/T18451b.hs b/testsuite/tests/polykinds/T18451b.hs deleted file mode 100644 index 5611a7afcb..0000000000 --- a/testsuite/tests/polykinds/T18451b.hs +++ /dev/null @@ -1,12 +0,0 @@ -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE DataKinds #-} -module Bug where - -import Data.Kind -import Data.Proxy - -type Const a b = a - -foo :: forall a b (c :: Const Type b). Proxy '[a, c] -foo = error "ruk" diff --git a/testsuite/tests/polykinds/T18451b.stderr b/testsuite/tests/polykinds/T18451b.stderr deleted file mode 100644 index 9389400d6d..0000000000 --- a/testsuite/tests/polykinds/T18451b.stderr +++ /dev/null @@ -1,7 +0,0 @@ - -T18451b.hs:11:15: error: [GHC-97739] - • These kind and type variables: a b (c :: Const Type b) - are out of dependency order. Perhaps try this ordering: - (b :: k) (a :: Const (*) b) (c :: Const (*) b) - • In the type signature: - foo :: forall a b (c :: Const Type b). Proxy '[a, c] diff --git a/testsuite/tests/polykinds/T22793.stderr b/testsuite/tests/polykinds/T22793.stderr index 8082fa5be0..fc91382642 100644 --- a/testsuite/tests/polykinds/T22793.stderr +++ b/testsuite/tests/polykinds/T22793.stderr @@ -1,36 +1,13 @@ T22793.hs:15:42: error: [GHC-25897] - • Couldn't match kind ‘ka’ with ‘k1’ - Expected kind ‘ks’, but ‘a’ has kind ‘ka’ + • Expected kind ‘ks’, but ‘a’ has kind ‘ka’ ‘ka’ is a rigid type variable bound by the type signature for ‘bob’ at T22793.hs:13:26-27 - ‘k1’ is a rigid type variable bound by - the type signature for ‘bob’ - at T22793.hs:13:16-17 - • In the second argument of ‘Foo’, namely ‘a’ - In the type signature: - bob :: forall {k1} - {ks} - {ka} - q - (p :: k1 -> q -> Type) - (f :: ka -> q) - (s :: ks) - (t :: ks) - (a :: ka) - (b :: ka). Foo s a => p a (f b) -> p s (f t) - -T22793.hs:16:11: error: [GHC-25897] - • Couldn't match kind ‘ks’ with ‘k1’ - Expected kind ‘k1’, but ‘a’ has kind ‘ka’ ‘ks’ is a rigid type variable bound by the type signature for ‘bob’ at T22793.hs:13:21-22 - ‘k1’ is a rigid type variable bound by - the type signature for ‘bob’ - at T22793.hs:13:16-17 - • In the first argument of ‘p’, namely ‘a’ + • In the second argument of ‘Foo’, namely ‘a’ In the type signature: bob :: forall {k1} {ks} diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T index e16789136f..7a8d5aa7b4 100644 --- a/testsuite/tests/polykinds/all.T +++ b/testsuite/tests/polykinds/all.T @@ -226,7 +226,6 @@ test('T17963', normal, compile_fail, ['']) test('T18300', normal, compile_fail, ['']) test('T18451', normal, compile_fail, ['']) test('T18451a', normal, compile_fail, ['']) -test('T18451b', normal, compile_fail, ['']) test('NestedProxies', normal, compile, ['']) test('T18522-ppr', normal, ghci_script, ['T18522-ppr.script']) test('T18855', normal, compile, ['']) diff --git a/testsuite/tests/rep-poly/RepPolyBackpack1.stderr b/testsuite/tests/rep-poly/RepPolyBackpack1.stderr index cfdf4cf2bd..320ba6a6e1 100644 --- a/testsuite/tests/rep-poly/RepPolyBackpack1.stderr +++ b/testsuite/tests/rep-poly/RepPolyBackpack1.stderr @@ -1,6 +1,6 @@ [1 of 1] Processing number-unknown - [1 of 2] Compiling NumberUnknown[sig] ( number-unknown\NumberUnknown.hsig, nothing ) - [2 of 2] Compiling NumberStuff ( number-unknown\NumberStuff.hs, nothing ) + [1 of 2] Compiling NumberUnknown[sig] ( number-unknown/NumberUnknown.hsig, nothing ) + [2 of 2] Compiling NumberStuff ( number-unknown/NumberStuff.hs, nothing ) RepPolyBackpack1.bkp:17:5: error: [GHC-55287] The second pattern in the equation for ‘funcA’ diff --git a/testsuite/tests/rep-poly/RepPolyInferPatBind.stderr b/testsuite/tests/rep-poly/RepPolyInferPatBind.stderr index 486de932bd..a9643f4b73 100644 --- a/testsuite/tests/rep-poly/RepPolyInferPatBind.stderr +++ b/testsuite/tests/rep-poly/RepPolyInferPatBind.stderr @@ -8,6 +8,8 @@ RepPolyInferPatBind.hs:21:2: error: [GHC-55287] • The pattern binding does not have a fixed runtime representation. Its type is: T :: TYPE R + Cannot unify ‘R’ with the type variable ‘p0’ + because it is not a concrete ‘RuntimeRep’. • When checking that the pattern signature: T fits the type of its context: T In the pattern: x :: T diff --git a/testsuite/tests/rep-poly/RepPolyInferPatSyn.stderr b/testsuite/tests/rep-poly/RepPolyInferPatSyn.stderr index 7f5c4f1ca7..4515832b21 100644 --- a/testsuite/tests/rep-poly/RepPolyInferPatSyn.stderr +++ b/testsuite/tests/rep-poly/RepPolyInferPatSyn.stderr @@ -4,6 +4,8 @@ RepPolyInferPatSyn.hs:22:16: error: [GHC-55287] does not have a fixed runtime representation. Its type is: T :: TYPE R + Cannot unify ‘R’ with the type variable ‘p0’ + because it is not a concrete ‘RuntimeRep’. • When checking that the pattern signature: T fits the type of its context: T In the pattern: a :: T diff --git a/testsuite/tests/typecheck/no_skolem_info/T14040.stderr b/testsuite/tests/typecheck/no_skolem_info/T14040.stderr index c5e44796e1..966e19bec7 100644 --- a/testsuite/tests/typecheck/no_skolem_info/T14040.stderr +++ b/testsuite/tests/typecheck/no_skolem_info/T14040.stderr @@ -1,7 +1,7 @@ T14040.hs:27:46: error: [GHC-46956] - • Couldn't match kind ‘k1’ with ‘WeirdList z’ - Expected kind ‘WeirdList k1’, + • Couldn't match kind ‘k0’ with ‘WeirdList z’ + Expected kind ‘WeirdList k0’, but ‘xs’ has kind ‘WeirdList (WeirdList z)’ because kind variable ‘z’ would escape its scope This (rigid, skolem) kind variable is bound by @@ -25,8 +25,8 @@ T14040.hs:27:46: error: [GHC-46956] -> p _ wl T14040.hs:28:27: error: [GHC-46956] - • Couldn't match kind ‘k0’ with ‘z’ - Expected kind ‘WeirdList k0’, + • Couldn't match kind ‘k1’ with ‘z’ + Expected kind ‘WeirdList k1’, but ‘WeirdCons x xs’ has kind ‘WeirdList z’ because kind variable ‘z’ would escape its scope This (rigid, skolem) kind variable is bound by diff --git a/testsuite/tests/typecheck/should_compile/T22194.hs b/testsuite/tests/typecheck/should_compile/T22194.hs new file mode 100644 index 0000000000..70a3988b7c --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T22194.hs @@ -0,0 +1,64 @@ +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PartialTypeSignatures #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE MagicHash, UnboxedTuples #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE NoMonoLocalBinds #-} + +module Test where + +import Data.Kind +import GHC.Exts + +--import Control.Monad.Primitive -- primitive-0.7.4.0 +--import Data.Primitive.MutVar -- primitive-0.7.4.0 + +class Monad m => PrimMonad m where + type PrimState m + primitive :: (State# (PrimState m) -> (# State# (PrimState m), a #)) -> m a + +data MutVar s a = MutVar (MutVar# s a) + +newMutVar :: PrimMonad m => a -> m (MutVar (PrimState m) a) +newMutVar = error "urk" + +writeMutVar :: PrimMonad m => MutVar (PrimState m) a -> a -> m () +writeMutVar = error "Urk" + +----------- + +class Monad m => New a m where + new :: m a + +class Monad m => Add a m e | a -> e where + add :: a -> e -> m () + +data T (m :: Type -> Type) = T + +instance PrimMonad m => New (T m) m where + new = return T + +instance PrimMonad m => Add (T m) m Int where + add _ _ = return () + +test1 :: forall m. PrimMonad m => m () +test1 = do + ref <- newMutVar (undefined :: T m) + let g () = do + t <- new + add t (0 :: Int) + writeMutVar ref t + g () + +test2 :: forall m. PrimMonad m => m () +test2 = do + (ref :: MutVar (PrimState m) (T m)) <- newMutVar undefined + let g () = do + t <- new + add t (0 :: Int) + writeMutVar ref t + g () diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T index b2232d8f6e..b3a24ba4bf 100644 --- a/testsuite/tests/typecheck/should_compile/all.T +++ b/testsuite/tests/typecheck/should_compile/all.T @@ -867,6 +867,7 @@ test('T23018', normal, compile, ['']) test('T21909', normal, compile, ['']) test('T21909b', normal, compile, ['']) test('T21443', normal, compile, ['']) +test('T22194', normal, compile, ['']) test('QualifiedRecordUpdate', [ extra_files(['QualifiedRecordUpdate_aux.hs']) ] , multimod_compile, ['QualifiedRecordUpdate', '-v0']) diff --git a/testsuite/tests/typecheck/should_fail/T12785b.stderr b/testsuite/tests/typecheck/should_fail/T12785b.stderr index abcdee7619..5957527a61 100644 --- a/testsuite/tests/typecheck/should_fail/T12785b.stderr +++ b/testsuite/tests/typecheck/should_fail/T12785b.stderr @@ -1,6 +1,6 @@ T12785b.hs:30:65: error: [GHC-25897] - • Could not deduce ‘Payload (S n) (Payload n s1) ~ s’ + • Could not deduce ‘s ~ Payload (S n) (Payload n s1)’ arising from a use of ‘SBranchX’ from the context: m ~ S n bound by a pattern with constructor: diff --git a/testsuite/tests/typecheck/should_fail/T7869.stderr b/testsuite/tests/typecheck/should_fail/T7869.stderr index f6aa8d0bfc..d8532ea365 100644 --- a/testsuite/tests/typecheck/should_fail/T7869.stderr +++ b/testsuite/tests/typecheck/should_fail/T7869.stderr @@ -1,18 +1,16 @@ T7869.hs:3:12: error: [GHC-25897] - • Couldn't match type ‘a1’ with ‘a’ + • Couldn't match type ‘b1’ with ‘b’ Expected: [a1] -> b1 Actual: [a] -> b - ‘a1’ is a rigid type variable bound by + ‘b1’ is a rigid type variable bound by an expression type signature: forall a1 b1. [a1] -> b1 at T7869.hs:3:20-27 - ‘a’ is a rigid type variable bound by + ‘b’ is a rigid type variable bound by the inferred type of f :: [a] -> b at T7869.hs:3:1-27 • In the expression: f x In the expression: (\ x -> f x) :: [a] -> b In an equation for ‘f’: f = (\ x -> f x) :: [a] -> b - • Relevant bindings include - x :: [a1] (bound at T7869.hs:3:7) - f :: [a] -> b (bound at T7869.hs:3:1) + • Relevant bindings include f :: [a] -> b (bound at T7869.hs:3:1) diff --git a/testsuite/tests/typecheck/should_fail/tcfail097.stderr b/testsuite/tests/typecheck/should_fail/tcfail097.stderr index bad134d6bd..1caa93ab8d 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail097.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail097.stderr @@ -8,9 +8,9 @@ tcfail097.hs:5:6: error: [GHC-39999] The type variable ‘a0’ is ambiguous Potentially matching instances: instance Eq Ordering -- Defined in ‘GHC.Classes’ - instance Eq Integer -- Defined in ‘GHC.Num.Integer’ - ...plus 23 others - ...plus four instances involving out-of-scope types + instance Eq a => Eq (Solo a) -- Defined in ‘GHC.Classes’ + ...plus 22 others + ...plus five instances involving out-of-scope types (use -fprint-potential-instances to see them all) • In the ambiguity check for ‘f’ To defer the ambiguity check to use sites, enable AllowAmbiguousTypes |