Commit 4efdda90 authored by Richard Eisenberg's avatar Richard Eisenberg Committed by Marge Bot

Tiny fixes to comments around flattening.

parent b15a7fb8
Pipeline #11487 passed with stages
in 438 minutes and 6 seconds
......@@ -815,7 +815,7 @@ Because flattening zonks and the returned coercion ("co" above) is also
zonked, it's possible that (co :: xi ~ ty) isn't quite true. So, instead,
we can rely on this fact:
(F1) tcTypeKind(xi) succeeds and returns a fully zonked kind
(F0) co :: xi ~ zonk(ty)
Note that the left-hand type of co is *always* precisely xi. The right-hand
type may or may not be ty, however: if ty has unzonked filled-in metavariables,
......@@ -1535,7 +1535,7 @@ flattenTyVar tv
; return (ty2, co2 `mkTransCo` co1) }
FTRNotFollowed -- Done, but make sure the kind is zonked
-- Note [Flattening] invariant (F1)
-- Note [Flattening] invariant (F0) and (F1)
-> do { tv' <- liftTcS $ updateTyVarKindM zonkTcType tv
; role <- getRole
; let ty' = mkTyVarTy tv'
......@@ -1293,7 +1293,7 @@ The calls to mkAppTyM is the other place we are very careful.
Note [mkAppTyM]
mkAppTyM is trying to guaranteed the Purely Kinded Type Invariant
mkAppTyM is trying to guarantee the Purely Kinded Type Invariant
(PKTI) for its result type (fun arg). There are two ways it can go wrong:
* Nasty case 1: forall types (polykinds/T14174a)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment