diff options
| -rw-r--r-- | compiler/typecheck/TcFlatten.hs | 12 | ||||
| -rw-r--r-- | compiler/typecheck/TcHsType.hs | 5 | ||||
| -rw-r--r-- | compiler/types/Coercion.hs | 110 | ||||
| -rw-r--r-- | compiler/types/Coercion.hs-boot | 2 | ||||
| -rw-r--r-- | compiler/types/Type.hs | 4 | ||||
| -rw-r--r-- | testsuite/tests/dependent/should_fail/T15343.hs | 14 | ||||
| -rw-r--r-- | testsuite/tests/dependent/should_fail/T15343.stderr | 7 | ||||
| -rw-r--r-- | testsuite/tests/dependent/should_fail/all.T | 2 |
8 files changed, 107 insertions, 49 deletions
diff --git a/compiler/typecheck/TcFlatten.hs b/compiler/typecheck/TcFlatten.hs index ee13091681..529fbaffe9 100644 --- a/compiler/typecheck/TcFlatten.hs +++ b/compiler/typecheck/TcFlatten.hs @@ -1315,10 +1315,16 @@ flatten_args_slow orig_binders orig_inner_ki orig_fvs orig_roles orig_tys go acc_xis acc_cos lc [] inner_ki roles tys | Just k <- tcGetTyVar_maybe inner_ki , Just co1 <- liftCoSubstTyVar lc Nominal k - = do { let Pair flattened_kind _ = coercionKind co1 - (arg_cos, res_co) = decomposePiCos flattened_kind tys co1 - casted_tys = zipWith mkCastTy tys arg_cos + = do { let co1_kind = coercionKind co1 + (arg_cos, res_co) = decomposePiCos co1 co1_kind tys + casted_tys = ASSERT2( equalLength tys arg_cos + , ppr tys $$ ppr arg_cos ) + zipWith mkCastTy tys arg_cos + -- In general decomposePiCos can return fewer cos than tys, + -- but not here; see "If we're at all well-typed..." + -- in Note [Last case in flatten_args]. Hence the ASSERT. zapped_lc = zapLiftingContext lc + Pair flattened_kind _ = co1_kind (bndrs, new_inner) = splitPiTys flattened_kind ; (xis_out, cos_out, res_co_out) diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs index 7e5fcef426..463c7e0672 100644 --- a/compiler/typecheck/TcHsType.hs +++ b/compiler/typecheck/TcHsType.hs @@ -356,7 +356,10 @@ tcHsTypeApp :: LHsWcType GhcRn -> Kind -> TcM Type -- See Note [Recipe for checking a signature] in TcHsType tcHsTypeApp wc_ty kind | HsWC { hswc_ext = sig_wcs, hswc_body = hs_ty } <- wc_ty - = do { ty <- tcWildCardBindersX newWildTyVar Nothing sig_wcs $ \ _ -> + = do { ty <- solveLocalEqualities $ + -- We are looking at a user-written type, very like a + -- signature so we want to solve its equalities right now + tcWildCardBindersX newWildTyVar Nothing sig_wcs $ \ _ -> tcCheckLHsType hs_ty kind ; ty <- zonkPromoteType ty ; checkValidType TypeAppCtxt ty diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs index 8493a4ae82..2ca5151f78 100644 --- a/compiler/types/Coercion.hs +++ b/compiler/types/Coercion.hs @@ -271,43 +271,71 @@ decomposeFunCo r co = ASSERT2( all_ok, ppr co ) Pair s1t1 s2t2 = coercionKind co all_ok = isFunTy s1t1 && isFunTy s2t2 --- | Decompose a function coercion, either a dependent one or a non-dependent one. --- This is useful when you are trying to build (ty1 |> co) ty2 ty3 ... tyn, but --- you are pulling the coercions to the right. For example of why you might want --- to do so, see Note [Respecting definitional equality] in TyCoRep. --- This might return *fewer* coercions than there are arguments, if the kind provided --- doesn't have enough binders. --- The types passed in are the ty2 ... tyn. If the results are (arg_cos, res_co), --- then you should build --- @(ty1 (ty2 |> arg_cos1) (ty3 |> arg_cos2) ... (tym |> arg_com)|> res_co) tym+1 ... tyn@. -decomposePiCos :: Kind -- of the function (ty1), used only to tell -> from ∀ from other - -> [Type] -> CoercionN -> ([CoercionN], CoercionN) -decomposePiCos orig_kind orig_args orig_co = go [] orig_subst orig_kind orig_args orig_co +{- Note [Pushing a coercion into a pi-type] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Suppose we have this: + (f |> co) t1 .. tn +Then we want to push the coercion into the arguments, so as to make +progress. For example of why you might want to do so, see Note +[Respecting definitional equality] in TyCoRep. + +This is done by decomposePiCos. Specifically, if + decomposePiCos co [t1,..,tn] = ([co1,...,cok], cor) +then + (f |> co) t1 .. tn = (f (t1 |> co1) ... (tk |> cok)) |> cor) t(k+1) ... tn + +Notes: + +* k can be smaller than n! That is decomposePiCos can return *fewer* + coercions than there are arguments (ie k < n), if the kind provided + doesn't have enough binders. + +* If there is a type error, we might see + (f |> co) t1 + where co :: (forall a. ty) ~ (ty1 -> ty2) + Here 'co' is insoluble, but we don't want to crash in decoposePiCos. + So decomposePiCos carefully tests both sides of the coercion to check + they are both foralls or both arrows. Not doing this caused Trac #15343. +-} + +decomposePiCos :: HasDebugCallStack + => CoercionN -> Pair Type -- Coercion and its kind + -> [Type] + -> ([CoercionN], CoercionN) +-- See Note [Pushing a coercion into a pi-type] +decomposePiCos orig_co (Pair orig_k1 orig_k2) orig_args + = go [] (orig_subst,orig_k1) orig_co (orig_subst,orig_k2) orig_args where - orig_subst = mkEmptyTCvSubst $ mkInScopeSet $ tyCoVarsOfTypes (orig_kind : orig_args) - `unionVarSet` tyCoVarsOfCo orig_co - - go :: [CoercionN] -- accumulator for argument coercions, reversed - -> TCvSubst -- instantiating substitution - -> Kind -- of the function being applied (unsubsted) - -> [Type] -- arguments to that function - -> CoercionN -- coercion originally applied to the function + orig_subst = mkEmptyTCvSubst $ mkInScopeSet $ + tyCoVarsOfTypes orig_args `unionVarSet` tyCoVarsOfCo orig_co + + go :: [CoercionN] -- accumulator for argument coercions, reversed + -> (TCvSubst,Kind) -- Lhs kind of coercion + -> CoercionN -- coercion originally applied to the function + -> (TCvSubst,Kind) -- Rhs kind of coercion + -> [Type] -- Arguments to that function -> ([CoercionN], Coercion) - go acc_arg_cos subst ki (ty:tys) co - | Just (kv, inner_ki) <- splitForAllTy_maybe ki - -- know co :: (forall a:s1.t1) ~ (forall b:s2.t2) - -- function :: forall a:s1.t1 - -- (the function is not passed to decomposePiCos) - -- ty :: s2 - -- need arg_co :: s2 ~ s1 - -- res_co :: t1[ty |> arg_co / a] ~ t2[ty / b] - = let arg_co = mkNthCo Nominal 0 (mkSymCo co) - res_co = mkInstCo co (mkGReflLeftCo Nominal ty arg_co) - subst' = extendTCvSubst subst kv ty + -- Invariant: co :: subst1(k2) ~ subst2(k2) + + go acc_arg_cos (subst1,k1) co (subst2,k2) (ty:tys) + | Just (a, t1) <- splitForAllTy_maybe k1 + , Just (b, t2) <- splitForAllTy_maybe k2 + -- know co :: (forall a:s1.t1) ~ (forall b:s2.t2) + -- function :: forall a:s1.t1 (the function is not passed to decomposePiCos) + -- a :: s1 + -- b :: s2 + -- ty :: s2 + -- need arg_co :: s2 ~ s1 + -- res_co :: t1[ty |> arg_co / a] ~ t2[ty / b] + = let arg_co = mkNthCo Nominal 0 (mkSymCo co) + res_co = mkInstCo co (mkGReflLeftCo Nominal ty arg_co) + subst1' = extendTCvSubst subst1 a (ty `CastTy` arg_co) + subst2' = extendTCvSubst subst2 b ty in - go (arg_co : acc_arg_cos) subst' inner_ki tys res_co + go (arg_co : acc_arg_cos) (subst1', t1) res_co (subst2', t2) tys - | Just (_arg_ki, res_ki) <- splitFunTy_maybe ki + | Just (_s1, t1) <- splitFunTy_maybe k1 + , Just (_s2, t2) <- splitFunTy_maybe k2 -- know co :: (s1 -> t1) ~ (s2 -> t2) -- function :: s1 -> t1 -- ty :: s2 @@ -316,19 +344,17 @@ decomposePiCos orig_kind orig_args orig_co = go [] orig_subst orig_kind orig_arg = let (sym_arg_co, res_co) = decomposeFunCo Nominal co arg_co = mkSymCo sym_arg_co in - go (arg_co : acc_arg_cos) subst res_ki tys res_co + go (arg_co : acc_arg_cos) (subst1,t1) res_co (subst2,t2) tys - | let substed_ki = substTy subst ki - , isPiTy substed_ki - -- This might happen if we have to substitute in order to see that the kind - -- is a Π-type. - = let subst' = zapTCvSubst subst - in - go acc_arg_cos subst' substed_ki (ty:tys) co + | not (isEmptyTCvSubst subst1) || not (isEmptyTCvSubst subst2) + = go acc_arg_cos (zapTCvSubst subst1, substTy subst1 k1) + co + (zapTCvSubst subst2, substTy subst1 k2) + (ty:tys) -- tys might not be empty, if the left-hand type of the original coercion -- didn't have enough binders - go acc_arg_cos _subst _ki _tys co = (reverse acc_arg_cos, co) + go acc_arg_cos _ki1 co _ki2 _tys = (reverse acc_arg_cos, co) -- | Attempts to obtain the type variable underlying a 'Coercion' getCoVar_maybe :: Coercion -> Maybe CoVar diff --git a/compiler/types/Coercion.hs-boot b/compiler/types/Coercion.hs-boot index 6e6acd752a..89aab441de 100644 --- a/compiler/types/Coercion.hs-boot +++ b/compiler/types/Coercion.hs-boot @@ -38,7 +38,7 @@ mkAxiomRuleCo :: CoAxiomRule -> [Coercion] -> Coercion isGReflCo :: Coercion -> Bool isReflCo :: Coercion -> Bool isReflexiveCo :: Coercion -> Bool -decomposePiCos :: Kind -> [Type] -> Coercion -> ([Coercion], Coercion) +decomposePiCos :: HasDebugCallStack => Coercion -> Pair Type -> [Type] -> ([Coercion], Coercion) coVarKindsTypesRole :: HasDebugCallStack => CoVar -> (Kind, Kind, Type, Type, Role) coVarRole :: CoVar -> Role diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs index 45b1b74382..0833665757 100644 --- a/compiler/types/Type.hs +++ b/compiler/types/Type.hs @@ -669,7 +669,7 @@ the type checker (e.g. when matching type-function equations). mkAppTy :: Type -> Type -> Type -- See Note [Respecting definitional equality], invariant (EQ1). mkAppTy (CastTy fun_ty co) arg_ty - | ([arg_co], res_co) <- decomposePiCos (typeKind fun_ty) [arg_ty] co + | ([arg_co], res_co) <- decomposePiCos co (coercionKind co) [arg_ty] = (fun_ty `mkAppTy` (arg_ty `mkCastTy` arg_co)) `mkCastTy` res_co mkAppTy (TyConApp tc tys) ty2 = mkTyConApp tc (tys ++ [ty2]) @@ -691,7 +691,7 @@ mkAppTys (CastTy fun_ty co) arg_tys -- much more efficient then nested mkAppTy -- in TyCoRep = foldl AppTy ((mkAppTys fun_ty casted_arg_tys) `mkCastTy` res_co) leftovers where - (arg_cos, res_co) = decomposePiCos (typeKind fun_ty) arg_tys co + (arg_cos, res_co) = decomposePiCos co (coercionKind co) arg_tys (args_to_cast, leftovers) = splitAtList arg_cos arg_tys casted_arg_tys = zipWith mkCastTy args_to_cast arg_cos mkAppTys (TyConApp tc tys1) tys2 = mkTyConApp tc (tys1 ++ tys2) diff --git a/testsuite/tests/dependent/should_fail/T15343.hs b/testsuite/tests/dependent/should_fail/T15343.hs new file mode 100644 index 0000000000..9bb59c807a --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T15343.hs @@ -0,0 +1,14 @@ +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeInType #-} +module T15343 where + +import Data.Kind + +elimSing :: forall (p :: forall z. z). p +elimSing = undefined + +data WhySym :: Type -> Type + +hsym = elimSing @WhySym diff --git a/testsuite/tests/dependent/should_fail/T15343.stderr b/testsuite/tests/dependent/should_fail/T15343.stderr new file mode 100644 index 0000000000..79d81e5772 --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T15343.stderr @@ -0,0 +1,7 @@ + +T15343.hs:14:18: error: + • Expecting one more argument to ‘WhySym’ + Expected kind ‘forall z. z’, but ‘WhySym’ has kind ‘* -> *’ + • In the type ‘WhySym’ + In the expression: elimSing @WhySym + In an equation for ‘hsym’: hsym = elimSing @WhySym diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T index 1bc3f42a92..59d80375ff 100644 --- a/testsuite/tests/dependent/should_fail/all.T +++ b/testsuite/tests/dependent/should_fail/all.T @@ -33,3 +33,5 @@ test('InferDependency', normal, compile_fail, ['']) test('T15245', normal, compile_fail, ['']) test('T15215', normal, compile_fail, ['']) test('T15308', normal, compile_fail, ['-fno-print-explicit-kinds']) +test('T15343', normal, compile_fail, ['']) + |