#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