[commit: ghc] master: Use a well-kinded substitution to instantiate (4455c86)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/4455c86d1635bfb846e750b21dda36dcee028b5e/ghc

>---------------------------------------------------------------

commit 4455c86d1635bfb846e750b21dda36dcee028b5e
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Mon Aug 28 17:21:14 2017 +0100

    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


>---------------------------------------------------------------

4455c86d1635bfb846e750b21dda36dcee028b5e
 compiler/typecheck/Inst.hs                         | 28 +++++++++++++++++++++-
 compiler/typecheck/TcPat.hs                        |  9 +++++--
 testsuite/tests/typecheck/should_compile/T14154.hs | 16 +++++++++++++
 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 34e6e71..bb2b90c 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 18b148d..6be2a4e 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 0000000..e29ee85
--- /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 13a2719..b929195 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, [''])