[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
We probably want to keep the pure version for occasions where we know
#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. 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
participants (1)
-
GHC