[Haskell-cafe] ghci's choice of names for type variables

[Julian Bradfield]

On 2021-10-30, Joachim Breitner <mail at joachim-breitner.de> wrote:
> But the type checker also tries to preserves names, and in your example
>
>    Prelude> h (x : xs) = x
>    Prelude> :t h
>    h :: [a] -> a
>
> I _think_ this is an `a` because the list type is declared roughtly
> like follows
>
>    data [a] = [] | a:[a]

Yes, Johannes also suggested that (though I missed it in my first
reading of his message).

>        TyVarTv        -> fsLit "a"

>    | TyVarTv       -- A variant of TauTv, except that it should not be
>                    --   unified with a type, only with a type variable
>                    -- See Note [TyVarTv] in GHC.Tc.Utils.TcMType


The TyVarTv's which are named "a" appear, it says, only in kind
signatures and partial type signatures, neither of which I understand,
so presumably don't use.

> And the others produce either t’s or p’s. For the "p", the relevant
> code is
>
>    newMetaTyVarTyAtLevel :: TcLevel -> TcKind -> TcM TcType
>    newMetaTyVarTyAtLevel tc_lvl kind
>      = do  { details <- newTauTvDetailsAtLevel tc_lvl
>            ; name    <- newMetaTyVarName (fsLit "p")
>            ; return (mkTyVarTy (mkTcTyVar name kind details)) }
>
> but my knowledge of the type checker isn’t good enough to tell you in
> which situations this is used, and when to expect "p" and when to
> expect "t". And maybe GHC shouldn’t use "p" there, and simply
> consistently use "t", so that users aren’t even tempted to think about
> this…

Likewise, I can't work out what's going on here.

-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.