Really fix Trac #14158
authorSimon Peyton Jones <simonpj@microsoft.com>
Wed, 30 Aug 2017 15:19:37 +0000 (16:19 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Thu, 31 Aug 2017 07:16:58 +0000 (08:16 +0100)
I dug more into how #14158 started working. I temporarily reverted the
patch that "fixed" it, namely

    commit a6c448b403dbe8720178ca82100f34baedb1f47e
    Author: Simon Peyton Jones <simonpj@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...

compiler/typecheck/TcExpr.hs
testsuite/tests/typecheck/should_compile/T14158.hs [new file with mode: 0644]
testsuite/tests/typecheck/should_compile/all.T

index ec03f37..0ff7d1e 100644 (file)
@@ -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 (file)
index 0000000..88bb82e
--- /dev/null
@@ -0,0 +1,7 @@
+{-# LANGUAGE TypeApplications #-}
+
+module T14158 where
+
+import qualified Control.Category as Cat
+
+foo = (Cat.id @(->) >>=)
index fde7bae..bcd6a43 100644 (file)
@@ -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, [''])