[GHC] #15952: Reduce zonking-related invariants in the type checker
#15952: Reduce zonking-related invariants in the type checker -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: task | Status: new Priority: normal | Milestone: 8.6.3 Component: Compiler | Version: 8.6.2 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- The type checker currently maintains two invariants, documented in `Note [The well-kinded type invariant]` in TcType and `Note [The tcType invariant]` in TcHsType. These are a pain to maintain, and Simon and I cooked up a plan not to. Step 1. The tcType invariant is all about `tcInferApps`, at least according to the Note. Previously, we couldn't zonk in `tcInferApps`, because types were knot-tied. But now we can! So, `tcInferApps` could take the type only (not its kind), zonk it, then get the type's (zonked) kind. This might also mean that `tc_infer_hs_type` no longer needs to return a type/kind pair, but could just return a type. After this is done, we can likely remove all the zonks that are in service to the tcType invariant, findable by a search. Step 2. The well-kinded type invariant is also about the need to zonk sometimes. But, instead, we could just always zonk on-the-fly. That is, we introduce new functions like `tcTypeKind` and `tcSubstTy` that zonk as they go. To make sure we're calling the right function at the right time, we introduce `newtype TcType = TcType { unTcType :: Type }`. Then, we're forced to call monadic functions on `TcType`s. This will likely lead to code duplication between `Type` and `TcType`, but we might be able to banish `zonkTcType` (and its many friends) entirely. Also gone would be the `naked` functions, which are all about maintaining the well-kinded type invariant. This step would, as a side effect, fix #15799 and #15918, which is about treating `TcType`s differently from `Type`s. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15952> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15952: Reduce zonking-related invariants in the type checker -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: task | Status: new Priority: normal | Milestone: 8.6.3 Component: Compiler | Version: 8.6.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I propose dividing Step 2 into two. * '''Step 2a''': make `tcTypeKind` monadic, and get rid of the `naked` functions. This will fix #15799 and #15918. * '''Step 2b''': make `substTy` monadic too. After Step 2a, we still have * Invariant `(ForallInv)`: in a 'forall' type `forall a. blah`, all occurrences of `a` should still be visible in `blah` without zonking. So we don't need to make `substTy` monadic in Step 2a. Personally I think that Step 2b might not be worth the bother. Maintaining `(ForallInv)` is really not hard, whereas maintaining `Note [The well-kinded type invariant]` is extremely tricky. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15952#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15952: Reduce zonking-related invariants in the type checker -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: task | Status: new Priority: normal | Milestone: 8.6.3 Component: Compiler | Version: 8.6.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): When we execute Step 2a, there are two differences between `typeKind` and `tcTypeKind`: 1. `tcTypeKind` respects the distinction between `Constraint` and `Type`. Concretely, this means that `typeKind` uses `coreView` and `tcTypeKind` uses `tcView`; and the treatment of `FunTy` differs too. 2. `tcTypeKind` is monadic. This key change lets us remove some `zonkTcType`s, and all the `naked` business. These are separate issues. In `TcErrors`, for example, the types are all zonked, so (2) is not important; and yet making things monadic is a pain. So here's an idea: * '''Make `typeKind` respect the `Constraint`/`Type` distinction.''' So `typeKind (Eq Int)` would return `Constraint` rather than `Type`. But that doesn't matter! In Core-land, those two types are treated identically, so it doesn't matter if `typeKind` returns one vs the other! Then in `TcErrors` we can safely call the (pure) `typeKind`. --------------- To make `tcTypeKind` monadic we need a monadic version of `tcEqType`, because `tcEqType` calls `tcTypeKind` to compare the kinds of the two types. That may in any case be advantageous, because a monadic `tcEqType` will return True more often. We probably want to keep the pure version for occasions where we know the types are zonked. --------------- A couple of notes about `tcEqType`: * `tcEqType` currently returns `Maye Bool` to indicate that, when the types differ, whether they differ only in an invisible position. This is used just once, in `TcErrors`. Rather than return `Maybe Bool`, whith its assocaited allocation etc, I suggest we pass in a `Bool` flag saying whether to take invisible args into account. Then in `TcErrors` we can call `tcEqType` twice (with the flag set to True and False) and behave appropriately. This is only needed for the pure version (used in `TcErrors`). The monadic version ignores this visiblity stuff. * `tc_eq_type` currently takes a "view" function which is always `tcView`. Let's specialise to `tcView`. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15952#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15952: Reduce zonking-related invariants in the type checker -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: task | Status: new Priority: normal | Milestone: 8.6.3 Component: Compiler | Version: 8.6.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Old description:
The type checker currently maintains two invariants, documented in `Note [The well-kinded type invariant]` in TcType and `Note [The tcType invariant]` in TcHsType. These are a pain to maintain, and Simon and I cooked up a plan not to.
Step 1. The tcType invariant is all about `tcInferApps`, at least according to the Note. Previously, we couldn't zonk in `tcInferApps`, because types were knot-tied. But now we can! So, `tcInferApps` could take the type only (not its kind), zonk it, then get the type's (zonked) kind. This might also mean that `tc_infer_hs_type` no longer needs to return a type/kind pair, but could just return a type.
After this is done, we can likely remove all the zonks that are in service to the tcType invariant, findable by a search.
Step 2. The well-kinded type invariant is also about the need to zonk sometimes. But, instead, we could just always zonk on-the-fly. That is, we introduce new functions like `tcTypeKind` and `tcSubstTy` that zonk as they go. To make sure we're calling the right function at the right time, we introduce `newtype TcType = TcType { unTcType :: Type }`. Then, we're forced to call monadic functions on `TcType`s. This will likely lead to code duplication between `Type` and `TcType`, but we might be able to banish `zonkTcType` (and its many friends) entirely. Also gone would be the `naked` functions, which are all about maintaining the well-kinded type invariant. This step would, as a side effect, fix #15799 and #15918, which is about treating `TcType`s differently from `Type`s.
New description: The type checker currently maintains two invariants, documented in `Note [The well-kinded type invariant]` in TcType and `Note [The tcType invariant]` in TcHsType. These are a pain to maintain, and Simon and I cooked up a plan not to. Step 1. The tcType invariant is all about `tcInferApps`, at least according to the Note. Previously, we couldn't zonk in `tcInferApps`, because types were knot-tied. But now we can! So, `tcInferApps` could take the type only (not its kind), zonk it, then get the type's (zonked) kind. This might also mean that `tc_infer_hs_type` no longer needs to return a type/kind pair, but could just return a type. After this is done, we can likely remove all the zonks that are in service to the tcType invariant, findable by a search. Step 2. The well-kinded type invariant is also about the need to zonk sometimes. But, instead, we could just always zonk on-the-fly. That is, we introduce new functions like `tcTypeKind` and `tcSubstTy` that zonk as they go. To make sure we're calling the right function at the right time, we introduce `newtype TcType = TcType { unTcType :: Type }`. Then, we're forced to call monadic functions on `TcType`s. This will likely lead to code duplication between `Type` and `TcType`, but we might be able to banish `zonkTcType` (and its many friends) entirely. Also gone would be the `naked` functions, which are all about maintaining the well-kinded type invariant. This step would, as a side effect, fix #15799 and #15918, which is about treating `TcType`s differently from `Type`s. '''Work in progress on `wip/T15952`''' -- Comment (by simonpj): Commits on `wip/T15952`: {{{ commit b169960c5ed45a7b6fa35d2dbcb66f44128f6a38 Author: Simon Peyton Jones <simonpj@microsoft.com> Date: Wed Dec 5 08:43:59 2018 +0000 Start on Trac #15952 Actually it's working pretty well. Just one error message regression in typecheck/should_fail/T15629. }}} and {{{ commit 79d031326d614f6ca637b67a11949dab64afe728 Author: Simon Peyton Jones <simonpj@microsoft.com> Date: Wed Dec 5 12:25:14 2018 +0000 Remove TcKind result for tc_infer_hs_type More cleaning up All works except a couple or piResultTys crashes in polykinds/T11399 polykinds/T14174a due to using substTy (rather than nakedSubstTy) in piResultTys }}} and {{{ commit a99a43bbb7a8a506f31307591b3ee8e9ba3c4c6f Author: Simon Peyton Jones <simonpj@microsoft.com> Date: Thu Dec 6 09:24:44 2018 +0000 Make tcTypeKind monadic This patch is work in progress on Trac #15952. IT DOES NOT COMPILE. The main payload is progress towards making tcTypeKind monadic. However I have not yet made a monadic version of tcEqType, nor changed all those tcEqType calls to a monadic context. Hence, it won't compile as-is. I'm just parking the work I've done, on a branch, until I've had a chance to agree the path with Richard. (The previous patches on this branch /do/ compile and almost-completely validate.) }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15952#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15952: Reduce zonking-related invariants in the type checker -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: task | Status: new Priority: normal | Milestone: 8.6.3 Component: Compiler | Version: 8.6.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I agree we may not need `substTy` to be monadic. But if we don't make it monadic, it should panic if it ever spots a `TcTyVar`. The problem with making `typeKind` respect the `Type`/`Constraint` distinction is that it means everyone pays the price. Specifically, `typeKind (FunTy {}) = liftedTypeKind` is just fine right now, but if we want to get `typeKind` correct w.r.t. `Constraint`, then this case will have to recur (because of quantified constraints). I agree that doing this wouldn't cause misbehavior, but it would potentially slow, e.g., core passes down.
We probably want to keep the pure version for occasions where we know the types are zonked.
True, but only for syntactic convenience, right? The monadic version should be no less efficient than the pure one, if there are no metavars, I would think. I agree about the idea about the visibility stuff. It might be worthwhile, for performance reasons, to make the decision about visibility once, at the top of `tcEqType`, and then have two mostly-identical recursive functions, one which accounts for visibility and one that doesn't. The alternative is to consult the flag many times during the recursive processing, which seems wasteful. If `tc_eq_type` really is only ever called with `tcView`, then yes, specialize. Does that get you unblocked? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15952#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15952: Reduce zonking-related invariants in the type checker -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): A call this week clarified a few things: A. The second commit in comment:3 exposed an underlying bug. That is, we sometimes call `typeKind` in the type checker. This calls `piResultTys`. But `piResultTys` calls `substTy`, when really we need `nakedSubstTy`. We ''could'' make `tc` equivalents for all these to fix the problem. But better is just to go ahead with the plan in this ticket, which also fixes the problem. B. I've expressed worry about `substTy` encountering a `TcTyVar`. But we realized what's really going on: every substitution (in the type-checker) morally has a `TcLevel`. Substituting variables ''at or above'' that level is highly bogus. But substituting variables ''below'' that level is fine -- they're effectively rigid anyway. In practice, this means that we can instantiate polytypes that still mention meta-type-variables, ''as long as the levels are below the level of the substitution''. Should we actually track and check this? Probably not. But it's good to understand what's going on. This should be put in a Note. C. It's unclear what the advantages/disadvantages are of removing the second return value from `tc_infer_hs_type`. In the last, fallthrough case of that function, it might be quite a lot easier to return the kind rather than reconstruct it. I conjecture that this is purely a performance issue, not at all a correctness issue. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15952#comment:6> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15952: Reduce zonking-related invariants in the type checker -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I have made some progress here, all on `wip/T15952`. A big goal is to sweep away two tricky invariants: * `Note [The well-kinded type invariant]` in `TcType`, which asked that `tcTypeKind` would work even before zonking. But that led to the horrible need to maintain even Refl casts, because we might have `((a::kappa) (b::Type))` where `kappa` is a unification variable that has already been unified `kappa := Type -> Type`. This is only well-kinded if we can see through that unification variable. So previously we used `mkNakedCastTy` to add a stupid Refl cast. `((a::kappa) |> (Refl (Type->Type)) (b::Type)`. Not only is this unsavory, but it's also very fragile: many functions (e.g. substitution) eliminate that Refl cast. * `Note [The tcType invariant]` in `TcHsType`. This was closely related, and was a delicate invariant about the result kind of `tc_hs_type`. It forced a bunch of invariants on related functions. The good news is that I was able to completely dispense with both invariants. I've introduced * `Type.tcTypeKind :: TcType -> TcKind`. This is non-monadic, but respects the distinction between `Type` and `Constraint`. * `TcMType.tcTypeKindM :: TcType -> TcM TcKind`. This one is monadic, and looks through unification variables. You can call the former on any zonked `TcType`; but if the type may be well-kinded only after zonking, you must use the latter. It's always safe to use `tcTypeKindM`, but there are some times when it is clearly safe to call `tcTypeKind`, and very convenient do to so without resorting to the monad, such as in `TcErrors`. Sadly, it's not clear at every call site which is the right one. A number of other functions had to become monadic too * `tcEqTypeM` (because it calls `tcTypeKindM`) * `piResultTysM` (needed by `tcTypeKindM`) * `splitPiTyInvisibleM` * `invisibleTyBndrCountM` * `tcTupKindSortM` * `tcIsConstraintKindM` * `isPredTyM` All these functions appear together in `TcMType`. All the mkNakedX functions go away, which is great. This is all good, but I'm still unhappy. * There are many calls to `isPredTy`, just to distinguish `->` from `=>`. And we need `isPredTyM` now. I think we should just add an `ArgFlag` to `FunTy`. * These changes did not solve #15918 as we thought it would. The cause of #15918 is that `mkCastTy` calls `isReflexiveCo`, which does not respect the distinction between `Type` and `Constraint`. The reason `mkCastTy` calls the blunderbuss `isReflexiveCo` is described in `Note [Respecting definitional equality]` in `TyCoRep`. So do we need a `mkTcCastTy`, wich ''does'' respect the `Type`/`Constraint` distinction? And thence `mkTcAppTy` (since `mkAppTy` calls `mkCastTy`), and `tcSubstTy` as well? This smells like bringing all the `mkNakedX` functions back! I rather wonder if, rather than having the complicated invariants described in `Note [Respecting definitional equality]` we might instead just make the `splitX` functions able to deal with casts? Oddly, #15799 works in HEAD, and in this new branch; so the new stuff can't claim to have fixed it. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15952#comment:7> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15952: Reduce zonking-related invariants in the type checker -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I have not reviewed the code, but just responding to comment:7. I agree about adding `ArgFlag` to `FunTy`, but not the way you probably want. I see `FunTy` as an abbreviation of `ForAllTy`, where the argument is relevant (preserved at runtime) and non-dependent (cannot appear in the rest of the type). Morally (in my opinion), we should have `ForAllTy` store a `TyCoBinder`, which stores either a `Named TyCoVarBinder` or an `Anon Type`. The `TyCoVarBinder` is a pair containing a `TyVar` and an `ArgFlag`. This `ForAllTy` should be called `PiTy`. It was implemented en route to the TypeInType patch but then `FunTy` was re-extracted from it for performance reasons. "Adding `ArgFlag` to `FunTy`" really means that the primordial `PiTy` now stores either a `Named (ArgFlag, TyVar)` or an `Anon (ArgFlag, Type)`. (I've rewritted `TyCoVarBinder` as `(ArgFlag, TyVar)` to simplify the presentation... and to ignore coercion variables, which can indeed safely be ignore in these parts.) But looking at this definition, we see an "obvious" refactor: store a `(NamedFlag, ArgFlag, TyVar)` where `NamedFlag` is a `Bool` cognate that says whether or not the quantifier is dependent. In the end, though, this information is needed only for performance reasons, as we can always treat quantifiers as dependent, but some usage sites won't take advantage of this capability. So that leaves us with `(ArgFlag, TyVar)` as the payload of the binder part of a `PiTy` (along with the "body" part, containing a `Type`). In other words: {{{#!hs data Type = ... | PiTy (ArgFlag, TyVar) Type | ... }}} Now, consider this code that we might try to compile: {{{#!hs data Dict :: Constraint -> Type where MkDict :: c => Dict c foo :: forall (x :: Proxy (MkDict :: Dict c)). Proxy x -> () }}} What's the representation of the type of `foo`? It should be something like {{{#!hs foo :: PiTy (Specified, c :: Constraint) $ PiTy (Inferred, ct :: c) $ PiTy (Specified, x :: Proxy (Dict c) (MkDict c ct)) $ PiTy (Required, _ :: Proxy (Proxy (Dict c) (MkDict c ct)) x) $ unitTy }}} Now we have a usage site of `foo`. We instantiate this type. But, critically, '''how do we instantiate `ct`'''? Do we (a) emit an wanted constraint `c`, or (b) create a fresh unification variable `alpha` and then unify it with the right part of the type of the passed argument to `foo`? This choice matters -- it's conceivable that the solver in strategy (a) will find a different solution for `ct` than unification would come up with (in a situation with incoherency -- which normally does not imperil the type system). The bottom line here is that we need to indicate, for implicit arguments, precisely how GHC should try to infer them when they are omitted. Note that Agda does this: unification is indicated by single braces and solving is indicated by double braces. Currently, `ArgFlag` says when an argument is implicit. In the future, though, I think it will additionally need to specify an instantiation strategy for implicit arguments. To wit, we might have {{{#!hs data InstStrategy = Solve | Unify data ArgFlag = Inferred InstStrategy | Specified InstStrategy | Required }}} or possibly {{{#!hs data InstStrategy = Solve | Unify data VisibleInstAllowed = CanBeVisible | CannotBeVisible data ArgFlag = Invisible InstStrategy VisibleInstAllowed | Visible }}} Zooming back to the present: should we add `ArgFlag` to `FunTy`? I say: "no", because the current `ArgFlag` doesn't scale to the situation described above. Instead -- if we don't want to buy into the more elaborate scheme above -- we should make a new {{{#!hs data NonDepArgFlag -- rename me = SolvedFor | Visible -- I wish I could just reuse Required but no TDNR }}} and then add that to `FunTy`. This approach then naturally scales up to the more elaborate scheme described above. It also has the added bonus of not using the three-way `ArgFlag` to describe a situation which currently only has 2 possibilities. ------------------------------------- Frustrating about #15918. But I agree with your analysis here. As long as we have two different equality relations (the one where `Type ~ Constraint` and the one where it doesn't), this problem will persist. And I think trying to cheat by avoiding writing all these extra functions will fail. As to the idea of simplifying `mkCastTy` in favor of complicating `tcSplitXXX`, I think that might work fine... but I don't think it will save sweat or tears. We would need to have `tc` variants of all the splitting functions instead of all the making functions. And the problems we'll run into will be the same. I favor doing the work at construction, because I conjecture that we construct less often than we split, and it will make inspecting dumps easier (because we'll know that things that look different really are different). And I don't think that having, e.g., `mkTcCastTy` is as bad as the nakedness business. The naked casts were a nasty, fragile hack, using `Refl` in a way it was never intended. `mkTcCastTy`, on the other hand, is a perfectly sensible operation to build a type in a way so that types we consider equal have identical representations. The downside to the new approach is that it requires more code duplication, etc., than the naked- casts trick. -------------------------- About #15799: That bug requires #12045 to witness, though the underlying fault exists in HEAD. I never drilled down to figure out how #12045 triggers it. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15952#comment:8> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15952: Reduce zonking-related invariants in the type checker -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by simonpj: Old description:
The type checker currently maintains two invariants, documented in `Note [The well-kinded type invariant]` in TcType and `Note [The tcType invariant]` in TcHsType. These are a pain to maintain, and Simon and I cooked up a plan not to.
Step 1. The tcType invariant is all about `tcInferApps`, at least according to the Note. Previously, we couldn't zonk in `tcInferApps`, because types were knot-tied. But now we can! So, `tcInferApps` could take the type only (not its kind), zonk it, then get the type's (zonked) kind. This might also mean that `tc_infer_hs_type` no longer needs to return a type/kind pair, but could just return a type.
After this is done, we can likely remove all the zonks that are in service to the tcType invariant, findable by a search.
Step 2. The well-kinded type invariant is also about the need to zonk sometimes. But, instead, we could just always zonk on-the-fly. That is, we introduce new functions like `tcTypeKind` and `tcSubstTy` that zonk as they go. To make sure we're calling the right function at the right time, we introduce `newtype TcType = TcType { unTcType :: Type }`. Then, we're forced to call monadic functions on `TcType`s. This will likely lead to code duplication between `Type` and `TcType`, but we might be able to banish `zonkTcType` (and its many friends) entirely. Also gone would be the `naked` functions, which are all about maintaining the well-kinded type invariant. This step would, as a side effect, fix #15799 and #15918, which is about treating `TcType`s differently from `Type`s.
'''Work in progress on `wip/T15952`'''
New description: The type checker currently maintains two invariants, documented in `Note [The well-kinded type invariant]` in TcType and `Note [The tcType invariant]` in TcHsType. These are a pain to maintain, and Simon and I cooked up a plan not to. Step 1. The tcType invariant is all about `tcInferApps`, at least according to the Note. Previously, we couldn't zonk in `tcInferApps`, because types were knot-tied. But now we can! So, `tcInferApps` could take the type only (not its kind), zonk it, then get the type's (zonked) kind. This might also mean that `tc_infer_hs_type` no longer needs to return a type/kind pair, but could just return a type. After this is done, we can likely remove all the zonks that are in service to the tcType invariant, findable by a search. Step 2. The well-kinded type invariant is also about the need to zonk sometimes. But, instead, we could just always zonk on-the-fly. That is, we introduce new functions like `tcTypeKind` and `tcSubstTy` that zonk as they go. To make sure we're calling the right function at the right time, we introduce `newtype TcType = TcType { unTcType :: Type }`. Then, we're forced to call monadic functions on `TcType`s. This will likely lead to code duplication between `Type` and `TcType`, but we might be able to banish `zonkTcType` (and its many friends) entirely. Also gone would be the `naked` functions, which are all about maintaining the well-kinded type invariant. This step would, as a side effect, fix #15799 and #15918, which is about treating `TcType`s differently from `Type`s. '''Work in progress on `wip/T15952`''' '''Merge request at [https://gitlab.haskell.org/ghc/ghc/merge_requests/74]''' -- -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15952#comment:9> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15952: Reduce zonking-related invariants in the type checker -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: task | Status: closed Priority: normal | Milestone: 8.10.1 Component: Compiler | Version: 8.6.2 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | https://gitlab.haskell.org/ghc/ghc/merge_requests/206 -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => closed * differential: => https://gitlab.haskell.org/ghc/ghc/merge_requests/206 * resolution: => fixed * milestone: => 8.10.1 Comment: Landed in [https://gitlab.haskell.org/ghc/ghc/commit/682783828275cca5fd8bf5be5b52054c75... 682783828275cca5fd8bf5be5b52054c75e0e22c]. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15952#comment:10> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15952: Reduce zonking-related invariants in the type checker -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: task | Status: closed Priority: normal | Milestone: 8.10.1 Component: Compiler | Version: 8.6.2 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | https://gitlab.haskell.org/ghc/ghc/merge_requests/206 -------------------------------------+------------------------------------- Comment (by Simon Peyton Jones <simonpj@…>): In [changeset:"682783828275cca5fd8bf5be5b52054c75e0e22c/ghc" 6827838/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="682783828275cca5fd8bf5be5b52054c75e0e22c" Make a smart mkAppTyM This patch finally delivers on Trac #15952. Specifically * Completely remove Note [The tcType invariant], along with its complicated consequences (IT1-IT6). * Replace Note [The well-kinded type invariant] with: Note [The Purely Kinded Type Invariant (PKTI)] * Instead, establish the (PKTI) in TcHsType.tcInferApps, by using a new function mkAppTyM when building a type application. See Note [mkAppTyM]. * As a result we can remove the delicate mkNakedXX functions entirely. Specifically, mkNakedCastTy retained lots of extremly delicate Refl coercions which just cluttered everything up, and(worse) were very vulnerable to being silently eliminated by (say) substTy. This led to a succession of bug reports. The result is noticeably simpler to explain, simpler to code, and Richard and I are much more confident that it is correct. It does not actually fix any bugs, but it brings us closer. E.g. I hoped it'd fix #15918 and #15799, but it doesn't quite do so. However, it makes it much easier to fix. I also did a raft of other minor refactorings: * Use tcTypeKind consistently in the type checker * Rename tcInstTyBinders to tcInvisibleTyBinders, and refactor it a bit * Refactor tcEqType, pickyEqType, tcEqTypeVis Simpler, probably more efficient. * Make zonkTcType zonk TcTyCons, at least if they have any free unification variables -- see zonk_tc_tycon in TcMType.zonkTcTypeMapper. Not zonking these TcTyCons was actually a bug before. * Simplify try_to_reduce_no_cache in TcFlatten (a lot) * Combine checkExpectedKind and checkExpectedKindX. And then combine the invisible-binder instantation code Much simpler now. * Fix a little bug in TcMType.skolemiseQuantifiedTyVar. I'm not sure how I came across this originally. * Fix a little bug in TyCoRep.isUnliftedRuntimeRep (the ASSERT was over-zealous). Again I'm not certain how I encountered this. * Add a missing solveLocalEqualities in TcHsType.tcHsPartialSigType. I came across this when trying to get level numbers right. }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15952#comment:11> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC