diff options
| -rw-r--r-- | compiler/GHC/Core/Coercion.hs | 2 | ||||
| -rw-r--r-- | compiler/GHC/Core/Map/Type.hs | 7 | ||||
| -rw-r--r-- | compiler/GHC/Core/Reduction.hs | 2 | ||||
| -rw-r--r-- | compiler/GHC/Core/TyCo/Rep.hs | 80 | ||||
| -rw-r--r-- | compiler/GHC/Core/Type.hs | 62 | ||||
| -rw-r--r-- | compiler/GHC/Core/Unify.hs | 6 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Gen/HsType.hs | 17 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Solver/Canonical.hs | 5 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Solver/Rewrite.hs | 52 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Utils/TcType.hs | 34 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_compile/T19677.hs | 19 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_compile/all.T | 1 |
12 files changed, 215 insertions, 72 deletions
diff --git a/compiler/GHC/Core/Coercion.hs b/compiler/GHC/Core/Coercion.hs index ac09b0a7c4..a7b4a33584 100644 --- a/compiler/GHC/Core/Coercion.hs +++ b/compiler/GHC/Core/Coercion.hs @@ -477,7 +477,7 @@ decomposePiCos orig_co (Pair orig_k1 orig_k2) orig_args -> (TCvSubst,Kind) -- Rhs kind of coercion -> [Type] -- Arguments to that function -> ([CoercionN], Coercion) - -- Invariant: co :: subst1(k2) ~ subst2(k2) + -- Invariant: co :: subst1(k1) ~ subst2(k2) go acc_arg_cos (subst1,k1) co (subst2,k2) (ty:tys) | Just (a, t1) <- splitForAllTyCoVar_maybe k1 diff --git a/compiler/GHC/Core/Map/Type.hs b/compiler/GHC/Core/Map/Type.hs index 32b3fe054b..15c624d8b3 100644 --- a/compiler/GHC/Core/Map/Type.hs +++ b/compiler/GHC/Core/Map/Type.hs @@ -48,13 +48,13 @@ import GHC.Types.Var.Env import GHC.Types.Unique.FM import GHC.Utils.Outputable -import GHC.Data.Maybe import GHC.Utils.Panic import qualified Data.Map as Map import qualified Data.IntMap as IntMap import Control.Monad ( (>=>) ) +import GHC.Data.Maybe -- NB: Be careful about RULES and type families (#5821). So we should make sure -- to specify @Key TypeMapX@ (and not @DeBruijn Type@, the reduced form) @@ -136,16 +136,17 @@ xtC (D env co) f (CoercionMapX m) type TypeMapG = GenMap TypeMapX -- | @TypeMapX a@ is the base map from @DeBruijn Type@ to @a@, but without the --- 'GenMap' optimization. +-- 'GenMap' optimization. See Note [Computing equality on types] in GHC.Core.Type. data TypeMapX a = TM { tm_var :: VarMap a - , tm_app :: TypeMapG (TypeMapG a) + , tm_app :: TypeMapG (TypeMapG a) -- Note [Equality on AppTys] in GHC.Core.Type , tm_tycon :: DNameEnv a -- only InvisArg arrows here , tm_funty :: TypeMapG (TypeMapG (TypeMapG a)) -- keyed on the argument, result rep, and result -- constraints are never linear-restricted and are always lifted + -- See also Note [Equality on FunTys] in GHC.Core.TyCo.Rep , tm_forall :: TypeMapG (BndrMap a) -- See Note [Binders] in GHC.Core.Map.Expr , tm_tylit :: TyLitMap a diff --git a/compiler/GHC/Core/Reduction.hs b/compiler/GHC/Core/Reduction.hs index 254b4420e1..fbae18f797 100644 --- a/compiler/GHC/Core/Reduction.hs +++ b/compiler/GHC/Core/Reduction.hs @@ -807,7 +807,7 @@ simplifyArgsWorker orig_ki_binders orig_inner_ki orig_fvs orig_ki_binders orig_inner_ki orig_roles orig_simplified_args where - orig_lc = emptyLiftingContext $ mkInScopeSet $ orig_fvs + orig_lc = emptyLiftingContext $ mkInScopeSet orig_fvs go :: LiftingContext -- mapping from tyvars to rewriting coercions -> [TyCoBinder] -- Unsubsted binders of function's kind diff --git a/compiler/GHC/Core/TyCo/Rep.hs b/compiler/GHC/Core/TyCo/Rep.hs index 513001e42d..f1dcd8bfd6 100644 --- a/compiler/GHC/Core/TyCo/Rep.hs +++ b/compiler/GHC/Core/TyCo/Rep.hs @@ -166,10 +166,10 @@ data Type | CastTy Type KindCoercion -- ^ A kind cast. The coercion is always nominal. - -- INVARIANT: The cast is never reflexive - -- INVARIANT: The Type is not a CastTy (use TransCo instead) - -- INVARIANT: The Type is not a ForAllTy over a type variable - -- See Note [Respecting definitional equality] \(EQ2), (EQ3), (EQ4) + -- INVARIANT: The cast is never reflexive \(EQ2) + -- INVARIANT: The Type is not a CastTy (use TransCo instead) \(EQ3) + -- INVARIANT: The Type is not a ForAllTy over a tyvar \(EQ4) + -- See Note [Respecting definitional equality] | CoercionTy Coercion -- ^ Injection of a Coercion into a type @@ -302,6 +302,31 @@ When treated as a user type, In a FunTy { ft_af = InvisArg }, the argument type is always a Predicate type. +Note [Weird typing rule for ForAllTy] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Here are the typing rules for ForAllTy: + +tyvar : Type +inner : TYPE r +tyvar does not occur in r +------------------------------------ +ForAllTy (Bndr tyvar vis) inner : TYPE r + +inner : TYPE r +------------------------------------ +ForAllTy (Bndr covar vis) inner : Type + +Note that the kind of the result depends on whether the binder is a +tyvar or a covar. The kind of a forall-over-tyvar is the same as +the kind of the inner type. This is because quantification over types +is erased before runtime. By contrast, the kind of a forall-over-covar +is always Type, because a forall-over-covar is compiled into a function +taking a 0-bit-wide erased coercion argument. + +Because the tyvar form above includes r in its result, we must +be careful not to let any variables escape -- thus the last premise +of the rule above. + Note [Constraints in kinds] ~~~~~~~~~~~~~~~~~~~~~~~~~~~ Do we allow a type constructor to have a kind like @@ -452,7 +477,7 @@ casting. The same is true of expressions of type σ. So in some sense, τ and σ are interchangeable. But let's be more precise. If we examine the typing rules of FC (say, those in -https://cs.brynmawr.edu/~rae/papers/2015/equalities/equalities.pdf) +https://richarde.dev/papers/2015/equalities/equalities.pdf) there are several places where the same metavariable is used in two different premises to a rule. (For example, see Ty_App.) There is an implicit equality check here. What definition of equality should we use? By convention, we use @@ -470,7 +495,7 @@ equality check, can use any homogeneous relation that is smaller than ~, as those rules must also be admissible. A more drawn out argument around all of this is presented in Section 7.2 of -Richard E's thesis (http://cs.brynmawr.edu/~rae/papers/2016/thesis/eisenberg-thesis.pdf). +Richard E's thesis (http://richarde.dev/papers/2016/thesis/eisenberg-thesis.pdf). What would go wrong if we insisted on the casts matching? See the beginning of Section 8 in the unpublished paper above. Theoretically, nothing at all goes @@ -482,8 +507,8 @@ then we couldn't discard -- the output of kind-checking would be enormous, and we would need enormous casts with lots of CoherenceCo's to straighten them out. -Would anything go wrong if eqType respected type families? No, not at all. But -that makes eqType rather hard to implement. +Would anything go wrong if eqType looked through type families? No, not at +all. But that makes eqType rather hard to implement. Thus, the guideline for eqType is that it should be the largest easy-to-implement relation that is still smaller than ~ and homogeneous. The @@ -497,6 +522,23 @@ Another helpful principle with eqType is this: This principle also tells us that eqType must relate only types with the same kinds. +Interestingly, it must be the case that the free variables of t1 and t2 +might be different, even if t1 `eqType` t2. A simple example of this is +if we have both cv1 :: k1 ~ k2 and cv2 :: k1 ~ k2 in the environment. +Then t1 = t |> cv1 and t2 = t |> cv2 are eqType; yet cv1 is in the free +vars of t1 and cv2 is in the free vars of t2. Unless we choose to implement +eqType to be just α-equivalence, this wrinkle around free variables +remains. + +Yet not all is lost: we can say that any two equal types share the same +*relevant* free variables. Here, a relevant variable is a shallow +free variable (see Note [Shallow and deep free variables] in GHC.Core.TyCo.FVs) +that does not appear within a coercion. Note that type variables can +appear within coercions (in, say, a Refl node), but that coercion variables +cannot appear outside a coercion. We do not (yet) have a function to +extract relevant free variables, but it would not be hard to write if +the need arises. + Besides eqType, another equality relation that upholds the (EQ) property above is /typechecker equality/, which is implemented as GHC.Tc.Utils.TcType.tcEqType. See @@ -525,7 +567,7 @@ to differ, leading to a contradiction. Thus, co is reflexive. Accordingly, by eliminating reflexive casts, splitTyConApp need not worry about outermost casts to uphold (EQ). Eliminating reflexive casts is done -in mkCastTy. +in mkCastTy. This is (EQ1) below. Unforunately, that's not the end of the story. Consider comparing (T a b c) =? (T a b |> (co -> <Type>)) (c |> co) @@ -548,6 +590,7 @@ our (EQ) property. In order to detect reflexive casts reliably, we must make sure not to have nested casts: we update (t |> co1 |> co2) to (t |> (co1 `TransCo` co2)). +This is (EQ2) below. One other troublesome case is ForAllTy. See Note [Weird typing rule for ForAllTy]. The kind of the body is the same as the kind of the ForAllTy. Accordingly, @@ -570,6 +613,25 @@ In sum, in order to uphold (EQ), we need the following invariants: These invariants are all documented above, in the declaration for Type. +Note [Equality on FunTys] +~~~~~~~~~~~~~~~~~~~~~~~~~ +A (FunTy vis mult arg res) is just an abbreviation for a + TyConApp funTyCon [mult, arg_rep, res_rep, arg, res] +where + arg :: TYPE arg_rep + res :: TYPE res_rep +Note that the vis field of a FunTy appears nowhere in the +equivalent TyConApp. In Core, this is OK, because we no longer +care about the visibility of the argument in a FunTy +(the vis distinguishes between arg -> res and arg => res). +In the type-checker, we are careful not to decompose FunTys +with an invisible argument. See also Note [Decomposing fat arrow c=>t] +in GHC.Core.Type. + +In order to compare FunTys while respecting how they could +expand into TyConApps, we must check +the kinds of the arg and the res. + Note [Unused coercion variable in ForAllTy] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Suppose we have diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs index 6b88262ff5..0d82c010c0 100644 --- a/compiler/GHC/Core/Type.hs +++ b/compiler/GHC/Core/Type.hs @@ -43,6 +43,7 @@ module GHC.Core.Type ( tcSplitTyConApp_maybe, splitListTyConApp_maybe, repSplitTyConApp_maybe, + tcRepSplitTyConApp_maybe, mkForAllTy, mkForAllTys, mkInvisForAllTys, mkTyCoInvForAllTys, mkSpecForAllTy, mkSpecForAllTys, @@ -1058,13 +1059,16 @@ tcRepSplitAppTy_maybe :: Type -> Maybe (Type,Type) -- ^ Does the AppTy split as in 'tcSplitAppTy_maybe', but assumes that -- any coreView stuff is already done. Refuses to look through (c => t) tcRepSplitAppTy_maybe (FunTy { ft_af = af, ft_mult = w, ft_arg = ty1, ft_res = ty2 }) - | InvisArg <- af - = Nothing -- See Note [Decomposing fat arrow c=>t] - | otherwise + | VisArg <- af -- See Note [Decomposing fat arrow c=>t] + + -- See Note [The Purely Kinded Type Invariant (PKTI)] in GHC.Tc.Gen.HsType, + -- Wrinkle around FunTy + , Just rep1 <- getRuntimeRep_maybe ty1 + , Just rep2 <- getRuntimeRep_maybe ty2 = Just (TyConApp funTyCon [w, rep1, rep2, ty1], ty2) - where - rep1 = getRuntimeRep ty1 - rep2 = getRuntimeRep ty2 + + | otherwise + = Nothing tcRepSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2) tcRepSplitAppTy_maybe (TyConApp tc tys) @@ -1472,30 +1476,39 @@ splitTyConApp_maybe = repSplitTyConApp_maybe . coreFullView tcSplitTyConApp_maybe :: HasCallStack => Type -> Maybe (TyCon, [Type]) -- Defined here to avoid module loops between Unify and TcType. tcSplitTyConApp_maybe ty | Just ty' <- tcView ty = tcSplitTyConApp_maybe ty' -tcSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys) -tcSplitTyConApp_maybe (FunTy VisArg w arg res) - | Just arg_rep <- getRuntimeRep_maybe arg - , Just res_rep <- getRuntimeRep_maybe res - = Just (funTyCon, [w, arg_rep, res_rep, arg, res]) -tcSplitTyConApp_maybe _ = Nothing + | otherwise = tcRepSplitTyConApp_maybe ty ------------------- repSplitTyConApp_maybe :: HasDebugCallStack => Type -> Maybe (TyCon, [Type]) -- ^ Like 'splitTyConApp_maybe', but doesn't look through synonyms. This -- assumes the synonyms have already been dealt with. +repSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys) +repSplitTyConApp_maybe (FunTy _ w arg res) + -- NB: we're in Core, so no check for VisArg + = Just (funTyCon, [w, arg_rep, res_rep, arg, res]) + where + arg_rep = getRuntimeRep arg + res_rep = getRuntimeRep res +repSplitTyConApp_maybe _ = Nothing + +tcRepSplitTyConApp_maybe :: HasDebugCallStack => Type -> Maybe (TyCon, [Type]) +-- ^ Like 'tcSplitTyConApp_maybe', but doesn't look through synonyms. This +-- assumes the synonyms have already been dealt with. -- -- Moreover, for a FunTy, it only succeeds if the argument types -- have enough info to extract the runtime-rep arguments that -- the funTyCon requires. This will usually be true; -- but may be temporarily false during canonicalization: -- see Note [Decomposing FunTy] in GHC.Tc.Solver.Canonical --- -repSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys) -repSplitTyConApp_maybe (FunTy _ w arg res) +-- and Note [The Purely Kinded Type Invariant (PKTI)] in GHC.Tc.Gen.HsType, +-- Wrinkle around FunTy +tcRepSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys) +tcRepSplitTyConApp_maybe (FunTy VisArg w arg res) + -- NB: VisArg. See Note [Decomposing fat arrow c=>t] | Just arg_rep <- getRuntimeRep_maybe arg , Just res_rep <- getRuntimeRep_maybe res = Just (funTyCon, [w, arg_rep, res_rep, arg, res]) -repSplitTyConApp_maybe _ = Nothing +tcRepSplitTyConApp_maybe _ = Nothing ------------------- -- | Attempts to tease a list type apart and gives the type of the elements if @@ -2540,6 +2553,17 @@ ordering leads to nondeterminism. We hit the same problem in the TyVarTy case, comparing type variables is nondeterministic, note the call to nonDetCmpVar in nonDetCmpTypeX. See Note [Unique Determinism] for more details. + +Note [Computing equality on types] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +There are several places within GHC that depend on the precise choice of +definitional equality used. If we change that definition, all these places +must be updated. This Note merely serves as a place for all these places +to refer to, so searching for references to this Note will find every place +that needs to be updated. + +See also Note [Non-trivial definitional equality] in GHC.Core.TyCo.Rep. + -} nonDetCmpType :: Type -> Type -> Ordering @@ -2569,6 +2593,7 @@ data TypeOrdering = TLT -- ^ @t1 < t2@ nonDetCmpTypeX :: RnEnv2 -> Type -> Type -> Ordering -- Main workhorse -- See Note [Non-trivial definitional equality] in GHC.Core.TyCo.Rep + -- See Note [Computing equality on types] nonDetCmpTypeX env orig_t1 orig_t2 = case go env orig_t1 orig_t2 of -- If there are casts then we also need to do a comparison of the kinds of @@ -2623,7 +2648,10 @@ nonDetCmpTypeX env orig_t1 orig_t2 = | Just (s1, t1) <- repSplitAppTy_maybe ty1 = go env s1 s2 `thenCmpTy` go env t1 t2 go env (FunTy _ w1 s1 t1) (FunTy _ w2 s2 t2) - = go env s1 s2 `thenCmpTy` go env t1 t2 `thenCmpTy` go env w1 w2 + -- NB: nonDepCmpTypeX does the kind check requested by + -- Note [Equality on FunTys] in GHC.Core.TyCo.Rep + = liftOrdering (nonDetCmpTypeX env s1 s2 `thenCmp` nonDetCmpTypeX env t1 t2) + `thenCmpTy` go env w1 w2 -- Comparing multiplicities last because the test is usually true go env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = liftOrdering (tc1 `nonDetCmpTc` tc2) `thenCmpTy` gos env tys1 tys2 diff --git a/compiler/GHC/Core/Unify.hs b/compiler/GHC/Core/Unify.hs index bd54ecee39..2e6b89f355 100644 --- a/compiler/GHC/Core/Unify.hs +++ b/compiler/GHC/Core/Unify.hs @@ -800,14 +800,14 @@ see Note [Non-trivial definitional equality] in GHC.Core.TyCo.Rep Unlike the "impure unifiers" in the typechecker (the eager unifier in GHC.Tc.Utils.Unify, and the constraint solver itself in GHC.Tc.Solver.Canonical), the pure -unifier It does /not/ work up to ~. +unifier does /not/ work up to ~. The algorithm implemented here is rather delicate, and we depend on it to uphold certain properties. This is a summary of these required properties. Notation: - θ,φ substitutions + θ,φ substitutions ξ type-function-free types τ,σ other types τ♭ type τ, flattened @@ -1067,7 +1067,7 @@ unify_ty :: UMEnv -> UM () -- See Note [Specification of unification] -- Respects newtypes, PredTypes - +-- See Note [Computing equality on types] in GHC.Core.Type unify_ty env ty1 ty2 kco -- See Note [Comparing nullary type synonyms] in GHC.Core.Type. | TyConApp tc1 [] <- ty1 diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs index 7d9682582a..8628f75d99 100644 --- a/compiler/GHC/Tc/Gen/HsType.hs +++ b/compiler/GHC/Tc/Gen/HsType.hs @@ -1808,7 +1808,22 @@ that (a Int) will satisfy (PKTI). The absence of this caused #14174 and #14520. -The calls to mkAppTyM is the other place we are very careful. +The calls to mkAppTyM is the other place we are very careful; see Note [mkAppTyM]. + +Wrinkle around FunTy: +Note that the PKTI does *not* guarantee anything about the shape of FunTys. +Specifically, when we have (FunTy vis mult arg res), it should be the case +that arg :: TYPE rr1 and res :: TYPE rr2, for some rr1 and rr2. However, we +might not have this. Example: if the user writes (a -> b), then we might +invent a :: kappa1 and b :: kappa2. We soon will check whether kappa1 ~ TYPE rho1 +(for some rho1), and that will lead to kappa1 := TYPE rho1 (ditto for kappa2). +However, when we build the FunTy, we might not have zonked `a`, and so the +FunTy will be built without being able to purely extract the RuntimeReps. + +Because the PKTI does not guarantee that the RuntimeReps are available in a FunTy, +we must be aware of this when splitting: splitTyConApp and splitAppTy will *not* +split a FunTy if the RuntimeReps are not available. See also Note [Decomposing FunTy] +in GHC.Tc.Solver.Canonical. Note [mkAppTyM] ~~~~~~~~~~~~~~~ diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs index e8c4ee82e2..cdb86b92e2 100644 --- a/compiler/GHC/Tc/Solver/Canonical.hs +++ b/compiler/GHC/Tc/Solver/Canonical.hs @@ -914,7 +914,6 @@ track whether or not we've already rewritten. It is conceivable to do a better job at tracking whether or not a type is rewritten, but this is left as future work. (Mar '15) - Note [Decomposing FunTy] ~~~~~~~~~~~~~~~~~~~~~~~~ can_eq_nc' may attempt to decompose a FunTy that is un-zonked. This @@ -1291,8 +1290,8 @@ zonk_eq_types = go split2 = tcSplitFunTy_maybe ty2 go ty1 ty2 - | Just (tc1, tys1) <- repSplitTyConApp_maybe ty1 - , Just (tc2, tys2) <- repSplitTyConApp_maybe ty2 + | Just (tc1, tys1) <- tcRepSplitTyConApp_maybe ty1 + , Just (tc2, tys2) <- tcRepSplitTyConApp_maybe ty2 = if tc1 == tc2 && tys1 `equalLength` tys2 -- Crucial to check for equal-length args, because -- we cannot assume that the two args to 'go' have diff --git a/compiler/GHC/Tc/Solver/Rewrite.hs b/compiler/GHC/Tc/Solver/Rewrite.hs index 82c6c580a4..3f2f8f35ce 100644 --- a/compiler/GHC/Tc/Solver/Rewrite.hs +++ b/compiler/GHC/Tc/Solver/Rewrite.hs @@ -41,6 +41,8 @@ import GHC.Exts (oneShot) import Control.Monad import GHC.Utils.Monad ( zipWith3M ) import Data.List.NonEmpty ( NonEmpty(..) ) +import Control.Applicative (liftA3) +import GHC.Builtin.Types.Prim (tYPETyCon) {- ************************************************************************ @@ -470,28 +472,28 @@ rewrite_args_slow binders inner_ki fvs roles tys -- a Derived rewriting a Derived. The solution would be to generate evidence for -- Deriveds, thus avoiding this whole noBogusCoercions idea. See also -- Note [No derived kind equalities] - = do { rewritten_args <- zipWith3M fl (map isNamedBinder binders ++ repeat True) + = do { rewritten_args <- zipWith3M rw (map isNamedBinder binders ++ repeat True) roles tys ; return $ simplifyArgsWorker binders inner_ki fvs roles rewritten_args } where - {-# INLINE fl #-} - fl :: Bool -- must we ensure to produce a real coercion here? + {-# INLINE rw #-} + rw :: Bool -- must we ensure to produce a real coercion here? -- see comment at top of function -> Role -> Type -> RewriteM Reduction - fl True r ty = noBogusCoercions $ fl1 r ty - fl False r ty = fl1 r ty + rw True r ty = noBogusCoercions $ rw1 r ty + rw False r ty = rw1 r ty - {-# INLINE fl1 #-} - fl1 :: Role -> Type -> RewriteM Reduction - fl1 Nominal ty + {-# INLINE rw1 #-} + rw1 :: Role -> Type -> RewriteM Reduction + rw1 Nominal ty = setEqRel NomEq $ rewrite_one ty - fl1 Representational ty + rw1 Representational ty = setEqRel ReprEq $ rewrite_one ty - fl1 Phantom ty + rw1 Phantom ty -- See Note [Phantoms in the rewriter] = do { ty <- liftTcS $ zonkTcType ty ; return $ mkReflRedn Phantom ty } @@ -533,9 +535,35 @@ rewrite_one (TyConApp tc tys) rewrite_one (FunTy { ft_af = vis, ft_mult = mult, ft_arg = ty1, ft_res = ty2 }) = do { arg_redn <- rewrite_one ty1 ; res_redn <- rewrite_one ty2 - ; w_redn <- setEqRel NomEq $ rewrite_one mult + + -- Important: look at the *reduced* type, so that any unzonked variables + -- in kinds are gone and the getRuntimeRep succeeds. + -- cf. Note [Decomposing FunTy] in GHC.Tc.Solver.Canonical. + ; let arg_rep = getRuntimeRep (reductionReducedType arg_redn) + res_rep = getRuntimeRep (reductionReducedType res_redn) + + ; (w_redn, arg_rep_redn, res_rep_redn) <- setEqRel NomEq $ + liftA3 (,,) (rewrite_one mult) + (rewrite_one arg_rep) + (rewrite_one res_rep) ; role <- getRole - ; return $ mkFunRedn role vis w_redn arg_redn res_redn } + + ; let arg_rep_co = reductionCoercion arg_rep_redn + -- :: arg_rep ~ arg_rep_xi + arg_ki_co = mkTyConAppCo Nominal tYPETyCon [arg_rep_co] + -- :: TYPE arg_rep ~ TYPE arg_rep_xi + casted_arg_redn = mkCoherenceRightRedn role arg_redn arg_ki_co + -- :: ty1 ~> arg_xi |> arg_ki_co + + res_rep_co = reductionCoercion res_rep_redn + res_ki_co = mkTyConAppCo Nominal tYPETyCon [res_rep_co] + casted_res_redn = mkCoherenceRightRedn role res_redn res_ki_co + + -- We must rewrite the representations, because that's what would + -- be done if we used TyConApp instead of FunTy. These rewritten + -- representations are seen only in casts of the arg and res, below. + -- Forgetting this caused #19677. + ; return $ mkFunRedn role vis w_redn casted_arg_redn casted_res_redn } rewrite_one ty@(ForAllTy {}) -- TODO (RAE): This is inadequate, as it doesn't rewrite the kind of diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs index 367922e3e5..d878ccc75a 100644 --- a/compiler/GHC/Tc/Utils/TcType.hs +++ b/compiler/GHC/Tc/Utils/TcType.hs @@ -625,6 +625,10 @@ EQUAL TO, but we'd need to think carefully about But in fact (GivenInv) is automatically true, so we're adhering to it for now. See #18929. +* If a tyvar tv has level n, then the levels of all variables free + in tv's kind are <= n. Consequence: if tv is untouchable, so are + all variables in tv's kind. + Note [WantedInv] ~~~~~~~~~~~~~~~~ Why is WantedInv important? Consider this implication, where @@ -1591,6 +1595,7 @@ tc_eq_type :: Bool -- ^ True <=> do not expand type synonyms -> Type -> Type -> Bool -- Flags False, False is the usual setting for tc_eq_type +-- See Note [Computing equality on types] in Type tc_eq_type keep_syns vis_only orig_ty1 orig_ty2 = go orig_env orig_ty1 orig_ty2 where @@ -1620,10 +1625,14 @@ tc_eq_type keep_syns vis_only orig_ty1 orig_ty2 -- Make sure we handle all FunTy cases since falling through to the -- AppTy case means that tcRepSplitAppTy_maybe may see an unzonked -- kind variable, which causes things to blow up. + -- See Note [Equality on FunTys] in GHC.Core.TyCo.Rep: we must check + -- kinds here go env (FunTy _ w1 arg1 res1) (FunTy _ w2 arg2 res2) - = go env w1 w2 && go env arg1 arg2 && go env res1 res2 - go env ty (FunTy _ w arg res) = eqFunTy env w arg res ty - go env (FunTy _ w arg res) ty = eqFunTy env w arg res ty + = kinds_eq && go env arg1 arg2 && go env res1 res2 && go env w1 w2 + where + kinds_eq | vis_only = True + | otherwise = go env (typeKind arg1) (typeKind arg2) && + go env (typeKind res1) (typeKind res2) -- See Note [Equality on AppTys] in GHC.Core.Type go env (AppTy s1 t1) ty2 @@ -1658,25 +1667,6 @@ tc_eq_type keep_syns vis_only orig_ty1 orig_ty2 orig_env = mkRnEnv2 $ mkInScopeSet $ tyCoVarsOfTypes [orig_ty1, orig_ty2] - -- @eqFunTy w arg res ty@ is True when @ty@ equals @FunTy w arg res@. This is - -- sometimes hard to know directly because @ty@ might have some casts - -- obscuring the FunTy. And 'splitAppTy' is difficult because we can't - -- always extract a RuntimeRep (see Note [xyz]) if the kind of the arg or - -- res is unzonked. Thus this function, which handles this - -- corner case. - eqFunTy :: RnEnv2 -> Mult -> Type -> Type -> Type -> Bool - -- Last arg is /not/ FunTy - eqFunTy env w arg res ty@(AppTy{}) = get_args ty [] - where - get_args :: Type -> [Type] -> Bool - get_args (AppTy f x) args = get_args f (x:args) - get_args (CastTy t _) args = get_args t args - get_args (TyConApp tc tys) args - | tc == funTyCon - , [w', _, _, arg', res'] <- tys ++ args - = go env w w' && go env arg arg' && go env res res' - get_args _ _ = False - eqFunTy _ _ _ _ _ = False {-# INLINE tc_eq_type #-} -- See Note [Specialising tc_eq_type]. {- Note [Typechecker equality vs definitional equality] diff --git a/testsuite/tests/typecheck/should_compile/T19677.hs b/testsuite/tests/typecheck/should_compile/T19677.hs new file mode 100644 index 0000000000..1b29beb0d1 --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T19677.hs @@ -0,0 +1,19 @@ +{-# LANGUAGE ExplicitForAll, PolyKinds, DataKinds, TypeFamilies, GADTs #-} + +module T19677 where + +import GHC.Exts + +class C x where + meth :: x -> () +instance C (a -> b) where + meth _ = () + +type family Lifty throttle where + Lifty Int = LiftedRep + +data G a where + MkG :: G Int + +foo :: forall i (a :: TYPE (Lifty i)) (b :: TYPE (Lifty i)). G i -> (a -> b) -> () +foo MkG = meth diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T index 72105683a5..beccd0a597 100644 --- a/testsuite/tests/typecheck/should_compile/all.T +++ b/testsuite/tests/typecheck/should_compile/all.T @@ -739,6 +739,7 @@ test('T18412', normal, compile, ['']) test('T18470', normal, compile, ['']) test('T18308', normal, compile, ['']) test('T18323', normal, compile, ['']) +test('T19677', normal, compile, ['']) test('T18585', normal, compile, ['']) test('T18831', normal, compile, ['']) test('T18920', normal, compile, ['']) |