diff options
author | Simon Peyton Jones <simonpj@microsoft.com> | 2018-07-11 12:05:20 +0100 |
---|---|---|
committer | Simon Peyton Jones <simonpj@microsoft.com> | 2018-07-11 12:05:20 +0100 |
commit | e24da5edb4709bdb050c8d0676f302d0b87b8446 (patch) | |
tree | 823cddb94170ab2e7285d0e0aa43037941cb68dd /compiler/typecheck/TcType.hs | |
parent | 81d8b1792d01e0645468e35e23e758dd9c7a6349 (diff) | |
download | haskell-e24da5edb4709bdb050c8d0676f302d0b87b8446.tar.gz |
Better Note [The well-kinded type invariant]
c.f. Trac #14873
Diffstat (limited to 'compiler/typecheck/TcType.hs')
-rw-r--r-- | compiler/typecheck/TcType.hs | 40 |
1 files changed, 20 insertions, 20 deletions
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs index 96d4524ef6..83e62e0890 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 |