[commit: ghc] master: Better Note [The well-kinded type invariant] (e24da5e)

[git at git.haskell.org]

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

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

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

commit e24da5edb4709bdb050c8d0676f302d0b87b8446
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Wed Jul 11 12:05:20 2018 +0100

    Better Note [The well-kinded type invariant]
    
    c.f. Trac #14873


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

e24da5edb4709bdb050c8d0676f302d0b87b8446
 compiler/typecheck/TcType.hs | 40 ++++++++++++++++++++--------------------
 1 file changed, 20 insertions(+), 20 deletions(-)

diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index 96d4524..83e62e0 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -1402,26 +1402,26 @@ getDFunTyLitKey (StrTyLit n) = mkOccName Name.varName (show n)  -- hm
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 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/.
+During type inference, we maintain this invariant
+
+   (INV-TK): it is legal to call 'typeKind' on any Type ty,
+             /without/ zonking ty
+
+For example, suppose
+    kappa is a unification variable
+    We have already unified kappa := Type
+      yielding    co :: Refl (Type -> Type)
+    a :: kappa
+then consider the type
+    (a Int)
+If we call typeKind on that, we'll crash, because the (un-zonked)
+kind of 'a' is just kappa, not an arrow kind.  If we zonk first
+we'd be fine, but that is too tiresome, so instead we maintain
+(TK-INV).  So we do not form (a Int); instead we form
+    (a |> co) Int
+and typeKind has no problem with that.
+
+Bottom line: 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