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

[Joachim Breitner]

Hi,

Am Samstag, dem 30.10.2021 um 12:06 +0100 schrieb Julian Bradfield:
> I have tried to answer this by google and the list archives, but
> without success, though it wouldn't surprise me if there is a post
> buried somewhere.

I don’t know of such a post, so it’s good that you are starting the
discussion!

I think you looked at the right piece of code: The type inference deals
with metavariables which it instantiates to concrete types as it knows
more, and this is the source or these names:

metaInfoToTyVarName :: MetaInfo -> FastString
metaInfoToTyVarName  meta_info =
  case meta_info of
       TauTv          -> fsLit "t"
       TyVarTv        -> fsLit "a"
       RuntimeUnkTv   -> fsLit "r"
       CycleBreakerTv -> fsLit "b"

And here is the explanation for these:

data MetaInfo
   = TauTv         -- This MetaTv is an ordinary unification variable
                   -- A TauTv is always filled in with a tau-type, which
                   -- never contains any ForAlls.

   | 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

   | RuntimeUnkTv  -- A unification variable used in the GHCi debugger.
                   -- It /is/ allowed to unify with a polytype, unlike TauTv

   | CycleBreakerTv  -- Used to fix occurs-check problems in Givens
                     -- See Note [Type variable cycles] in
                     -- GHC.Tc.Solver.Canonical


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]
   
If we’d define the data type with a different type variable, ghc will
happily use that:

   Prelude> data Foo hello = Foo hello
   Prelude> h (Foo x) = x
   Prelude> :t h
   h :: Foo hello -> hello
   
So I think all examples where you use existing definitions (:, +) the
type variables likely comes from there.

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…

Ok, this was less comprehensive than I hoped for, but maybe others can
pick up this thread

Cheers,
Joachim


-- 
Joachim Breitner
  mail at joachim-breitner.de
  http://www.joachim-breitner.de/