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

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, [''])