[commit: ghc] master: Really fix Trac #14158 (2c133b6)

[git at git.haskell.org]

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

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/2c133b67df374c73bc8069cefd7d57e1d2a14fc3/ghc

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

commit 2c133b67df374c73bc8069cefd7d57e1d2a14fc3
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Wed Aug 30 16:19:37 2017 +0100

    Really fix Trac #14158
    
    I dug more into how #14158 started working. I temporarily reverted the
    patch that "fixed" it, namely
    
        commit a6c448b403dbe8720178ca82100f34baedb1f47e
        Author: Simon Peyton Jones <simonpj at microsoft.com>
        Date:   Mon Aug 28 17:33:59 2017 +0100
    
        Small refactor of getRuntimeRep
    
    Sure enough, there was a real bug, described in the new
    TcExpr Note [Visible type application zonk]
    
    In general, syntactic substituion should be kind-preserving!
    Maybe we should check that invariant...


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

2c133b67df374c73bc8069cefd7d57e1d2a14fc3
 compiler/typecheck/TcExpr.hs                       | 44 +++++++++++++++++++++-
 testsuite/tests/typecheck/should_compile/T14158.hs |  7 ++++
 testsuite/tests/typecheck/should_compile/all.T     |  1 +
 3 files changed, 50 insertions(+), 2 deletions(-)

diff --git a/compiler/typecheck/TcExpr.hs b/compiler/typecheck/TcExpr.hs
index ec03f37..0ff7d1e 100644
--- a/compiler/typecheck/TcExpr.hs
+++ b/compiler/typecheck/TcExpr.hs
@@ -65,7 +65,7 @@ import PrelNames
 import DynFlags
 import SrcLoc
 import Util
-import VarEnv  ( emptyTidyEnv )
+import VarEnv  ( emptyTidyEnv, mkInScopeSet )
 import ListSetOps
 import Maybes
 import Outputable
@@ -1294,7 +1294,18 @@ tcArgs fun orig_fun_ty fun_orig orig_args herald
                                 , ppr inner_ty, pprTyVar tv
                                 , ppr vis ]) )
                     ; ty_arg <- tcHsTypeApp hs_ty_arg kind
-                    ; let insted_ty = substTyWithUnchecked [tv] [ty_arg] inner_ty
+
+                    ; inner_ty <- zonkTcType inner_ty
+                          -- See Note [Visible type application zonk]
+
+                    ; let in_scope  = mkInScopeSet (tyCoVarsOfTypes [upsilon_ty, ty_arg])
+                          insted_ty = substTyWithInScope in_scope [tv] [ty_arg] inner_ty
+                                      -- NB: tv and ty_arg have the same kind, so this
+                                      --     substitution is kind-respecting
+                    ; traceTc "VTA" (vcat [ppr tv, debugPprType kind
+                                          , debugPprType ty_arg
+                                          , debugPprType (typeKind ty_arg)
+                                          , debugPprType insted_ty ])
                     ; (inner_wrap, args', res_ty)
                         <- go acc_args (n+1) insted_ty args
                    -- inner_wrap :: insted_ty "->" (map typeOf args') -> res_ty
@@ -1326,6 +1337,35 @@ tcArgs fun orig_fun_ty fun_orig orig_args herald
                text "Cannot apply expression of type" <+> quotes (ppr ty) $$
                text "to a visible type argument" <+> quotes (ppr arg) }
 
+{- Note [Visible type application zonk]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+* Substitutions should be kind-preserving, so we need kind(tv) = kind(ty_arg).
+
+* tcHsTypeApp only guarantees that
+    - ty_arg is zonked
+    - kind(zonk(tv)) = kind(ty_arg)
+  (checkExpectedKind zonks as it goes).
+
+So we must zonk inner_ty as well, to guarantee consistency between zonk(tv)
+and inner_ty.  Otherwise we can build an ill-kinded type.  An example was
+Trac #14158, where we had:
+   id :: forall k. forall (cat :: k -> k -> *). forall (a :: k). cat a a
+and we had the visible type application
+  id @(->)
+
+* We instantiated k := kappa, yielding
+    forall (cat :: kappa -> kappa -> *). forall (a :: kappa). cat a a
+* Then we called tcHsTypeApp (->) with expected kind (kappa -> kappa -> *).
+* That instantiated (->) as ((->) q1 q1), and unified kappa := q1,
+  Here q1 :: RuntimeRep
+* Now we substitute
+     cat  :->  (->) q1 q1 :: TYPE q1 -> TYPE q1 -> *
+  but we must first zonk the inner_ty to get
+      forall (a :: TYPE q1). cat a a
+  so that the result of substitution is well-kinded
+  Failing to do so led to Trac #14158.
+-}
+
 ----------------
 tcArg :: LHsExpr GhcRn                   -- The function (for error messages)
       -> LHsExpr GhcRn                   -- Actual arguments
diff --git a/testsuite/tests/typecheck/should_compile/T14158.hs b/testsuite/tests/typecheck/should_compile/T14158.hs
new file mode 100644
index 0000000..88bb82e
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T14158.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE TypeApplications #-}
+
+module T14158 where
+
+import qualified Control.Category as Cat
+
+foo = (Cat.id @(->) >>=)
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index fde7bae..bcd6a43 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -574,3 +574,4 @@ test('T13984', normal, compile, [''])
 test('T14128', normal, multimod_compile, ['T14128Main', '-v0'])
 test('T14149', normal, compile, [''])
 test('T14154', normal, compile, [''])
+test('T14158', normal, compile, [''])