Re: Debug printing inside the typechecker knot

No. You'll see that zonkTcTyVars returns a [TcType], while zonkTyBndrs returns a [TyVar] -- this won't end well. If you look further in zonkTyBndrs, you'll see that it calls `zonkTcTypeToType (tyVarKind tv)` (roughly), making the equivalent to be TcMType.zonkTyCoVarKind.

Ah. I was led astray because there is a TcMType.zonkTyCoVarKind function, but not a TcMType.zonkTyCoVarKinds function (with an -s at the end). Similarly strange is that there is a TcHsType.zonkTyBndrs function, but not a TcHsType.zonkTyBndr function (without an -s at the end). Out of curiosity, is a TcHsType counterpart to TcMType.zonkTcTyVar(s)?

Clearly, it would behoove use to rename these functions to be more systematic.

Indeed. What would be better names for these? It looks like we've identified at least a couple things that could be cleaned up in TcMType and TcHsType, so if you suggest a more consistent naming scheme, I would be willing to implement it. My eventual goal is to write up this wisdom in a GHC wiki page simply because I keep getting frustrated any time I have to debug code in the typechecker knot, and I'd like to codify this solution somewhere where I can look it up in the future if (when) I eventually forget it. Ryan S. On Thu, Apr 4, 2019 at 3:05 PM Richard Eisenberg wrote:

...

On Apr 4, 2019, at 2:55 PM, Ryan Scott wrote:

Good to know, thanks. I assume that TcMType.zonkTcTypes is to TcHsType.zonkTcTypeToTypes as TcMType.zonkTcTyVars is to TcHsType.zonkTyBndrs?

No. You'll see that zonkTcTyVars returns a [TcType], while zonkTyBndrs returns a [TyVar] -- this won't end well. If you look further in zonkTyBndrs, you'll see that it calls `zonkTcTypeToType (tyVarKind tv)` (roughly), making the equivalent to be TcMType.zonkTyCoVarKind.

Clearly, it would behoove use to rename these functions to be more systematic.

...

Also, what exactly is the optimization that ZonkEnv performs in types? And why don't the functions in TcMType make use of this optimization?

Suppose we have

forall (a :: kappa). ... a ...

We laboriously discover that kappa should be (Type -> Type). The ZonkEnv stores a mapping (a |-> (a :: Type -> Type)) so that when we spot the `a` in the body of the forall, we don't have to repeat the zonk -- we just do a lookup. But, of course, zonking the occurrence of `a` would also work.

Why don't we do this in TcMType? There's likely no good reason -- it would be effective there, too. But it would be less effective. The code in TcHsSyn generally starts with *closed* types/terms, meaning that all type variables will be brought into scope somewhere. In contrast, TcMType functions can work over *open* terms, so we have less opportunity to extend the ZonkEnv.

Richard

...

Ryan S. _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs