Debug printing inside the typechecker knot

[Ryan Scott]

> 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 <rae at richarde.dev> wrote:
>
>
>
> > On Apr 4, 2019, at 2:55 PM, Ryan Scott <ryan.gl.scott at gmail.com> 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 at haskell.org
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>