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/

Joachim is right that, when you use a function that's already defined somewhere, GHC will use its choice of type variable names. That explains all the 'a's you observe. As for the others, `t` is GHC's letter of choice most of the time, and it's hard to predict (even for me, with pretty deep knowledge of the type checker) when it will use `p`. Bottom line: don't think about this too much -- there's not much of a signal in the noise. :) Richard

On Oct 30, 2021, at 7:06 AM, Julian Bradfield wrote:

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.

This is GHCI 8.10.7.

When ghci infers types, it sometimes produces types with "a", with "t", and with "p" (and maybe others), as in the following set of examples:

Prelude> h (x : xs) = x Prelude> :t h h :: [a] -> a Prelude> foo f x = not(f x) Prelude> :t foo foo :: (t -> Bool) -> t -> Bool Prelude> bar f x = (f x) + 1 Prelude> :t bar bar :: Num a => (t -> a) -> t -> a Prelude> barb f x g y = (f x)+(g y) Prelude> :t barb barb :: Num a => (t1 -> a) -> t1 -> (t2 -> a) -> t2 -> a Prelude> gar f x = f x Prelude> :t gar gar :: (t1 -> t2) -> t1 -> t2 Prelude> fooa x = x Prelude> :t fooa fooa :: p -> p

What is its rationale? I have attempted to find it in the typechecker code, and I see things that suggest "t" is something to do with tau types (monotypes?), and "p" has something to do with levels, but going from basic Haskell and a modest theoretical acquaintance with System F to being able to read the GHCi type-checker is several steps too far!

Can somebody give me a brief explanation of what's going on? In particular, is there actual information about the types in the choice of letters, or is it just incidental information about the way type inference proceeded?

Thanks, Julian.

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

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.