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@joachim-breitner.de http://www.joachim-breitner.de/