diff options
| -rw-r--r-- | compiler/typecheck/Inst.hs | 28 | ||||
| -rw-r--r-- | compiler/typecheck/TcPat.hs | 9 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_compile/T14154.hs | 16 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_compile/all.T | 1 |
4 files changed, 51 insertions, 3 deletions
diff --git a/compiler/typecheck/Inst.hs b/compiler/typecheck/Inst.hs index 34e6e71d46..bb2b90c771 100644 --- a/compiler/typecheck/Inst.hs +++ b/compiler/typecheck/Inst.hs @@ -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) + {- ************************************************************************ * * diff --git a/compiler/typecheck/TcPat.hs b/compiler/typecheck/TcPat.hs index 18b148d8b6..6be2a4e965 100644 --- a/compiler/typecheck/TcPat.hs +++ b/compiler/typecheck/TcPat.hs @@ -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 diff --git a/testsuite/tests/typecheck/should_compile/T14154.hs b/testsuite/tests/typecheck/should_compile/T14154.hs new file mode 100644 index 0000000000..e29ee85504 --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T14154.hs @@ -0,0 +1,16 @@ +{-# 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 diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T index 13a2719c96..b929195c16 100644 --- a/testsuite/tests/typecheck/should_compile/all.T +++ b/testsuite/tests/typecheck/should_compile/all.T @@ -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, ['']) |