Respect Note [The tcType invariant]

I tried to do this with

    commit 0a12d92a8f65d374f9317af2759af2b46267ad5c
    Author: Simon Peyton Jones <simonpj@microsoft.com>
    Date:   Wed Dec 13 12:53:26 2017 +0000

    Further improvements to well-kinded types

    The typechecker has the invariant that every type should be well-kinded
    as it stands, without zonking.  See Note [The well-kinded type invariant]
    in TcType.

    That invariant was not being upheld, which led to Trac #14174.  I fixed
    part of it, but T14174a showed that there was more.  This patch finishes
    the job.

But I didn't get it quite right as Trac #14873 showed.

This patch fixes the problem; although I am still a bit unhappy.
(See "A worry" in the HsApp case of tc_infer_hs_type.)

3 files changed, 95 insertions, 14 deletions

diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index a8b9fe8c93..2b324ca080 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -500,22 +500,31 @@ tc_infer_lhs_type mode (L span ty)
 -- | Infer the kind of a type and desugar. This is the "up" type-checker,
 -- as described in Note [Bidirectional type checking]
 tc_infer_hs_type :: TcTyMode -> HsType GhcRn -> TcM (TcType, TcKind)
+tc_infer_hs_type mode (HsParTy t)          = tc_infer_lhs_type mode t
 tc_infer_hs_type mode (HsTyVar _ (L _ tv)) = tcTyVar mode tv
+
 tc_infer_hs_type mode (HsAppTy ty1 ty2)
