Commit 5b10d537 authored by Simon Peyton Jones's avatar Simon Peyton Jones Committed by Ben Gamari
Browse files

Fix decompsePiCos and visible type application

Trac #15343 was caused by two things

First, in TcHsType.tcHsTypeApp, which deals with the type argment
in visible type application, we were failing to call
solveLocalEqualities. But the type argument is like a user type
signature so it's at least inconsitent not to do so.

I thought that would nail it.  But it didn't. It turned out that we
were ended up calling decomposePiCos on a type looking like this
    (f |> co) Int

where co :: (forall a. ty) ~ (t1 -> t2)

Now, 'co' is insoluble, and we'll report that later.  But meanwhile
we don't want to crash in decomposePiCos.

My fix involves keeping track of the type on both sides of the
coercion, and ensuring that the outer shape matches before
decomposing.  I wish there was a simpler way to do this. But
I think this one is at least robust.

I suppose it is possible that the decomposePiCos fix would
have cured the original report, but I'm leaving the one-line
tcHsTypeApp fix in too because it just seems more consistent.

(cherry picked from commit aedbf7f1)
parent 391ee977
...@@ -1304,10 +1304,16 @@ flatten_args_slow orig_binders orig_inner_ki orig_fvs orig_roles orig_tys ...@@ -1304,10 +1304,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 go acc_xis acc_cos lc [] inner_ki roles tys
| Just k <- tcGetTyVar_maybe inner_ki | Just k <- tcGetTyVar_maybe inner_ki
, Just co1 <- liftCoSubstTyVar lc Nominal k , Just co1 <- liftCoSubstTyVar lc Nominal k
= do { let Pair flattened_kind _ = coercionKind co1 = do { let co1_kind = coercionKind co1
(arg_cos, res_co) = decomposePiCos flattened_kind tys co1 (arg_cos, res_co) = decomposePiCos co1 co1_kind tys
casted_tys = zipWith mkCastTy tys arg_cos 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 zapped_lc = zapLiftingContext lc
Pair flattened_kind _ = co1_kind
(bndrs, new_inner) = splitPiTys flattened_kind (bndrs, new_inner) = splitPiTys flattened_kind
; (xis_out, cos_out, res_co_out) ; (xis_out, cos_out, res_co_out)
......
...@@ -356,7 +356,10 @@ tcHsTypeApp :: LHsWcType GhcRn -> Kind -> TcM Type ...@@ -356,7 +356,10 @@ tcHsTypeApp :: LHsWcType GhcRn -> Kind -> TcM Type
-- See Note [Recipe for checking a signature] in TcHsType -- See Note [Recipe for checking a signature] in TcHsType
tcHsTypeApp wc_ty kind tcHsTypeApp wc_ty kind
| HsWC { hswc_ext = sig_wcs, hswc_body = hs_ty } <- wc_ty | 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 tcCheckLHsType hs_ty kind
; ty <- zonkPromoteType ty ; ty <- zonkPromoteType ty
; checkValidType TypeAppCtxt ty ; checkValidType TypeAppCtxt ty
......
...@@ -271,42 +271,71 @@ decomposeFunCo r co = ASSERT2( all_ok, ppr co ) ...@@ -271,42 +271,71 @@ decomposeFunCo r co = ASSERT2( all_ok, ppr co )
Pair s1t1 s2t2 = coercionKind co Pair s1t1 s2t2 = coercionKind co
all_ok = isFunTy s1t1 && isFunTy s2t2 all_ok = isFunTy s1t1 && isFunTy s2t2
-- | Decompose a function coercion, either a dependent one or a non-dependent one. {- Note [Pushing a coercion into a pi-type]
-- 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 Suppose we have this:
-- to do so, see Note [Respecting definitional equality] in TyCoRep. (f |> co) t1 .. tn
-- This might return *fewer* coercions than there are arguments, if the kind provided Then we want to push the coercion into the arguments, so as to make
-- doesn't have enough binders. progress. For example of why you might want to do so, see Note
-- The types passed in are the ty2 ... tyn. If the results are (arg_cos, res_co), [Respecting definitional equality] in TyCoRep.
-- then you should build
-- @(ty1 (ty2 |> arg_cos1) (ty3 |> arg_cos2) ... (tym |> arg_com)|> res_co) tym+1 ... tyn@. This is done by decomposePiCos. Specifically, if
decomposePiCos :: Kind -- of the function (ty1), used only to tell -> from ∀ from other decomposePiCos co [t1,..,tn] = ([co1,...,cok], cor)
-> [Type] -> CoercionN -> ([CoercionN], CoercionN) then
decomposePiCos orig_kind orig_args orig_co = go [] orig_subst orig_kind orig_args orig_co (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 where
orig_subst = mkEmptyTCvSubst $ mkInScopeSet $ tyCoVarsOfTypes (orig_kind : orig_args) orig_subst = mkEmptyTCvSubst $ mkInScopeSet $
`unionVarSet` tyCoVarsOfCo orig_co tyCoVarsOfTypes orig_args `unionVarSet` tyCoVarsOfCo orig_co
go :: [CoercionN] -- accumulator for argument coercions, reversed go :: [CoercionN] -- accumulator for argument coercions, reversed
-> TCvSubst -- instantiating substitution -> (TCvSubst,Kind) -- Lhs kind of coercion
-> Kind -- of the function being applied (unsubsted) -> CoercionN -- coercion originally applied to the function
-> [Type] -- arguments to that function -> (TCvSubst,Kind) -- Rhs kind of coercion
-> CoercionN -- coercion originally applied to the function -> [Type] -- Arguments to that function
-> ([CoercionN], Coercion) -> ([CoercionN], Coercion)
go acc_arg_cos subst ki (ty:tys) co -- Invariant: co :: subst1(k2) ~ subst2(k2)
| Just (kv, inner_ki) <- splitForAllTy_maybe ki
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) -- know co :: (forall a:s1.t1) ~ (forall b:s2.t2)
-- function :: forall a:s1.t1 (the function is not passed to decomposePiCos) -- function :: forall a:s1.t1 (the function is not passed to decomposePiCos)
-- a :: s1
-- b :: s2
-- ty :: s2 -- ty :: s2
-- need arg_co :: s2 ~ s1 -- need arg_co :: s2 ~ s1
-- res_co :: t1[ty |> arg_co / a] ~ t2[ty / b] -- res_co :: t1[ty |> arg_co / a] ~ t2[ty / b]
= let arg_co = mkNthCo Nominal 0 (mkSymCo co) = let arg_co = mkNthCo Nominal 0 (mkSymCo co)
res_co = mkInstCo co (mkNomReflCo ty `mkCoherenceLeftCo` arg_co) res_co = mkInstCo co (mkNomReflCo ty `mkCoherenceLeftCo` arg_co)
subst' = extendTCvSubst subst kv ty subst1' = extendTCvSubst subst1 a (ty `CastTy` arg_co)
subst2' = extendTCvSubst subst2 b ty
in 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) -- know co :: (s1 -> t1) ~ (s2 -> t2)
-- function :: s1 -> t1 -- function :: s1 -> t1
-- ty :: s2 -- ty :: s2
...@@ -315,19 +344,17 @@ decomposePiCos orig_kind orig_args orig_co = go [] orig_subst orig_kind orig_arg ...@@ -315,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 = let (sym_arg_co, res_co) = decomposeFunCo Nominal co
arg_co = mkSymCo sym_arg_co arg_co = mkSymCo sym_arg_co
in 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 | not (isEmptyTCvSubst subst1) || not (isEmptyTCvSubst subst2)
, isPiTy substed_ki = go acc_arg_cos (zapTCvSubst subst1, substTy subst1 k1)
-- This might happen if we have to substitute in order to see that the kind co
-- is a Π-type. (zapTCvSubst subst2, substTy subst1 k2)
= let subst' = zapTCvSubst subst (ty:tys)
in
go acc_arg_cos subst' substed_ki (ty:tys) co
-- tys might not be empty, if the left-hand type of the original coercion -- tys might not be empty, if the left-hand type of the original coercion
-- didn't have enough binders -- 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' -- | Attempts to obtain the type variable underlying a 'Coercion'
getCoVar_maybe :: Coercion -> Maybe CoVar getCoVar_maybe :: Coercion -> Maybe CoVar
......
...@@ -36,7 +36,7 @@ mkAxiomRuleCo :: CoAxiomRule -> [Coercion] -> Coercion ...@@ -36,7 +36,7 @@ mkAxiomRuleCo :: CoAxiomRule -> [Coercion] -> Coercion
isReflCo :: Coercion -> Bool isReflCo :: Coercion -> Bool
isReflexiveCo :: 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) coVarKindsTypesRole :: HasDebugCallStack => CoVar -> (Kind, Kind, Type, Type, Role)
coVarRole :: CoVar -> Role coVarRole :: CoVar -> Role
......
...@@ -663,7 +663,7 @@ the type checker (e.g. when matching type-function equations). ...@@ -663,7 +663,7 @@ the type checker (e.g. when matching type-function equations).
mkAppTy :: Type -> Type -> Type mkAppTy :: Type -> Type -> Type
-- See Note [Respecting definitional equality], invariant (EQ1). -- See Note [Respecting definitional equality], invariant (EQ1).
mkAppTy (CastTy fun_ty co) arg_ty 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 = (fun_ty `mkAppTy` (arg_ty `mkCastTy` arg_co)) `mkCastTy` res_co
mkAppTy (TyConApp tc tys) ty2 = mkTyConApp tc (tys ++ [ty2]) mkAppTy (TyConApp tc tys) ty2 = mkTyConApp tc (tys ++ [ty2])
...@@ -685,7 +685,7 @@ mkAppTys (CastTy fun_ty co) arg_tys -- much more efficient then nested mkAppTy ...@@ -685,7 +685,7 @@ mkAppTys (CastTy fun_ty co) arg_tys -- much more efficient then nested mkAppTy
-- in TyCoRep -- in TyCoRep
= foldl AppTy ((mkAppTys fun_ty casted_arg_tys) `mkCastTy` res_co) leftovers = foldl AppTy ((mkAppTys fun_ty casted_arg_tys) `mkCastTy` res_co) leftovers
where 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 (args_to_cast, leftovers) = splitAtList arg_cos arg_tys
casted_arg_tys = zipWith mkCastTy args_to_cast arg_cos casted_arg_tys = zipWith mkCastTy args_to_cast arg_cos
mkAppTys (TyConApp tc tys1) tys2 = mkTyConApp tc (tys1 ++ tys2) mkAppTys (TyConApp tc tys1) tys2 = mkTyConApp tc (tys1 ++ tys2)
......
{-# 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
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
...@@ -33,3 +33,5 @@ test('InferDependency', normal, compile_fail, ['']) ...@@ -33,3 +33,5 @@ test('InferDependency', normal, compile_fail, [''])
test('T15245', normal, compile_fail, ['']) test('T15245', normal, compile_fail, [''])
test('T15215', normal, compile_fail, ['']) test('T15215', normal, compile_fail, [''])
test('T15308', normal, compile_fail, ['-fno-print-explicit-kinds']) test('T15308', normal, compile_fail, ['-fno-print-explicit-kinds'])
test('T15343', normal, compile_fail, [''])
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment