Commit 4455c86d authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Use a well-kinded substitution to instantiate

In tcDataConPat we were creating an ill-kinded substitution
-- or at least one that is well kinded only after you have solved
other equalities.  THat led to a crash, because the instantiated
data con type was ill-kinded.

This patch guarantees that the instantiating substitution is
well-kinded.

Fixed Trac #14154
parent 86e6a5f2
......@@ -12,7 +12,7 @@ The @Inst@ type: dictionaries or method instances
module Inst (
deeplySkolemise,
topInstantiate, topInstantiateInferred, deeplyInstantiate,
instCall, instDFunType, instStupidTheta,
instCall, instDFunType, instStupidTheta, instTyVarsWith,
newWanted, newWanteds,
tcInstBinders, tcInstBinder,
......@@ -279,6 +279,32 @@ deeply_instantiate orig subst ty
, text "subst:" <+> ppr subst ])
; return (idHsWrapper, ty') }
instTyVarsWith :: CtOrigin -> [TyVar] -> [TcType] -> TcM TCvSubst
-- Use this when you want to instantiate (forall a b c. ty) with
-- types [ta, tb, tc], but when the kinds of 'a' and 'ta' might
-- not yet match (perhaps because there are unsolved constraints; Trac #14154)
-- If they don't match, emit a kind-equality to promise that they will
-- eventually do so, and thus make a kind-homongeneous substitution.
instTyVarsWith orig tvs tys
= go empty_subst tvs tys
where
empty_subst = mkEmptyTCvSubst (mkInScopeSet (tyCoVarsOfTypes tys))
go subst [] []
= return subst
go subst (tv:tvs) (ty:tys)
| tv_kind `tcEqType` ty_kind
= go (extendTCvSubst subst tv ty) tvs tys
| otherwise
= do { co <- emitWantedEq orig KindLevel Nominal ty_kind tv_kind
; go (extendTCvSubst subst tv (ty `mkCastTy` co)) tvs tys }
where
tv_kind = substTy subst (tyVarKind tv)
ty_kind = typeKind ty
go _ _ _ = pprPanic "instTysWith" (ppr tvs $$ ppr tys)
{-
************************************************************************
* *
......
......@@ -736,8 +736,13 @@ tcDataConPat penv (L con_span con_name) data_con pat_ty arg_pats thing_inside
; let all_arg_tys = eqSpecPreds eq_spec ++ theta ++ arg_tys
; checkExistentials ex_tvs all_arg_tys penv
; (tenv, ex_tvs') <- tcInstSuperSkolTyVarsX
(zipTvSubst univ_tvs ctxt_res_tys) ex_tvs
; tenv <- instTyVarsWith PatOrigin univ_tvs ctxt_res_tys
-- NB: Do not use zipTvSubst! See Trac #14154
-- We want to create a well-kinded substitution, so
-- that the instantiated type is well-kinded
; (tenv, ex_tvs') <- tcInstSuperSkolTyVarsX tenv ex_tvs
-- Get location from monad, not from ex_tvs
; let -- pat_ty' = mkTyConApp tycon ctxt_res_tys
......
{-# Language RankNTypes, DerivingStrategies, TypeApplications,
ScopedTypeVariables, GADTs, PolyKinds #-}
module T14154 where
newtype Ran g h a
= MkRan (forall b. (a -> g b) -> h b)
newtype Swap p f g a where
MkSwap :: p g f a -> Swap p f g a
ireturn :: forall m i a. a -> m i i a
ireturn = undefined
xs = case ireturn @(Swap Ran) 'a' of
MkSwap (MkRan f) -> f print
......@@ -572,3 +572,4 @@ test('T13915a', normal, multimod_compile, ['T13915a', '-v0'])
test('T13915b', normal, compile, [''])
test('T13984', normal, compile, [''])
test('T14149', normal, compile, [''])
test('T14154', normal, compile, [''])
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