summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--compiler/GHC/Core/Coercion.hs2
-rw-r--r--compiler/GHC/Core/Map/Type.hs7
-rw-r--r--compiler/GHC/Core/Reduction.hs2
-rw-r--r--compiler/GHC/Core/TyCo/Rep.hs80
-rw-r--r--compiler/GHC/Core/Type.hs62
-rw-r--r--compiler/GHC/Core/Unify.hs6
-rw-r--r--compiler/GHC/Tc/Gen/HsType.hs17
-rw-r--r--compiler/GHC/Tc/Solver/Canonical.hs5
-rw-r--r--compiler/GHC/Tc/Solver/Rewrite.hs52
-rw-r--r--compiler/GHC/Tc/Utils/TcType.hs34
-rw-r--r--testsuite/tests/typecheck/should_compile/T19677.hs19
-rw-r--r--testsuite/tests/typecheck/should_compile/all.T1
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, [''])