Add nakedSubstTy and use it in TcHsType.tcInferApps
authorSimon Peyton Jones <simonpj@microsoft.com>
Mon, 9 Jul 2018 16:29:22 +0000 (17:29 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Tue, 10 Jul 2018 08:28:43 +0000 (09:28 +0100)
This was a tricky one.

During type checking we maintain TcType:
   Note [The well-kinded type invariant]
That is, types are well-kinded /without/ zonking.

But in tcInferApps we were destroying that invariant by calling
substTy, which in turn uses smart constructors, which eliminate
apparently-redundant Refl casts.

This is horribly hard to debug beause they really are Refls and
so it "ought" to be OK to discard them. But it isn't, as the
above Note describes in some detail.

Maybe we should review the invariant?  But for now I just followed
it, tricky thought it is.

This popped up because (for some reason) when I fixed Trac #15343,
that exposed this bug by making test polykinds/T14174a fail (in
Trac #14174 which indeed has the same origin).

So this patch fixes a long standing and very subtle bug.

One interesting point: I defined nakedSubstTy in a few lines by
using the generic mapType stuff.  I note that the "normal"
TyCoRep.substTy does /not/ use mapType.  But perhaps it should:
substTy has lots of $! strict applications in it, and they could
all be eliminated just by useing the StrictIdentity monad.  And
that'd make it much easier to experiment with switching between
strict and lazy versions.

compiler/typecheck/TcHsType.hs
compiler/typecheck/TcType.hs

index 624e920..0063e39 100644 (file)
@@ -546,8 +546,8 @@ then
 without any zonking needed.  The reason for this is that in
 tcInferApps we see (F ty), and we kind-check 'ty' with an
 expected-kind coming from F.  Then, to make the resulting application
-well kinded --- see Note [Ensure well-kinded types] in TcType --- we
-need the kind-checked 'ty' to have exactly the kind that F expects,
+well kinded --- see Note [The well-kinded type invariant] in TcType ---
+we need the kind-checked 'ty' to have exactly the kind that F expects,
 with no funny zonking nonsense in between.
 
 The tcType invariant also applies to checkExpectedKind: if
@@ -938,7 +938,10 @@ tcInferApps mode mb_kind_info orig_hs_ty fun_ty fun_ki orig_hs_args
 
       -- no user-written args left. We're done!
     go _ acc_args subst fun ki_binders inner_ki []
-      = return (fun, reverse acc_args, substTy subst $ mkPiTys ki_binders inner_ki)
+      = return ( fun
+               , reverse acc_args
+               , nakedSubstTy subst $ mkPiTys ki_binders inner_ki)
+                 -- nakedSubstTy: see Note [The well-kinded type invariant]
 
       -- The function's kind has a binder. Is it visible or invisible?
     go n acc_args subst fun (ki_binder:ki_binders) inner_ki
@@ -955,11 +958,16 @@ tcInferApps mode mb_kind_info orig_hs_ty fun_ty fun_ki orig_hs_args
       = do { traceTc "tcInferApps (vis)" (vcat [ ppr ki_binder, ppr arg
                                                , ppr (tyBinderType ki_binder)
                                                , ppr subst ])
+           ; let exp_kind = nakedSubstTy subst $ tyBinderType ki_binder
+                            -- nakedSubstTy: see Note [The well-kinded type invariant]
            ; arg' <- addErrCtxt (funAppCtxt orig_hs_ty arg n) $
-                     tc_lhs_type mode arg (substTy subst $ tyBinderType ki_binder)
+                     tc_lhs_type mode arg exp_kind
+           ; traceTc "tcInferApps (vis 1)" (vcat [ ppr exp_kind
+                                                 , ppr arg'
+                                                 , ppr (typeKind arg') ])
            ; let subst' = extendTvSubstBinderAndInScope subst ki_binder arg'
            ; go (n+1) (arg' : acc_args) subst'
-                (mkNakedAppTy fun arg')
+                (mkNakedAppTy fun arg') -- See Note [The well-kinded type invariant]
                 ki_binders inner_ki args }
 
        -- We've run out of known binders in the functions's kind.
@@ -975,7 +983,7 @@ tcInferApps mode mb_kind_info orig_hs_ty fun_ty fun_ki orig_hs_args
            ; let new_in_scope = tyCoVarsOfTypes [arg_k, res_k]
                  subst'       = zapped_subst `extendTCvInScopeSet` new_in_scope
            ; go n acc_args subst'
-                (fun `mkNakedCastTy` co)
+                (fun `mkNakedCastTy` co)  -- See Note [The well-kinded type invariant]
                 [mkAnonBinder arg_k]
                 res_k all_args }
       where
index 31d759e..96d4524 100644 (file)
@@ -52,7 +52,7 @@ module TcType (
   -- Builders
   mkPhiTy, mkInfSigmaTy, mkSpecSigmaTy, mkSigmaTy,
   mkNakedTyConApp, mkNakedAppTys, mkNakedAppTy,
-  mkNakedCastTy,
+  mkNakedCastTy, nakedSubstTy,
 
   --------------------------------
   -- Splitters
@@ -226,6 +226,7 @@ import ErrUtils( Validity(..), MsgDoc, isValid )
 import qualified GHC.LanguageExtensions as LangExt
 
 import Data.List  ( mapAccumL )
+import Data.Functor.Identity( Identity(..) )
 import Data.IORef
 import Data.List.NonEmpty( NonEmpty(..) )
 import qualified Data.Semigroup as Semi
@@ -1391,6 +1392,69 @@ getDFunTyLitKey :: TyLit -> OccName
 getDFunTyLitKey (NumTyLit n) = mkOccName Name.varName (show n)
 getDFunTyLitKey (StrTyLit n) = mkOccName Name.varName (show n)  -- hm
 
+{- *********************************************************************
+*                                                                      *
+           Maintaining the well-kinded type invariant
+*                                                                      *
+********************************************************************* -}
+
+{- Note [The well-kinded type invariant]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+See also Note [The tcType invariant] in TcHsType.
+
+During type inference, we maintain the invariant that
+
+   INVARIANT: every type is well-kinded /without/ zonking
+
+   EXCEPT: you are allowed (ty |> co) even if the kind of ty
+           does not match the from-kind of co.
+
+Main goal: if this invariant is respected, then typeKind cannot fail
+(as it can for ill-kinded types).
+
+In particular, we can get types like
+     (k |> co) Int
+where
+    k :: kappa
+    co :: Refl (Type -> Type)
+    kappa is a unification variable and kappa := Type already
+
+So in the un-zonked form (k Int) would be ill-kinded,
+but (k |> co) Int is well-kinded.  So we want to keep that 'co'
+/even though it is Refl/.
+
+Immediate consequence: during type inference we cannot use the "smart
+contructors" for types, particularly
+   mkAppTy, mkCastTy
+because they all eliminate Refl casts.  Solution: during type
+inference use the mkNakedX type formers, which do no Refl-elimination.
+E.g. mkNakedCastTy uses an actual CastTy, without optimising for
+Refl.  (NB: mkNakedCastTy is only called in two places: in tcInferApps
+and in checkExpectedResultKind.)
+
+Where does this show up in practice: apparently mainly in
+TcHsType.tcInferApps.  Suppose we are kind-checking the type (a Int),
+where (a :: kappa).  Then in tcInferApps we'll run out of binders on
+a's kind, so we'll call matchExpectedFunKind, and unify
+   kappa := kappa1 -> kappa2,  with evidence co :: kappa ~ (kappa1 ~ kappa2)
+That evidence is actually Refl, but we must not discard the cast to
+form the result type
+   ((a::kappa) (Int::*))
+bacause that does not satisfy the invariant, and crashes TypeKind.  This
+caused Trac #14174 and #14520.
+
+Notes:
+
+* The Refls will be removed later, when we zonk the type.
+
+* This /also/ applies to substitution.  We must use nakedSubstTy,
+  not substTy, bucause the latter uses smart constructors that do
+  Refl-elimination.
+
+* None of this is to do with knot-tying, which is the (quite distinct)
+  motivation for mkNakedTyConApp
+-}
+
 ---------------
 mkNakedTyConApp :: TyCon -> [Type] -> Type
 -- Builds a TyConApp
@@ -1421,33 +1485,21 @@ mkNakedCastTy :: Type -> Coercion -> Type
 -- In fact the calls to mkNakedCastTy ar pretty few and far between.
 mkNakedCastTy ty co = CastTy ty co
 
-{- Note [The well-kinded type invariant]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-During type inference, we maintain the invariant that
-
-   INVARIANT: every type is well-kinded /without/ zonking
-
-and in particular that typeKind does not fail (as it can for
-ill-kinded types).
-
-Now suppose we are kind-checking the type (a Int), where (a :: kappa).
-Then in tcInferApps we'll run out of binders on a's kind, so
-we'll call matchExpectedFunKind, and unify
-   kappa := kappa1 -> kappa2,  with evidence co :: kappa ~ (kappa1 ~ kappa2)
-That evidence is actually Refl, but we must not discard the cast to
-form the result type
-   ((a::kappa) (Int::*))
-bacause that does not satisfy the invariant, and crashes TypeKind.  This
-caused Trac #14174 and #14520.
-
-Solution: make mkNakedCastTy use an actual CastTy, without optimising
-for Refl. Now everything is well-kinded.  The CastTy will be removed
-later, when we zonk.  Still, it's distressingly delicate.
-
-NB: mkNakedCastTy is only called in two places:
-    in tcInferApps and in checkExpectedResultKind.
-    See Note [The tcType invariant] in TcHsType.
--}
+nakedSubstTy :: HasCallStack => TCvSubst -> TcType  -> TcType
+nakedSubstTy subst ty
+  | isEmptyTCvSubst subst = ty
+  | otherwise             = runIdentity                   $
+                            checkValidSubst subst [ty] [] $
+                            mapType nakedSubstMapper subst ty
+  -- Interesting idea: use StrictIdentity to avoid space leaks
+
+nakedSubstMapper :: TyCoMapper TCvSubst Identity
+nakedSubstMapper
+  = TyCoMapper { tcm_smart    = False
+               , tcm_tyvar    = \subst tv -> return (substTyVar subst tv)
+               , tcm_covar    = \subst cv -> return (substCoVar subst cv)
+               , tcm_hole     = \_ hole   -> return (HoleCo hole)
+               , tcm_tybinder = \subst tv _ -> return (substTyVarBndr subst tv) }
 
 {-
 ************************************************************************