-  = do { let (fun_ty, arg_tys) = splitHsAppTys ty1 [ty2]
-       ; (fun_ty', fun_kind) <- tc_infer_lhs_type mode fun_ty
-       ; fun_kind' <- zonkTcType fun_kind
-       ; tcTyApps mode fun_ty fun_ty' fun_kind' arg_tys }
-tc_infer_hs_type mode (HsParTy t)     = tc_infer_lhs_type mode t
-tc_infer_hs_type mode (HsOpTy lhs (L loc_op op) rhs)
-  | not (op `hasKey` funTyConKey)
-  = do { (op', op_kind) <- tcTyVar mode op
-       ; op_kind' <- zonkTcType op_kind
-       ; tcTyApps mode (noLoc $ HsTyVar NotPromoted (L loc_op op)) op' op_kind' [lhs, rhs] }
+  = do { let (hs_fun_ty, hs_arg_tys) = splitHsAppTys ty1 [ty2]
+       ; (fun_ty, fun_kind) <- tc_infer_lhs_type mode hs_fun_ty
+         -- A worry: what if fun_kind needs zoonking?
+         -- We used to zonk it here, but that got fun_ty and fun_kind
+         -- out of sync (see the precondition to tcTyApps), which caused
+         -- Trac #14873.  So I'm now zonking in tcTyVar, and not here.
+         -- Is that enough?  Seems so, but I can't see how to be certain.
+       ; tcTyApps mode hs_fun_ty fun_ty fun_kind hs_arg_tys }
+
+tc_infer_hs_type mode (HsOpTy lhs lhs_op@(L _ hs_op) rhs)
+  | not (hs_op `hasKey` funTyConKey)
+  = do { (op, op_kind) <- tcTyVar mode hs_op
+         -- See "A worry" in the HsApp case
+       ; tcTyApps mode (noLoc $ HsTyVar NotPromoted lhs_op) op op_kind [lhs, rhs] }
+
 tc_infer_hs_type mode (HsKindSig ty sig)
   = do { sig' <- tc_lhs_kind (kindLevel mode) sig
+       ; traceTc "tc_infer_hs_type:sig" (ppr ty $$ ppr sig')
        ; ty' <- tc_lhs_type mode ty sig'
        ; return (ty', sig') }
+
 -- HsSpliced is an annotation produced by 'RnSplice.rnSpliceType' to communicate
 -- the splice location to the typechecker. Here we skip over it in order to have
 -- the same kind inferred for a given expression whether it was produced from
@@ -524,6 +533,7 @@ tc_infer_hs_type mode (HsKindSig ty sig)
 -- See Note [Delaying modFinalizers in untyped splices].
 tc_infer_hs_type mode (HsSpliceTy (HsSpliced _ (HsSplicedTy ty)) _)
   = tc_infer_hs_type mode ty
+
 tc_infer_hs_type mode (HsDocTy ty _) = tc_infer_lhs_type mode ty
 tc_infer_hs_type _    (HsCoreTy ty)  = return (ty, typeKind ty)
 tc_infer_hs_type mode other_ty
@@ -846,6 +856,10 @@ tcInferApps :: TcTyMode
             -> TcKind               -- ^ Function kind (zonked)
             -> [LHsType GhcRn]      -- ^ Args
             -> TcM (TcType, [TcType], TcKind) -- ^ (f args, args, result kind)
+-- Precondition: typeKind fun_ty = fun_ki
+--    Reason: we will return a type application like (fun_ty arg1 ... argn),
+--            and that type must be well-kinded
+--            See Note [The tcType invariant]
 tcInferApps mode mb_kind_info orig_hs_ty fun_ty fun_ki orig_hs_args
   = do { traceTc "tcInferApps {" (ppr orig_hs_ty $$ ppr orig_hs_args $$ ppr fun_ki)
        ; stuff <- go 1 [] empty_subst fun_ty orig_ki_binders orig_inner_ki orig_hs_args
@@ -887,7 +901,8 @@ tcInferApps mode mb_kind_info orig_hs_ty fun_ty fun_ki orig_hs_args
            ; arg' <- addErrCtxt (funAppCtxt orig_hs_ty arg n) $
                      tc_lhs_type mode arg (substTy subst $ tyBinderType ki_binder)
            ; let subst' = extendTvSubstBinderAndInScope subst ki_binder arg'
-           ; go (n+1) (arg' : acc_args) subst' (mkNakedAppTy fun arg')
+           ; go (n+1) (arg' : acc_args) subst'
+                (mkNakedAppTy fun arg')
                 ki_binders inner_ki args }
 
        -- We've run out of known binders in the functions's kind.
@@ -924,8 +939,9 @@ tcTyApps :: TcTyMode
          -> TcKind               -- ^ Function kind (zonked)
          -> [LHsType GhcRn]      -- ^ Args
          -> TcM (TcType, TcKind) -- ^ (f args, result kind)
-tcTyApps mode orig_hs_ty ty ki args
-  = do { (ty', _args, ki') <- tcInferApps mode Nothing orig_hs_ty ty ki args
+-- Precondition: see precondition for tcInferApps
+tcTyApps mode orig_hs_ty fun_ty fun_ki args
+  = do { (ty', _args, ki') <- tcInferApps mode Nothing orig_hs_ty fun_ty fun_ki args
        ; return (ty', ki') }
 
 --------------------------
@@ -965,6 +981,12 @@ checkExpectedKindX mb_kind_env pp_hs_ty ty act_kind exp_kind
                                   , uo_visible  = True } -- the hs_ty is visible
             ty' = mkNakedAppTys ty new_args
 
+      ; traceTc "checkExpectedKind" $
+        vcat [ pp_hs_ty
+             , text "act_kind:" <+> ppr act_kind
+             , text "act_kind':" <+> ppr act_kind'
+             , text "exp_kind:" <+> ppr exp_kind ]
+
       ; if act_kind' `tcEqType` exp_kind
         then return (ty', new_args, mkTcNomReflCo exp_kind)  -- This is very common
         else do { co_k <- uType KindLevel origin act_kind' exp_kind
@@ -1039,7 +1061,16 @@ tcTyVar mode name         -- Could be a tyvar, a tycon, or a datacon
   = do { traceTc "lk1" (ppr name)
        ; thing <- tcLookup name
        ; case thing of
-           ATyVar _ tv -> return (mkTyVarTy tv, tyVarKind tv)
+           ATyVar _ tv -> -- Important: zonk before returning
+                          -- We may have the application ((a::kappa) b)
+                          -- where kappa is already unified to (k1 -> k2)
+                          -- Then we want to see that arrow.  Best done
+                          -- here because we are also maintaining
+                          -- Note [The tcType invariant], so we don't just
+                          -- want to zonk the kind, leaving the TyVar
+                          -- un-zonked  (Trac #114873)
+                          do { ty <- zonkTcTyVar tv
+                             ; return (ty, typeKind ty) }
 
            ATcTyCon tc_tc -> do { -- See Note [GADT kind self-reference]
                                   unless
diff --git a/testsuite/tests/polykinds/T14873.hs b/testsuite/tests/polykinds/T14873.hs
new file mode 100644
index 0000000000..6bb66ec640
--- /dev/null
+++ b/testsuite/tests/polykinds/T14873.hs
@@ -0,0 +1,49 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+module T14873 where
+
+import Data.Kind (Type)
+
+data family Sing (a :: k)
+
+newtype instance Sing (f :: k1 ~> k2) =
+  SLambda { applySing :: forall t. Sing t -> Sing (Apply f t) }
+
+data TyFun :: Type -> Type -> Type
+type a ~> b = TyFun a b -> Type
+infixr 0 ~>
+type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
+
+class SingI (a :: k) where
+  sing :: Sing a
+
+data ColSym1 :: f a -> a ~> Bool
+type instance Apply (ColSym1 x) y = Col x y
+
+class PColumn (f :: Type -> Type) where
+  type Col (x :: f a) (y :: a) :: Bool
+
+class SColumn (f :: Type -> Type) where
+  sCol :: forall (x :: f a) (y :: a).
+    Sing x -> Sing y -> Sing (Col x y :: Bool)
+
+instance (SColumn f, SingI x) => SingI (ColSym1 (x :: f a) :: a ~> Bool) where
+  sing = SLambda (sCol (sing @_ @x))
+
+{-  When the bug was present, this smaller kind-incorrect version also
+    elicited the same piResultTy crash
+
+    But it's kind-incorrect, whereas the main test case should compile file
+
+class SingI (a :: k) where
+
+class SColumn (f :: Type -> Type) where
+
+instance -- forall (f :: Type -> Type) a (x :: f a).
+         SColumn f => SingI (x :: f a)
+-}
+
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 36eb07be07..ac46b2bf30 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -185,4 +185,5 @@ test('T14580', normal, compile_fail, [''])
 test('T14515', normal, compile, [''])
 test('T14723', normal, compile, [''])
 test('T14846', normal, compile_fail, [''])
+test('T14873', normal, compile, [''])